| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Bifunctor.Monoidal
Contents
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.grmapcombine.bwdassoc≡fmap(bwdassoc).combine.glmapcombine
Methods
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.
Methods
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 @() @() @Eitherintroduce @(->) @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.grmapintroduce≡bwdunitr.fwdunitr
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.glmapintroduce≡fmap(bwdunitl).fwdunitl