内部合成子 - 雑多な感じ

内部合成子

internal composition operator

モノイダル閉圏の指数随伴系において

射の合成の内部hom函手バージョン

https://gyazo.com/84297f1a4b95b9ecebbed440f957cde9

code:sig

(a,b,c).comp : (a⊸b)⊗(b⊸c) -> a⊸c

(a,b,c).comp =

(a⊸b)⊗(b⊸c).a.unit

; a ⊸ (a,(a⊸b),(b⊸c)).α-

; a ⊸ b.a.eval ⊗ (b⊸c)

; a ⊸ c.b.eval

where

L-C-MC C ⊗ i α λ ρ

左モノイダル閉圏

Adjunction C C (a⊗) (a⊸) a.unit a.eval

任意の対象aについての左指数随伴系

性質

内部恒等射との合成は恒等射

内部合成子と内部恒等射の単位律

結合律

WIP.icon