Safe Haskell	None
Language	Haskell2010

Proarrow.Squares

Synopsis

object :: forall {k1} (hk :: CAT k1) (vk :: CAT k1) (k2 :: k1). (HasCompanions hk vk, Ob0 vk k2) => Sq '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2) '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2)
hArr :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: CAT k1} {j :: k1} {k2 :: k1} (p :: hk j k2) (q :: hk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) => (p ~> q) -> Sq '(p '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk k2 k2) '(q '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk j j)
hId :: forall {k1} (hk :: CAT k1) (vk :: CAT k1) (j :: k1) (k2 :: k1) (p :: hk k2 j). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob p) => Sq '(p '::: ('Nil :: Path hk j j), 'Nil :: Path vk j j) '(p '::: ('Nil :: Path hk j j), 'Nil :: Path vk k2 k2)
compId :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob0 hk j, Ob0 hk k2, Ob f) => Sq '(Companion hk f '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk k2 k2) '(Companion hk f '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk j j)
conjId :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (f :: vk j k2). (Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) => Sq '(Conjoint hk f '::: ('Nil :: Path hk j j), 'Nil :: Path vk j j) '(Conjoint hk f '::: ('Nil :: Path hk j j), 'Nil :: Path vk k2 k2)
vArr :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2) (g :: vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) => (f ~> g) -> Sq '('Nil :: Path hk j j, f '::: ('Nil :: Path vk k2 k2)) '(I :: Path hk k2 k2, g '::: ('Nil :: Path vk k2 k2))
vId :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) => Sq '('Nil :: Path hk j j, f '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, f '::: ('Nil :: Path vk k2 k2))
vId' :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) => Obj f -> Sq '('Nil :: Path hk j j, f '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, f '::: ('Nil :: Path vk k2 k2))
(|||) :: forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1} {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l) (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h) (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2). HasCompanions hk vk => Sq '(ps, ds) '(qs, es) -> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs)
(===) :: forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1} {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j) (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i) (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2). HasCompanions hk vk => Sq '(rs, es) '(ss, fs) -> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs)
toRight :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob' f) => Sq '('Nil :: Path hk j j, f '::: ('Nil :: Path vk k2 k2)) '(Companion hk f '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk j j)
toLeft :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2). (Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) => Sq '(Conjoint hk f '::: ('Nil :: Path hk j j), f '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2)
fromLeft :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob' f) => Sq '(Companion hk f '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk k2 k2) '('Nil :: Path hk k2 k2, f '::: ('Nil :: Path vk k2 k2))
fromRight :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2). (Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) => Sq '('Nil :: Path hk j j, 'Nil :: Path vk j j) '(Conjoint hk f '::: ('Nil :: Path hk j j), f '::: ('Nil :: Path vk k2 k2))
vUnitor :: forall {k1} (hk :: CAT k1) (vk :: CAT k1) (k2 :: k1). (HasCompanions hk vk, Ob0 vk k2) => Sq '('Nil :: Path hk k2 k2, (I :: vk k2 k2) '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2)
vUnitorInv :: forall {s} (hk :: CAT s) (vk :: CAT s) (k :: s). (HasCompanions hk vk, Ob0 vk k) => Sq '('Nil :: Path hk k k, 'Nil :: Path vk k k) '('Nil :: Path hk k k, (I :: vk k k) '::: ('Nil :: Path vk k k))
vCombine :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (f :: vk i j) (g :: vk j k2). (HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob0 hk i, Ob0 hk j, Ob0 hk k2, Ob f, Ob g) => Sq '('Nil :: Path hk i i, f '::: (g '::: ('Nil :: Path vk k2 k2))) '('Nil :: Path hk k2 k2, O g f '::: ('Nil :: Path vk k2 k2))
vSplit :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (f :: vk i j) (g :: vk j k2). (HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob0 hk i, Ob0 hk j, Ob0 hk k2, Ob f, Ob g) => Sq '('Nil :: Path hk i i, O g f '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, f '::: (g '::: ('Nil :: Path vk k2 k2)))

Documentation

object :: forall {k1} (hk :: CAT k1) (vk :: CAT k1) (k2 :: k1). (HasCompanions hk vk, Ob0 vk k2) => Sq '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2) '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2) Source Comments #

The empty square for an object.

k-----k
|     |
|     |
|     |
k-----k

hArr :: forall {k1} {hk :: k1 -> k1 -> Type} {vk :: CAT k1} {j :: k1} {k2 :: k1} (p :: hk j k2) (q :: hk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) => (p ~> q) -> Sq '(p '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk k2 k2) '(q '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk j j) Source Comments #

Make a square from a horizontal proarrow

k-----k
|     |
p--@--q
|     |
j-----j

hId :: forall {k1} (hk :: CAT k1) (vk :: CAT k1) (j :: k1) (k2 :: k1) (p :: hk k2 j). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob p) => Sq '(p '::: ('Nil :: Path hk j j), 'Nil :: Path vk j j) '(p '::: ('Nil :: Path hk j j), 'Nil :: Path vk k2 k2) Source Comments #

A horizontal identity square.

j-----j
|     |
p-----p
|     |
k-----k

compId :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob0 hk j, Ob0 hk k2, Ob f) => Sq '(Companion hk f '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk k2 k2) '(Companion hk f '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk j j) Source Comments #

A horizontal identity square for a companion.

Requires a type application: compId @f

k-----k
|     |
f>--->f
|     |
j-----j

conjId :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (f :: vk j k2). (Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) => Sq '(Conjoint hk f '::: ('Nil :: Path hk j j), 'Nil :: Path vk j j) '(Conjoint hk f '::: ('Nil :: Path hk j j), 'Nil :: Path vk k2 k2) Source Comments #

A horizontal identity square for a conjoint.

Requires a type application: conjId @f

j-----j
|     |
f>--->f
|     |
k-----k

vArr :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2) (g :: vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) => (f ~> g) -> Sq '('Nil :: Path hk j j, f '::: ('Nil :: Path vk k2 k2)) '(I :: Path hk k2 k2, g '::: ('Nil :: Path vk k2 k2)) Source Comments #

Make a square from a vertical arrow

j--f--k
|  v  |
|  @  |
|  v  |
j--g--k

vId :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob f) => Sq '('Nil :: Path hk j j, f '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, f '::: ('Nil :: Path vk k2 k2)) Source Comments #

A vertical identity square.

j--f--k
|  v  |
|  |  |
|  v  |
j--f--k

vId' :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2) => Obj f -> Sq '('Nil :: Path hk j j, f '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, f '::: ('Nil :: Path vk k2 k2)) Source Comments #

(|||) :: forall {k1} {b :: k1} {k2 :: k1} {i :: k1} {hk :: CAT k1} {vk :: CAT k1} {h :: k1} {l :: k1} {m :: k1} (ps :: Path hk m l) (qs :: Path hk b h) (rs :: Path hk k2 i) (ds :: Path vk l h) (es :: Path vk m b) (fs :: Path vk h i) (gs :: Path vk b k2). HasCompanions hk vk => Sq '(ps, ds) '(qs, es) -> Sq '(qs, fs) '(rs, gs) -> Sq '(ps, ds +++ fs) '(rs, es +++ gs) infixl 6 Source Comments #

Horizontal composition

l--d--h     h--f--i     l-d+f-i
|  v  |     |  v  |     |  v  |
p--@--q ||| q--@--r  =  p--@--r
|  v  |     |  v  |     |  v  |
m--e--j     j--g--k     m-e+g-k

(===) :: forall {k1} {k2 :: k1} {b :: k1} {hk :: CAT k1} {vk :: CAT k1} {h :: k1} {i :: k1} {j :: k1} {l :: k1} (ps :: Path hk l j) (qs :: Path hk k2 b) (rs :: Path hk j h) (ss :: Path hk b i) (es :: Path vk h i) (fs :: Path vk j b) (gs :: Path vk l k2). HasCompanions hk vk => Sq '(rs, es) '(ss, fs) -> Sq '(ps, fs) '(qs, gs) -> Sq '(ps +++ rs, es) '(qs +++ ss, gs) infixl 5 Source Comments #

Vertical composition

 h--e--i
 |  v  |
 r--@--s
 |  v  |
 j--f--k
   ===
 j--f--k
 |  v  |
 p--@--q
 |  v  |
 l--g--m

   v v

 h--e--i
 |  v  |
p+r-@-q+s
 |  v  |
 j--g--k

toRight :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob' f) => Sq '('Nil :: Path hk j j, f '::: ('Nil :: Path vk k2 k2)) '(Companion hk f '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk j j) Source Comments #

Bend a vertical arrow in the companion direction.

j--f--k
|  v  |
|  \->f
|     |
j-----j

toLeft :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2). (Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) => Sq '(Conjoint hk f '::: ('Nil :: Path hk j j), f '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2) Source Comments #

Bend a vertical arrow in the conjoint direction.

j--f--k
|  v  |
f<-/  |
|     |
k-----k

fromLeft :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (f :: vk j k2). (HasCompanions hk vk, Ob' f) => Sq '(Companion hk f '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk k2 k2) '('Nil :: Path hk k2 k2, f '::: ('Nil :: Path vk k2 k2)) Source Comments #

Bend a companion proarrow back to a vertical arrow.

k-----k
|     |
f>-\  |
|  v  |
j--f--k

fromRight :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {j :: k1} {k2 :: k1} (f :: vk j k2). (Equipment hk vk, Ob0 vk j, Ob0 vk k2, Ob f) => Sq '('Nil :: Path hk j j, 'Nil :: Path vk j j) '(Conjoint hk f '::: ('Nil :: Path hk j j), f '::: ('Nil :: Path vk k2 k2)) Source Comments #

Bend a conjoint proarrow back to a vertical arrow.

j-----j
|     |
|  /-<f
|  v  |
j--f--k

vUnitor :: forall {k1} (hk :: CAT k1) (vk :: CAT k1) (k2 :: k1). (HasCompanions hk vk, Ob0 vk k2) => Sq '('Nil :: Path hk k2 k2, (I :: vk k2 k2) '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, 'Nil :: Path vk k2 k2) Source Comments #

vUnitorInv :: forall {s} (hk :: CAT s) (vk :: CAT s) (k :: s). (HasCompanions hk vk, Ob0 vk k) => Sq '('Nil :: Path hk k k, 'Nil :: Path vk k k) '('Nil :: Path hk k k, (I :: vk k k) '::: ('Nil :: Path vk k k)) Source Comments #

vCombine :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (f :: vk i j) (g :: vk j k2). (HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob0 hk i, Ob0 hk j, Ob0 hk k2, Ob f, Ob g) => Sq '('Nil :: Path hk i i, f '::: (g '::: ('Nil :: Path vk k2 k2))) '('Nil :: Path hk k2 k2, O g f '::: ('Nil :: Path vk k2 k2)) Source Comments #

vSplit :: forall {k1} {hk :: CAT k1} {vk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} (f :: vk i j) (g :: vk j k2). (HasCompanions hk vk, Ob0 vk i, Ob0 vk j, Ob0 vk k2, Ob0 hk i, Ob0 hk j, Ob0 hk k2, Ob f, Ob g) => Sq '('Nil :: Path hk i i, O g f '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, f '::: (g '::: ('Nil :: Path vk k2 k2))) Source Comments #