Safe Haskell	None
Language	GHC2024

Proarrow.Squares.Relative

Synopsis

unit :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k} {e :: k} {j :: hk e a} {t :: vk a e}. (Equipment hk vk, Monad 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 '::: (j '::: ('Nil :: Path hk a a)), 'Nil :: Path vk a a)
mult :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k} {e :: k} {j :: hk e a} {t :: vk a e}. (Equipment hk vk, Monad j (Companion hk t), Ob0 vk a, Ob0 vk e, Ob t, Ob j) => Sq '(Companion hk t '::: (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)
leftAdjunct :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k} {c :: k} {e :: k} {j :: hk e a} {l :: vk a c} {r :: vk c e}. (Equipment hk vk, Adjunction j (Companion hk l) (Companion hk r), Ob0 vk a, Ob0 vk c, Ob0 vk e, Ob j, Ob l, Ob r) => Sq '(Conjoint hk l '::: ('Nil :: Path hk a a), 'Nil :: Path vk a a) '(Companion hk r '::: (j '::: ('Nil :: Path hk a a)), 'Nil :: Path vk c c)
rightAdjunct :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k} {c :: k} {e :: k} {j :: hk e a} {l :: vk a c} {r :: vk c e}. (Equipment hk vk, Adjunction j (Companion hk l) (Companion hk r), Ob0 vk a, Ob0 vk c, Ob0 vk e, Ob j, Ob l, Ob r) => Sq '(Companion hk r '::: (j '::: ('Nil :: Path hk a a)), 'Nil :: Path vk a a) '(Conjoint hk l '::: ('Nil :: Path hk a a), 'Nil :: Path vk c c)

Documentation

unit :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k} {e :: k} {j :: hk e a} {t :: vk a e}. (Equipment hk vk, Monad 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 '::: (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 :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k} {e :: k} {j :: hk e a} {t :: vk a e}. (Equipment hk vk, Monad j (Companion hk t), Ob0 vk a, Ob0 vk e, Ob t, Ob j) => Sq '(Companion hk t '::: (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

leftAdjunct :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k} {c :: k} {e :: k} {j :: hk e a} {l :: vk a c} {r :: vk c e}. (Equipment hk vk, Adjunction j (Companion hk l) (Companion hk r), Ob0 vk a, Ob0 vk c, Ob0 vk e, Ob j, Ob l, Ob r) => Sq '(Conjoint hk l '::: ('Nil :: Path hk a a), 'Nil :: Path vk a a) '(Companion hk r '::: (j '::: ('Nil :: Path hk a a)), 'Nil :: Path vk c c) Source Comments #

j-relative adjunction

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

rightAdjunct :: forall {k} {hk :: k -> k -> Type} {vk :: k -> k -> Type} {a :: k} {c :: k} {e :: k} {j :: hk e a} {l :: vk a c} {r :: vk c e}. (Equipment hk vk, Adjunction j (Companion hk l) (Companion hk r), Ob0 vk a, Ob0 vk c, Ob0 vk e, Ob j, Ob l, Ob r) => Sq '(Companion hk r '::: (j '::: ('Nil :: Path hk a a)), 'Nil :: Path vk a a) '(Conjoint hk l '::: ('Nil :: Path hk a a), 'Nil :: Path vk c c) Source Comments #

j-relative adjunction, other direction

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