Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class (Associative cat t1, Associative cat t2, Associative cat to) => Semigroupal cat t1 t2 to f where
- combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y'))
- class Unital cat i1 i2 io f where
- introduce :: cat io (f i1 i2)
- class (Tensor cat t1 i1, Tensor cat t2 i2, Tensor cat to io, Semigroupal cat t1 t2 to f, Unital cat i1 i2 io f) => Monoidal cat t1 i1 t2 i2 to io f
Semigroupal
class (Associative cat t1, Associative cat t2, Associative cat to) => Semigroupal cat t1 t2 to f where Source #
Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\).
A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is Semigroupal
if it supports a
natural transformation \(\phi_{AB,CD} : F\ A\ B \bullet F\ C\ D \to F\ (A \otimes C)\ (B \otimes D)\), which we call combine
.
Laws
Associativity:
\[ \require{AMScd} \begin{CD} (F A B \bullet F C D) \bullet F X Y @>>{\alpha_{\mathcal{D}}}> F A B \bullet (F C D \bullet F X Y) \\ @VV{\phi_{AB,CD} \bullet 1}V @VV{1 \bullet \phi_{CD,FY}}V \\ F (A \otimes C) (B \otimes D) \bullet F X Y @. F A B \bullet (F (C \otimes X) (D \otimes Y) \\ @VV{\phi_{(A \otimes C)(B \otimes D),XY}}V @VV{\phi_{AB,(C \otimes X)(D \otimes Y)}}V \\ F ((A \otimes C) \otimes X) ((B \otimes D) \otimes Y) @>>{F \alpha_{\mathcal{C_1}}} \alpha_{\mathcal{C_2}}> F (A \otimes (C \otimes X)) (B \otimes (D \otimes Y)) \\ \end{CD} \]
combine
.
grmap
combine
.
bwd
assoc
≡fmap
(bwd
assoc
).
combine
.
glmap
combine
combine :: cat (to (f x y) (f x' y')) (f (t1 x x') (t2 y y')) Source #
A natural transformation \(\phi_{AB,CD} : F\ A\ B \bullet F\ C\ D \to F\ (A \otimes C)\ (B \otimes D)\).
Examples
>>>
:t combine @(->) @(,) @(,) @(,) @(,)
combine @(->) @(,) @(,) @(,) @(,) :: ((x, y), (x', y')) -> ((x, x'), (y, y'))
>>>
combine @(->) @(,) @(,) @(,) @(,) ((True, "Hello"), ((), "World"))
((True,()),("Hello","World"))
>>>
combine @(->) @(,) @(,) @(,) @(->) (show, (>10)) (True, 11)
("True",True)
Instances
Unital
class Unital cat i1 i2 io f where Source #
Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\).
A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is Unital
if it supports a morphism
\(\phi : I_{\mathcal{D}} \to F\ I_{\mathcal{C_1}}\ I_{\mathcal{C_2}}\), which we call introduce
.
introduce :: cat io (f i1 i2) Source #
introduce
maps from the identity in \(\mathcal{C_1} \times \mathcal{C_2}\) to the
identity in \(\mathcal{D}\).
Examples
>>>
introduce @(->) @() @() @() @(,) ()
((),())
>>>
:t introduce @(->) @Void @() @() @Either
introduce @(->) @Void @() @() @Either :: () -> Either Void ()
>>>
introduce @(->) @Void @() @() @Either ()
Right ()
Instances
Monoidal
class (Tensor cat t1 i1, Tensor cat t2 i2, Tensor cat to io, Semigroupal cat t1 t2 to f, Unital cat i1 i2 io f) => Monoidal cat t1 i1 t2 i2 to io f Source #
Given monoidal categories \((\mathcal{C}, \otimes, I_{\mathcal{C}})\) and \((\mathcal{D}, \bullet, I_{\mathcal{D}})\).
A bifunctor \(F : \mathcal{C_1} \times \mathcal{C_2} \to \mathcal{D}\) is Monoidal
if it maps between \(\mathcal{C_1} \times \mathcal{C_2}\)
and \(\mathcal{D}\) while preserving their monoidal structure. Eg., a homomorphism of monoidal categories.
See NCatlab for more details.
Laws
Right Unitality:
\[ \require{AMScd} \begin{CD} F A B \bullet I_{\mathcal{D}} @>{1 \bullet \phi}>> F A B \bullet F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}}\\ @VV{\rho_{\mathcal{D}}}V @VV{\phi AB,I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}}}V \\ F A B @<<{F \rho_{\mathcal{C_{1}}} \rho_{\mathcal{C_{2}}}}< F (A \otimes I_{\mathcal{C_{1}}}) (B \otimes I_{\mathcal{C_{2}}}) \end{CD} \]
combine
.
grmap
introduce
≡bwd
unitr
.
fwd
unitr
Left Unitality:
\[ \begin{CD} I_{\mathcal{D}} \bullet F A B @>{\phi \bullet 1}>> F I_{\mathcal{C_{1}}} I_{\mathcal{C_{2}}} \bullet F A B\\ @VV{\lambda_{\mathcal{D}}}V @VV{I_{\mathcal{C_{1}}}I_{\mathcal{C_{2}}},\phi AB}V \\ F A B @<<{F \lambda_{\mathcal{C_{1}}} \lambda_{\mathcal{C_{2}}}}< F (I_{\mathcal{C_{1}}} \otimes A) (I_{\mathcal{C_{2}}} \otimes B) \end{CD} \]
combine
.
glmap
introduce
≡fmap
(bwd
unitl
).
fwd
unitl