Safe Haskell | None |
---|---|
Language | Haskell2010 |
Proarrow.Category.Bicategory.Co
Documentation
newtype COK (kk :: CAT k) (j :: k) (k1 :: k) Source Comments #
Constructors
CO (kk j k1) |
Instances
Bicategory kk => Bicategory (COK kk :: k -> k -> Type) Source Comments # | Create a dual of a bicategory by reversing the 2-cells. | ||||||||
Defined in Proarrow.Category.Bicategory.Co Methods o :: forall {k1 :: k} (i :: k) (j :: k) (a :: COK kk i j) (b :: COK kk i j) (c :: COK kk j k1) (d :: COK kk j k1). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments # (\\\) :: forall (i :: k) (j :: k) (ps :: COK kk i j) (qs :: COK kk i j) r. ((Ob0 (COK kk) i, Ob0 (COK kk) j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments # leftUnitor :: forall (i :: k) (j :: k) (a :: COK kk i j). Obj a -> O (I :: COK kk i i) a ~> a Source Comments # leftUnitorInv :: forall (i :: k) (j :: k) (a :: COK kk i j). Obj a -> a ~> O (I :: COK kk i i) a Source Comments # rightUnitor :: forall (i :: k) (j :: k) (a :: COK kk i j). Obj a -> O a (I :: COK kk j j) ~> a Source Comments # rightUnitorInv :: forall (i :: k) (j :: k) (a :: COK kk i j). Obj a -> a ~> O a (I :: COK kk j j) Source Comments # associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: COK kk i j2) (b :: COK kk j2 j1) (c :: COK kk j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) Source Comments # associatorInv :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: COK kk i j2) (b :: COK kk j2 j1) (c :: COK kk j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c Source Comments # | |||||||||
RightKanExtension j2 f => LeftKanExtension ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments # | |||||||||
RightKanLift j f => LeftKanLift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments # | |||||||||
LeftKanExtension j2 f => RightKanExtension ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments # | |||||||||
LeftKanLift j f => RightKanLift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments # | |||||||||
Monad m => Comonad ('CO m :: COK kk a a) Source Comments # | |||||||||
Comonad m => Monad ('CO m :: COK kk a a) Source Comments # | |||||||||
Double hk vk => Double (OPK hk :: k -> k -> Type) (COK vk :: k -> k -> Type) Source Comments # | |||||||||
Defined in Proarrow.Category.Double Associated Types
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 | ||||||||
Defined in Proarrow.Category.Double.Quintet Associated Types
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 # | |||||||||
CategoryOf (kk j k2) => CategoryOf (COK kk j k2) Source Comments # | |||||||||
Defined in Proarrow.Category.Bicategory.Co | |||||||||
CategoryOf (kk j k2) => Promonad (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments # | |||||||||
CategoryOf (kk j k2) => Profunctor (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments # | |||||||||
Defined in Proarrow.Category.Bicategory.Co | |||||||||
type Ob0 (COK kk :: k2 -> k2 -> Type) (k3 :: k1) Source Comments # | |||||||||
Defined in Proarrow.Category.Bicategory.Co | |||||||||
type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments # | |||||||||
type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments # | |||||||||
type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments # | |||||||||
type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments # | |||||||||
type I Source Comments # | |||||||||
Defined in Proarrow.Category.Bicategory.Co | |||||||||
type O (a :: COK kk j1 j2) (b :: COK kk j2 k2) Source Comments # | |||||||||
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) Source Comments # | |||||||||
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
| |||||||||
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) Source Comments # | |||||||||
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
| |||||||||
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) Source Comments # | |||||||||
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
| |||||||||
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) Source Comments # | |||||||||
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
| |||||||||
type UN ('CO :: kk j k2 -> COK kk j k2) ('CO k3 :: COK kk j k2) Source Comments # | |||||||||
type (~>) Source Comments # | |||||||||
type Ob (a :: COK kk j k2) Source Comments # | |||||||||
data Co (a :: COK kk j k1) (b :: COK kk j k1) where Source Comments #
Constructors
Co :: forall {k} {kk :: CAT k} {j :: k} {k1 :: k} (b1 :: kk j k1) (a1 :: kk j k1). (b1 ~> a1) -> Co ('CO a1) ('CO b1) |
Instances
CategoryOf (kk j k2) => Promonad (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments # | |
CategoryOf (kk j k2) => Profunctor (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments # | |
Defined in Proarrow.Category.Bicategory.Co |
concatFoldCo :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k2). (Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k2) => SPath ps -> O (UN ('CO :: kk i j -> COK kk i j) (Fold ps)) (UN ('CO :: kk j k2 -> COK kk j k2) (Fold qs)) ~> UN ('CO :: kk i k2 -> COK kk i k2) (Fold (ps +++ qs)) Source Comments #
splitFoldCo :: forall {k1} {kk :: CAT k1} {i :: k1} {j :: k1} {k2 :: k1} {ps :: Path (COK kk) i j} (qs :: Path (COK kk) j k2). (Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k2) => SPath ps -> UN ('CO :: kk i k2 -> COK kk i k2) (Fold (ps +++ qs)) ~> O (UN ('CO :: kk i j -> COK kk i j) (Fold ps)) (UN ('CO :: kk j k2 -> COK kk j k2) (Fold qs)) Source Comments #