Safe Haskell	None
Language	GHC2024

Proarrow.Squares.Relative

Synopsis

unit :: forall {k} {kk :: k -> k -> Type} {a :: k} {e :: k} {j :: kk e a} {t :: kk a e}. (Equipment kk, Monad j t, IsTight t) => Sq ('Nil :: Path kk a a) (t '::: (j '::: ('Nil :: Path kk a a))) ('Nil :: Path kk a a) ('Nil :: Path kk a a)
mult :: forall {k} {kk :: k -> k -> Type} {a :: k} {e :: k} {j :: kk e a} {t :: kk a e} (t' :: kk e a). (Equipment kk, Monad j t, TightPair t t') => Sq (t '::: (j '::: ('Nil :: Path kk a a))) (t '::: (t' '::: ('Nil :: Path kk a a))) ('Nil :: Path kk a a) ('Nil :: Path kk a a)
leftAdjunct :: forall {k} {kk :: k -> k -> Type} {a :: k} {c :: k} {e :: k} {j :: kk e a} {l :: kk a c} {l' :: kk c a} {r :: kk c e}. (Equipment kk, Adjunction j l r, IsTight r, TightPair l l') => Sq (l' '::: ('Nil :: Path kk a a)) (r '::: (j '::: ('Nil :: Path kk a a))) ('Nil :: Path kk a a) ('Nil :: Path kk c c)
rightAdjunct :: forall {k} {kk :: k -> k -> Type} {a :: k} {c :: k} {e :: k} {j :: kk e a} {l :: kk a c} {l' :: kk c a} {r :: kk c e}. (Equipment kk, Adjunction j l r, IsTight r, TightPair l l') => Sq (r '::: (j '::: ('Nil :: Path kk a a))) (l' '::: ('Nil :: Path kk a a)) ('Nil :: Path kk a a) ('Nil :: Path kk c c)

Documentation

unit :: forall {k} {kk :: k -> k -> Type} {a :: k} {e :: k} {j :: kk e a} {t :: kk a e}. (Equipment kk, Monad j t, IsTight t) => Sq ('Nil :: Path kk a a) (t '::: (j '::: ('Nil :: Path kk a a))) ('Nil :: Path kk a a) ('Nil :: Path kk a a) Source Comments #

The unit square for a j-relative monad t.

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

mult :: forall {k} {kk :: k -> k -> Type} {a :: k} {e :: k} {j :: kk e a} {t :: kk a e} (t' :: kk e a). (Equipment kk, Monad j t, TightPair t t') => Sq (t '::: (j '::: ('Nil :: Path kk a a))) (t '::: (t' '::: ('Nil :: Path kk a a))) ('Nil :: Path kk a a) ('Nil :: Path kk a a) Source Comments #

The multiplication square for a j-relative monad t.

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

leftAdjunct :: forall {k} {kk :: k -> k -> Type} {a :: k} {c :: k} {e :: k} {j :: kk e a} {l :: kk a c} {l' :: kk c a} {r :: kk c e}. (Equipment kk, Adjunction j l r, IsTight r, TightPair l l') => Sq (l' '::: ('Nil :: Path kk a a)) (r '::: (j '::: ('Nil :: Path kk a a))) ('Nil :: Path kk a a) ('Nil :: Path kk c c) Source Comments #

j-relative adjunction

A-----A
|  /--j
l<-@  |
|  \->r
C-----C

rightAdjunct :: forall {k} {kk :: k -> k -> Type} {a :: k} {c :: k} {e :: k} {j :: kk e a} {l :: kk a c} {l' :: kk c a} {r :: kk c e}. (Equipment kk, Adjunction j l r, IsTight r, TightPair l l') => Sq (r '::: (j '::: ('Nil :: Path kk a a))) (l' '::: ('Nil :: Path kk a a)) ('Nil :: Path kk a a) ('Nil :: Path kk c c) Source Comments #

j-relative adjunction, other direction

A-----A
j--\  |
|  @<-l
r->/  |
C-----C