Homotopy Type Theory monoidal dagger category > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed



A monoidal dagger category is a dagger category CC with

  • a functor ()():(C×C)C(-)\otimes(-): (C \times C) \to C from the product dagger category of CC to CC itself called the tensor product.

  • an object Ι:Ob(C)\Iota: Ob(C) called the tensor unit.

  • a type family

p:(()()) =() () p: ((-) \otimes (-))^\dagger = (-)^\dagger \otimes (-)^\dagger

with dependent terms

p f,g:(fg) =f g p_{f,g}: (f \otimes g)^\dagger = f^\dagger \otimes g^\dagger

for morphisms f:hom(D,E)f:hom(D,E) and g:hom(F,G)g:hom(F,G),

  • a natural unitary isomorphism type family
α:(()())() ()(()())\alpha: ((-)\otimes(-))\otimes(-) \cong^\dagger (-)\otimes((-)\otimes(-))

called the associator, with dependent terms

α D,E,F:(DE)F D(EF)\alpha_{D, E, F}: (D\otimes E)\otimes F \cong^\dagger D\otimes(E\otimes F)

for objects D:CD:C, E:CE:C, F:CF:C.

  • a natural unitary isomorphism type family
λ:Ι() ()\lambda: \Iota\otimes(-) \cong^\dagger (-)

called the left unitor, with dependent terms

λ A:ΙA A\lambda_{A}: \Iota\otimes A \cong^\dagger A

for objects A:CA:C.

  • a natural unitary isomorphism type family
ρ:()Ι ()\rho: (-)\otimes\Iota \cong^\dagger (-)

called the right unitor, with dependent terms

ρ A:AΙ A\rho_{A}: A\otimes\Iota \cong^\dagger A

for objects A:CA:C.

  • a type family
τ:ρ ()Ι ()=(Ι ()ρ ())α (),Ι,()\tau: \rho_{(-)} \otimes \Iota_{(-)} = (\Iota_{(-)} \otimes \rho_{(-)}) \circ \alpha_{{(-)}, \Iota, {(-)}}

called the triangle identity, with dependent terms

τ A,B:ρ AΙ B=(1 Aρ B)α A,Ι,B\tau_{A, B}: \rho_A \otimes \Iota_B = (1_A \otimes \rho_B) \circ \alpha_{A, \Iota, B}

for objects A:CA:C, B:CB:C.

  • a type family
π:α (),(),()()α ()(),(),()=(id ()α (),(),())α (),()(),()(α (),(),()id ())\pi: \alpha_{(-), (-), (-) \otimes (-)} \circ \alpha_{(-) \otimes (-), (-), (-)} = (id_{(-)} \otimes \alpha_{(-), (-), (-)}) \circ \alpha_{(-), (-) \otimes (-), (-)} \circ (\alpha_{(-), (-), (-)} \otimes id_{(-)})

called the pentagon identity, with dependent terms

π D,E,F,G:α D,E,FGα DE,F,G=(id Dα E,F,G)α D,EF,G(α D,E,Fid G)\pi_{D,E,F,G}: \alpha_{D, E, F \otimes G} \circ \alpha_{D \otimes E, F, G} = (id_D \otimes \alpha_{E, F, G}) \circ \alpha_{D, E \otimes F, G} \circ (\alpha_{D, E, F} \otimes id_G)

for objects D:CD:C, E:CE:C, F:CF:C, G:CG:C.


See also

Revision on February 14, 2022 at 16:42:56 by Anonymous?. See the history of this page for a list of all contributions to it.