proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Squares.Relative

Synopsis

Documentation

unit :: forall {k} {hk :: CAT k} {vk :: k -> k -> Type} {a :: k} {e :: k} {j :: vk a e} {t :: vk a e}. (Equipment hk vk, Monad (Conjoint hk j) (Companion hk t), Ob0 vk a, Ob0 vk e, Ob t, Ob j) => Sq '('Nil :: Path hk a a, 'Nil :: Path vk a a) '(Companion hk t '::: (Conjoint hk j '::: ('Nil :: Path hk a a)), 'Nil :: Path vk a a) Source Comments #

The unit square for a j-relative monad t.

A-----A
|  /-<j
|  @  |
|  \->t
A-----A

mult :: forall {k} {hk :: CAT k} {vk :: k -> k -> Type} {a :: k} {e :: k} {j :: vk a e} {t :: vk a e}. (Equipment hk vk, Monad (Conjoint hk j) (Companion hk t), Ob0 vk a, Ob0 vk e, Ob t, Ob j) => Sq '(Companion hk t '::: (Conjoint hk j '::: (Companion hk t '::: ('Nil :: Path hk e e))), 'Nil :: Path vk e e) '(Companion hk t '::: ('Nil :: Path hk e e), 'Nil :: Path vk a a) Source Comments #

The multiplication square for a j-relative monad t.

E-----E
t>-\  |
j<-@->t
t>-/  |
A-----A