| 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, 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, 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, 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)))
- vCombineAll :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob ps) => Sq '('Nil :: Path hk j j, ps) '('Nil :: Path hk k2 k2, Fold ps '::: ('Nil :: Path vk k2 k2))
- vSplitAll :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob ps) => Sq '('Nil :: Path hk j j, Fold ps '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, ps)
- hCombineAll :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path hk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob ps) => Sq '(ps, 'Nil :: Path vk k2 k2) '(Fold ps '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk j j)
- hSplitAll :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path hk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob ps) => Sq '(Fold ps '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk k2 k2) '(ps, 'Nil :: Path vk j j)
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, 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, 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, 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 #
vCombineAll :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob ps) => Sq '('Nil :: Path hk j j, ps) '('Nil :: Path hk k2 k2, Fold ps '::: ('Nil :: Path vk k2 k2)) Source Comments #
Combine a whole bunch of vertical arrows into one composed arrow.
J-p..-K | vvv | | \@/ | | v | J--f--K
vSplitAll :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path vk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob ps) => Sq '('Nil :: Path hk j j, Fold ps '::: ('Nil :: Path vk k2 k2)) '('Nil :: Path hk k2 k2, ps) Source Comments #
Split one composed arrow into a whole bunch of vertical arrows.
J--f--K | v | | /@\ | | vvv | J-p..-K
hCombineAll :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path hk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob ps) => Sq '(ps, 'Nil :: Path vk k2 k2) '(Fold ps '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk j j) Source Comments #
Combine a whole bunch of horizontal proarrows into one composed proarrow.
K-----K p--\ | :--@--f :--/ | J-----J
hSplitAll :: forall {k1} {hk :: CAT k1} {vk :: CAT k1} {j :: k1} {k2 :: k1} (ps :: Path hk j k2). (HasCompanions hk vk, Ob0 vk j, Ob0 vk k2, Ob ps) => Sq '(Fold ps '::: ('Nil :: Path hk k2 k2), 'Nil :: Path vk k2 k2) '(ps, 'Nil :: Path vk j j) Source Comments #
Split one composed proarrow into a whole bunch of horizontal proarrows.
K-----K | /--p f--@--: | \--: J-----J