Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Double

Synopsis

type SQ1 (hk :: CAT c) (vk :: CAT c) = forall {h :: c} {i :: c} {j :: c} {k :: c}. hk h j -> hk i k -> vk h i -> vk j k -> Type
type SQ (hk :: CAT c) (vk :: CAT c) = SQ1 (Path hk) (Path vk)
class (Bicategory hk, Bicategory vk) => Double (hk :: CAT k) (vk :: CAT k) where
- data Sq (hk :: CAT k) (vk :: CAT k) :: SQ hk vk
- data Sq1 (hk :: CAT k) (vk :: CAT k) :: SQ1 hk vk
- singleton :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (p :: hk h j) (q :: hk i k1) (f :: vk h i) (g :: vk j k1). (DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k1, Ob p, Ob q, Ob f, Ob g) => Sq1 hk vk p q f g -> Sq hk vk (p '::: ('Nil :: Path hk j j)) (q '::: ('Nil :: Path hk k1 k1)) (f '::: ('Nil :: Path vk i i)) (g '::: ('Nil :: Path vk k1 k1))
- folded :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path hk h j) (qs :: Path hk i k1) (fs :: Path vk h i) (gs :: Path vk j k1). (DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k1, Ob ps, Ob qs, Ob fs, Ob gs) => Sq hk vk ps qs fs gs -> Sq1 hk vk (Fold ps) (Fold qs) (Fold fs) (Fold gs)
- object :: forall (k1 :: k). DOb hk vk k1 => Sq hk vk ('Nil :: Path hk k1 k1) ('Nil :: Path hk k1 k1) ('Nil :: Path vk k1 k1) ('Nil :: Path vk k1 k1)
- hArr :: forall (j :: k) (k1 :: k) (ps :: Path hk j k1) (qs :: Path hk j k1). (DOb hk vk j, DOb hk vk k1) => (ps ~> qs) -> Sq hk vk ps qs ('Nil :: Path vk j j) ('Nil :: Path vk k1 k1)
- hArr1 :: forall (j :: k) (k1 :: k) (p :: hk j k1) (q :: hk j k1). (DOb hk vk j, DOb hk vk k1) => (p ~> q) -> Sq1 hk vk p q (I :: vk j j) (I :: vk k1 k1)
- (|||) :: forall {a1 :: k} {a2 :: k} {b1 :: k} {b2 :: k} {c1 :: k} {c2 :: k} (ps :: Path hk a1 a2) (qs :: Path hk b1 b2) (fs :: Path vk a1 b1) (gs :: Path vk a2 b2) (rs :: Path hk c1 c2) (hs :: Path vk b1 c1) (is :: Path vk b2 c2). Sq hk vk ps qs fs gs -> Sq hk vk qs rs hs is -> Sq hk vk ps rs (fs +++ hs) (gs +++ is)
- vArr :: forall (j :: k) (k1 :: k) (fs :: Path vk j k1) (gs :: Path vk j k1). (DOb hk vk j, DOb hk vk k1) => (fs ~> gs) -> Sq hk vk ('Nil :: Path hk j j) ('Nil :: Path hk k1 k1) fs gs
- vArr1 :: forall (j :: k) (k1 :: k) (f :: vk j k1) (g :: vk j k1). (DOb hk vk j, DOb hk vk k1) => (f ~> g) -> Sq1 hk vk (I :: hk j j) (I :: hk k1 k1) f g
- (===) :: forall {h :: k} {b1 :: k} {i :: k} {b2 :: k} {j :: k} {k1 :: k} (ps :: Path hk h b1) (qs :: Path hk i b2) (fs :: Path vk h i) (gs :: Path vk b1 b2) (rs :: Path hk b1 j) (ss :: Path hk b2 k1) (hs :: Path vk j k1). Sq hk vk ps qs fs gs -> Sq hk vk rs ss gs hs -> Sq hk vk (ps +++ rs) (qs +++ ss) fs hs
- (\\\\) :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path hk h j) (qs :: Path hk i k1) (fs :: Path vk h i) (gs :: Path vk j k1) r. ((DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k1, Ob ps, Ob qs, Ob fs, Ob gs) => r) -> Sq hk vk ps qs fs gs -> r
type DOb (hk :: CAT k) (vk :: CAT k1) (k3 :: k2) = (Ob0 hk k3, Ob0 vk k3)
class Double hk vk => Equipment (hk :: k -> k -> Type) (vk :: k -> k -> Type) where
- type Companion (hk :: k -> k -> Type) (vk :: k -> k -> Type) (f :: vk j k1) :: hk j k1
- type Conjoint (hk :: k -> k -> Type) (vk :: k -> k -> Type) (f :: vk j k1) :: hk k1 j
- fromRight :: forall (j :: k) (k1 :: k) (f :: vk j k1). (DOb hk vk j, DOb hk vk k1, Ob f) => Sq hk vk ('Nil :: Path hk j j) (Companion hk vk f '::: ('Nil :: Path hk k1 k1)) ('Nil :: Path vk j j) (f '::: ('Nil :: Path vk k1 k1))
- toLeft :: forall (j :: k) (k1 :: k) (f :: vk j k1). (DOb hk vk j, DOb hk vk k1, Ob f) => Sq hk vk (Companion hk vk f '::: ('Nil :: Path hk k1 k1)) ('Nil :: Path hk k1 k1) (f '::: ('Nil :: Path vk k1 k1)) ('Nil :: Path vk k1 k1)
- toRight :: forall (j :: k) (k1 :: k) (f :: vk j k1). (DOb hk vk j, DOb hk vk k1, Ob f) => Sq hk vk ('Nil :: Path hk j j) (Conjoint hk vk f '::: ('Nil :: Path hk j j)) (f '::: ('Nil :: Path vk k1 k1)) ('Nil :: Path vk j j)
- fromLeft :: forall (j :: k) (k1 :: k) (f :: vk j k1). (DOb hk vk j, DOb hk vk k1, Ob f) => Sq hk vk (Conjoint hk vk f '::: ('Nil :: Path hk j j)) ('Nil :: Path hk k1 k1) ('Nil :: Path vk k1 k1) (f '::: ('Nil :: Path vk k1 k1))
- withComOb :: forall (j :: k) (k1 :: k) (f :: vk j k1) r. (DOb hk vk j, DOb hk vk k1, Ob f) => Obj f -> (Ob (Companion hk vk f) => r) -> r
- withConOb :: forall (j :: k) (k1 :: k) (f :: vk j k1) r. (DOb hk vk j, DOb hk vk k1, Ob f) => Obj f -> (Ob (Conjoint hk vk f) => r) -> r
type UnOp (ps :: Path (OPK kk) j k1) = UN ('OP :: kk k1 j -> OPK kk j k1) (Fold ps)
type UnCo (fs :: Path (COK kk) j k1) = UN ('CO :: kk j k1 -> COK kk j k1) (Fold fs)
type CoSq (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1) = Sq (OPK hk) (COK vk) ps qs fs gs

Documentation

type SQ1 (hk :: CAT c) (vk :: CAT c) = forall {h :: c} {i :: c} {j :: c} {k :: c}. hk h j -> hk i k -> vk h i -> vk j k -> Type Source Comments #

The kind of a square p q f g. > h--f--i > | v | > p--@--q > | v | > j--g--k

type SQ (hk :: CAT c) (vk :: CAT c) = SQ1 (Path hk) (Path vk) Source Comments #

class (Bicategory hk, Bicategory vk) => Double (hk :: CAT k) (vk :: CAT k) where Source Comments #

Double categories, strictified in both directions.

Associated Types

data Sq (hk :: CAT k) (vk :: CAT k) :: SQ hk vk Source Comments #

data Sq1 (hk :: CAT k) (vk :: CAT k) :: SQ1 hk vk Source Comments #

Methods

singleton :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (p :: hk h j) (q :: hk i k1) (f :: vk h i) (g :: vk j k1). (DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k1, Ob p, Ob q, Ob f, Ob g) => Sq1 hk vk p q f g -> Sq hk vk (p '::: ('Nil :: Path hk j j)) (q '::: ('Nil :: Path hk k1 k1)) (f '::: ('Nil :: Path vk i i)) (g '::: ('Nil :: Path vk k1 k1)) Source Comments #

folded :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path hk h j) (qs :: Path hk i k1) (fs :: Path vk h i) (gs :: Path vk j k1). (DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k1, Ob ps, Ob qs, Ob fs, Ob gs) => Sq hk vk ps qs fs gs -> Sq1 hk vk (Fold ps) (Fold qs) (Fold fs) (Fold gs) Source Comments #

object :: forall (k1 :: k). DOb hk vk k1 => Sq hk vk ('Nil :: Path hk k1 k1) ('Nil :: Path hk k1 k1) ('Nil :: Path vk k1 k1) ('Nil :: Path vk k1 k1) Source Comments #

The empty square for an object.

hArr :: forall (j :: k) (k1 :: k) (ps :: Path hk j k1) (qs :: Path hk j k1). (DOb hk vk j, DOb hk vk k1) => (ps ~> qs) -> Sq hk vk ps qs ('Nil :: Path vk j j) ('Nil :: Path vk k1 k1) Source Comments #

Make a square from a horizontal arrow

hArr1 :: forall (j :: k) (k1 :: k) (p :: hk j k1) (q :: hk j k1). (DOb hk vk j, DOb hk vk k1) => (p ~> q) -> Sq1 hk vk p q (I :: vk j j) (I :: vk k1 k1) Source Comments #

(|||) :: forall {a1 :: k} {a2 :: k} {b1 :: k} {b2 :: k} {c1 :: k} {c2 :: k} (ps :: Path hk a1 a2) (qs :: Path hk b1 b2) (fs :: Path vk a1 b1) (gs :: Path vk a2 b2) (rs :: Path hk c1 c2) (hs :: Path vk b1 c1) (is :: Path vk b2 c2). Sq hk vk ps qs fs gs -> Sq hk vk qs rs hs is -> Sq hk vk ps rs (fs +++ hs) (gs +++ is) infixl 6 Source Comments #

Horizontal composition

vArr :: forall (j :: k) (k1 :: k) (fs :: Path vk j k1) (gs :: Path vk j k1). (DOb hk vk j, DOb hk vk k1) => (fs ~> gs) -> Sq hk vk ('Nil :: Path hk j j) ('Nil :: Path hk k1 k1) fs gs Source Comments #

Make a square from a vertical arrow (in the opposite direction to match the quintet construction)

vArr1 :: forall (j :: k) (k1 :: k) (f :: vk j k1) (g :: vk j k1). (DOb hk vk j, DOb hk vk k1) => (f ~> g) -> Sq1 hk vk (I :: hk j j) (I :: hk k1 k1) f g Source Comments #

(===) :: forall {h :: k} {b1 :: k} {i :: k} {b2 :: k} {j :: k} {k1 :: k} (ps :: Path hk h b1) (qs :: Path hk i b2) (fs :: Path vk h i) (gs :: Path vk b1 b2) (rs :: Path hk b1 j) (ss :: Path hk b2 k1) (hs :: Path vk j k1). Sq hk vk ps qs fs gs -> Sq hk vk rs ss gs hs -> Sq hk vk (ps +++ rs) (qs +++ ss) fs hs infixl 5 Source Comments #

Vertical composition

(\\\\) :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path hk h j) (qs :: Path hk i k1) (fs :: Path vk h i) (gs :: Path vk j k1) r. ((DOb hk vk h, DOb hk vk i, DOb hk vk j, DOb hk vk k1, Ob ps, Ob qs, Ob fs, Ob gs) => r) -> Sq hk vk ps qs fs gs -> r Source Comments #

Instances

Instances details

Double hk vk => Double (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Double

Associated Types

data Sq (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1)
Instance details Defined in Proarrow.Category.Double data Sq (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1) where CoSq :: forall {k} {hk :: CAT k} {vk :: CAT k} {h :: k} {i :: k} {j :: k} {k1 :: k} (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1). (Ob ps, Ob qs, Ob fs, Ob gs) => Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs) -> Sq (OPK hk) (COK vk) ps qs fs gs
data Sq1 (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (p :: OPK hk h j) (q :: OPK hk i k1) (f :: COK vk h i) (g :: COK vk j k1)
Instance details Defined in Proarrow.Category.Double data Sq1 (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) (p :: OPK hk h j) (q :: OPK hk i k1) (f :: COK vk h i) (g :: COK vk j k1) where CoSq1 :: forall {k} {h :: k} {j :: k} {i :: k} {k1 :: k} (hk :: CAT k) (vk :: CAT k) (p :: OPK hk h j) (q :: OPK hk i k1) (g :: COK vk j k1) (f :: COK vk h i). Sq1 hk vk (UN ('OP :: hk j h -> OPK hk h j) p) (UN ('OP :: hk k1 i -> OPK hk i k1) q) (UN ('CO :: vk j k1 -> COK vk j k1) g) (UN ('CO :: vk h i -> COK vk h i) f) -> Sq1 (OPK hk) (COK vk) p q f g

Methods

singleton :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (p :: OPK hk h j) (q :: OPK hk i k1) (f :: COK vk h i) (g :: COK vk j k1). (DOb (OPK hk) (COK vk) h, DOb (OPK hk) (COK vk) i, DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1, Ob p, Ob q, Ob f, Ob g) => Sq1 (OPK hk) (COK vk) p q f g -> Sq (OPK hk) (COK vk) (p '::: ('Nil :: Path (OPK hk) j j)) (q '::: ('Nil :: Path (OPK hk) k1 k1)) (f '::: ('Nil :: Path (COK vk) i i)) (g '::: ('Nil :: Path (COK vk) k1 k1)) Source Comments #

folded :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1). (DOb (OPK hk) (COK vk) h, DOb (OPK hk) (COK vk) i, DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1, Ob ps, Ob qs, Ob fs, Ob gs) => Sq (OPK hk) (COK vk) ps qs fs gs -> Sq1 (OPK hk) (COK vk) (Fold ps) (Fold qs) (Fold fs) (Fold gs) Source Comments #

object :: forall (k1 :: k). DOb (OPK hk) (COK vk) k1 => Sq (OPK hk) (COK vk) ('Nil :: Path (OPK hk) k1 k1) ('Nil :: Path (OPK hk) k1 k1) ('Nil :: Path (COK vk) k1 k1) ('Nil :: Path (COK vk) k1 k1) Source Comments #

hArr :: forall (j :: k) (k1 :: k) (ps :: Path (OPK hk) j k1) (qs :: Path (OPK hk) j k1). (DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1) => (ps ~> qs) -> Sq (OPK hk) (COK vk) ps qs ('Nil :: Path (COK vk) j j) ('Nil :: Path (COK vk) k1 k1) Source Comments #

hArr1 :: forall (j :: k) (k1 :: k) (p :: OPK hk j k1) (q :: OPK hk j k1). (DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1) => (p ~> q) -> Sq1 (OPK hk) (COK vk) p q (I :: COK vk j j) (I :: COK vk k1 k1) Source Comments #

(|||) :: forall {a1 :: k} {a2 :: k} {b1 :: k} {b2 :: k} {c1 :: k} {c2 :: k} (ps :: Path (OPK hk) a1 a2) (qs :: Path (OPK hk) b1 b2) (fs :: Path (COK vk) a1 b1) (gs :: Path (COK vk) a2 b2) (rs :: Path (OPK hk) c1 c2) (hs :: Path (COK vk) b1 c1) (is :: Path (COK vk) b2 c2). Sq (OPK hk) (COK vk) ps qs fs gs -> Sq (OPK hk) (COK vk) qs rs hs is -> Sq (OPK hk) (COK vk) ps rs (fs +++ hs) (gs +++ is) Source Comments #

vArr :: forall (j :: k) (k1 :: k) (fs :: Path (COK vk) j k1) (gs :: Path (COK vk) j k1). (DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1) => (fs ~> gs) -> Sq (OPK hk) (COK vk) ('Nil :: Path (OPK hk) j j) ('Nil :: Path (OPK hk) k1 k1) fs gs Source Comments #

vArr1 :: forall (j :: k) (k1 :: k) (f :: COK vk j k1) (g :: COK vk j k1). (DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1) => (f ~> g) -> Sq1 (OPK hk) (COK vk) (I :: OPK hk j j) (I :: OPK hk k1 k1) f g Source Comments #

(===) :: forall {h :: k} {b1 :: k} {i :: k} {b2 :: k} {j :: k} {k1 :: k} (ps :: Path (OPK hk) h b1) (qs :: Path (OPK hk) i b2) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) b1 b2) (rs :: Path (OPK hk) b1 j) (ss :: Path (OPK hk) b2 k1) (hs :: Path (COK vk) j k1). Sq (OPK hk) (COK vk) ps qs fs gs -> Sq (OPK hk) (COK vk) rs ss gs hs -> Sq (OPK hk) (COK vk) (ps +++ rs) (qs +++ ss) fs hs Source Comments #

(\\\\) :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1) r. ((DOb (OPK hk) (COK vk) h, DOb (OPK hk) (COK vk) i, DOb (OPK hk) (COK vk) j, DOb (OPK hk) (COK vk) k1, Ob ps, Ob qs, Ob fs, Ob gs) => r) -> Sq (OPK hk) (COK vk) ps qs fs gs -> r Source Comments #

Bicategory kk => Double (QKK kk :: k -> k -> Type) (COK kk :: k -> k -> Type) Source Comments #

The quintet construction. Create a double category of squares alpha :: ps +++ gs ~> fs +++ qs from a bicategory.

Instance details

Defined in Proarrow.Category.Double.Quintet

Associated Types

data Sq (QKK kk :: k -> k -> Type) (COK kk :: k -> k -> Type) (ps :: Path (QKK kk) h j) (qs :: Path (QKK kk) i k1) (fs :: Path (COK kk) h i) (gs :: Path (COK kk) j k1)
Instance details Defined in Proarrow.Category.Double.Quintet data Sq (QKK kk :: k -> k -> Type) (COK kk :: k -> k -> Type) (ps :: Path (QKK kk) h j) (qs :: Path (QKK kk) i k1) (fs :: Path (COK kk) h i) (gs :: Path (COK kk) j k1) where Q :: forall {k} (kk :: CAT k) (h :: k) (j :: k) (ps :: Path (QKK kk) h j) (i :: k) (k1 :: k) (qs :: Path (QKK kk) i k1) (fs :: Path (COK kk) h i) (gs :: Path (COK kk) j k1). (IsPath ps, IsPath qs, IsPath fs, IsPath gs) => Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs) -> Sq (QKK kk) (COK kk) ps qs fs gs
data Sq1 (QKK kk :: k -> k -> Type) (COK kk :: k -> k -> Type) (p :: QKK kk h j) (q :: QKK kk i k1) (f :: COK kk h i) (g :: COK kk j k1)
Instance details Defined in Proarrow.Category.Double.Quintet data Sq1 (QKK kk :: k -> k -> Type) (COK kk :: k -> k -> Type) (p :: QKK kk h j) (q :: QKK kk i k1) (f :: COK kk h i) (g :: COK kk j k1) where Q1 :: forall {k} (kk :: CAT k) (h :: k) (i :: k) (j :: k) (k1 :: k) (p :: QKK kk h j) (q :: QKK kk i k1) (f :: COK kk h i) (g :: COK kk j k1). (Ob0 kk h, Ob0 kk i, Ob0 kk j, Ob0 kk k1, Ob p, Ob q, Ob f, Ob g) => (O (UN ('QK :: kk h j -> QKK kk h j) p) (UN ('CO :: kk j k1 -> COK kk j k1) g) ~> O (UN ('CO :: kk h i -> COK kk h i) f) (UN ('QK :: kk i k1 -> QKK kk i k1) q)) -> Sq1 (QKK kk) (COK kk) p q f g

Methods

singleton :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (p :: QKK kk h j) (q :: QKK kk i k1) (f :: COK kk h i) (g :: COK kk j k1). (DOb (QKK kk) (COK kk) h, DOb (QKK kk) (COK kk) i, DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1, Ob p, Ob q, Ob f, Ob g) => Sq1 (QKK kk) (COK kk) p q f g -> Sq (QKK kk) (COK kk) (p '::: ('Nil :: Path (QKK kk) j j)) (q '::: ('Nil :: Path (QKK kk) k1 k1)) (f '::: ('Nil :: Path (COK kk) i i)) (g '::: ('Nil :: Path (COK kk) k1 k1)) Source Comments #

folded :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path (QKK kk) h j) (qs :: Path (QKK kk) i k1) (fs :: Path (COK kk) h i) (gs :: Path (COK kk) j k1). (DOb (QKK kk) (COK kk) h, DOb (QKK kk) (COK kk) i, DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1, Ob ps, Ob qs, Ob fs, Ob gs) => Sq (QKK kk) (COK kk) ps qs fs gs -> Sq1 (QKK kk) (COK kk) (Fold ps) (Fold qs) (Fold fs) (Fold gs) Source Comments #

object :: forall (k1 :: k). DOb (QKK kk) (COK kk) k1 => Sq (QKK kk) (COK kk) ('Nil :: Path (QKK kk) k1 k1) ('Nil :: Path (QKK kk) k1 k1) ('Nil :: Path (COK kk) k1 k1) ('Nil :: Path (COK kk) k1 k1) Source Comments #

hArr :: forall (j :: k) (k1 :: k) (ps :: Path (QKK kk) j k1) (qs :: Path (QKK kk) j k1). (DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) => (ps ~> qs) -> Sq (QKK kk) (COK kk) ps qs ('Nil :: Path (COK kk) j j) ('Nil :: Path (COK kk) k1 k1) Source Comments #

hArr1 :: forall (j :: k) (k1 :: k) (p :: QKK kk j k1) (q :: QKK kk j k1). (DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) => (p ~> q) -> Sq1 (QKK kk) (COK kk) p q (I :: COK kk j j) (I :: COK kk k1 k1) Source Comments #

(|||) :: forall {a1 :: k} {a2 :: k} {b1 :: k} {b2 :: k} {c1 :: k} {c2 :: k} (ps :: Path (QKK kk) a1 a2) (qs :: Path (QKK kk) b1 b2) (fs :: Path (COK kk) a1 b1) (gs :: Path (COK kk) a2 b2) (rs :: Path (QKK kk) c1 c2) (hs :: Path (COK kk) b1 c1) (is :: Path (COK kk) b2 c2). Sq (QKK kk) (COK kk) ps qs fs gs -> Sq (QKK kk) (COK kk) qs rs hs is -> Sq (QKK kk) (COK kk) ps rs (fs +++ hs) (gs +++ is) Source Comments #

vArr :: forall (j :: k) (k1 :: k) (fs :: Path (COK kk) j k1) (gs :: Path (COK kk) j k1). (DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) => (fs ~> gs) -> Sq (QKK kk) (COK kk) ('Nil :: Path (QKK kk) j j) ('Nil :: Path (QKK kk) k1 k1) fs gs Source Comments #

vArr1 :: forall (j :: k) (k1 :: k) (f :: COK kk j k1) (g :: COK kk j k1). (DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1) => (f ~> g) -> Sq1 (QKK kk) (COK kk) (I :: QKK kk j j) (I :: QKK kk k1 k1) f g Source Comments #

(===) :: forall {h :: k} {b1 :: k} {i :: k} {b2 :: k} {j :: k} {k1 :: k} (ps :: Path (QKK kk) h b1) (qs :: Path (QKK kk) i b2) (fs :: Path (COK kk) h i) (gs :: Path (COK kk) b1 b2) (rs :: Path (QKK kk) b1 j) (ss :: Path (QKK kk) b2 k1) (hs :: Path (COK kk) j k1). Sq (QKK kk) (COK kk) ps qs fs gs -> Sq (QKK kk) (COK kk) rs ss gs hs -> Sq (QKK kk) (COK kk) (ps +++ rs) (qs +++ ss) fs hs Source Comments #

(\\\\) :: forall (h :: k) (i :: k) (j :: k) (k1 :: k) (ps :: Path (QKK kk) h j) (qs :: Path (QKK kk) i k1) (fs :: Path (COK kk) h i) (gs :: Path (COK kk) j k1) r. ((DOb (QKK kk) (COK kk) h, DOb (QKK kk) (COK kk) i, DOb (QKK kk) (COK kk) j, DOb (QKK kk) (COK kk) k1, Ob ps, Ob qs, Ob fs, Ob gs) => r) -> Sq (QKK kk) (COK kk) ps qs fs gs -> r Source Comments #

type DOb (hk :: CAT k) (vk :: CAT k1) (k3 :: k2) = (Ob0 hk k3, Ob0 vk k3) Source Comments #

class Double hk vk => Equipment (hk :: k -> k -> Type) (vk :: k -> k -> Type) where Source Comments #

Associated Types

type Companion (hk :: k -> k -> Type) (vk :: k -> k -> Type) (f :: vk j k1) :: hk j k1 Source Comments #

type Conjoint (hk :: k -> k -> Type) (vk :: k -> k -> Type) (f :: vk j k1) :: hk k1 j Source Comments #

Methods

fromRight :: forall (j :: k) (k1 :: k) (f :: vk j k1). (DOb hk vk j, DOb hk vk k1, Ob f) => Sq hk vk ('Nil :: Path hk j j) (Companion hk vk f '::: ('Nil :: Path hk k1 k1)) ('Nil :: Path vk j j) (f '::: ('Nil :: Path vk k1 k1)) Source Comments #

toLeft :: forall (j :: k) (k1 :: k) (f :: vk j k1). (DOb hk vk j, DOb hk vk k1, Ob f) => Sq hk vk (Companion hk vk f '::: ('Nil :: Path hk k1 k1)) ('Nil :: Path hk k1 k1) (f '::: ('Nil :: Path vk k1 k1)) ('Nil :: Path vk k1 k1) Source Comments #

toRight :: forall (j :: k) (k1 :: k) (f :: vk j k1). (DOb hk vk j, DOb hk vk k1, Ob f) => Sq hk vk ('Nil :: Path hk j j) (Conjoint hk vk f '::: ('Nil :: Path hk j j)) (f '::: ('Nil :: Path vk k1 k1)) ('Nil :: Path vk j j) Source Comments #

fromLeft :: forall (j :: k) (k1 :: k) (f :: vk j k1). (DOb hk vk j, DOb hk vk k1, Ob f) => Sq hk vk (Conjoint hk vk f '::: ('Nil :: Path hk j j)) ('Nil :: Path hk k1 k1) ('Nil :: Path vk k1 k1) (f '::: ('Nil :: Path vk k1 k1)) Source Comments #

withComOb :: forall (j :: k) (k1 :: k) (f :: vk j k1) r. (DOb hk vk j, DOb hk vk k1, Ob f) => Obj f -> (Ob (Companion hk vk f) => r) -> r Source Comments #

withConOb :: forall (j :: k) (k1 :: k) (f :: vk j k1) r. (DOb hk vk j, DOb hk vk k1, Ob f) => Obj f -> (Ob (Conjoint hk vk f) => r) -> r Source Comments #

type UnOp (ps :: Path (OPK kk) j k1) = UN ('OP :: kk k1 j -> OPK kk j k1) (Fold ps) Source Comments #

type UnCo (fs :: Path (COK kk) j k1) = UN ('CO :: kk j k1 -> COK kk j k1) (Fold fs) Source Comments #

type CoSq (ps :: Path (OPK hk) h j) (qs :: Path (OPK hk) i k1) (fs :: Path (COK vk) h i) (gs :: Path (COK vk) j k1) = Sq (OPK hk) (COK vk) ps qs fs gs Source Comments #