proarrow-0: Category theory with a central role for profunctors
Safe HaskellNone
LanguageHaskell2010

Proarrow.Category.Bicategory.Co

Documentation

newtype COK (kk :: CAT k) (j :: k) (k1 :: k) Source Comments #

Constructors

CO (kk j k1) 

Instances

Instances details
Bicategory kk => Bicategory (COK kk :: k -> k -> Type) Source Comments #

Create a dual of a bicategory by reversing the 2-cells.

Instance details

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 # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Ran j2 f)

Methods

lan :: 'CO f ~> O ('CO j2) (Lan ('CO j2) ('CO f)) Source Comments #

lanUniv :: forall (g :: COK kk d e). Ob g => ('CO f ~> O ('CO j2) g) -> Lan ('CO j2) ('CO f) ~> g Source Comments #

RightKanLift j f => LeftKanLift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Rift j f)

Methods

lift :: 'CO f ~> O (Lift ('CO j) ('CO f)) ('CO j) Source Comments #

liftUniv :: forall (g :: COK kk e d). Ob g => ('CO f ~> O g ('CO j)) -> Lift ('CO j) ('CO f) ~> g Source Comments #

LeftKanExtension j2 f => RightKanExtension ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Lan j2 f)

Methods

ran :: O ('CO j2) (Ran ('CO j2) ('CO f)) ~> 'CO f Source Comments #

ranUniv :: forall (g :: COK kk d e). Ob g => (O ('CO j2) g ~> 'CO f) -> g ~> Ran ('CO j2) ('CO f) Source Comments #

LeftKanLift j f => RightKanLift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Lift j f)

Methods

rift :: O (Rift ('CO j) ('CO f)) ('CO j) ~> 'CO f Source Comments #

riftUniv :: forall (g :: COK kk e d). Ob g => (O g ('CO j) ~> 'CO f) -> g ~> Rift ('CO j) ('CO f) Source Comments #

Monad m => Comonad ('CO m :: COK kk a a) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

epsilon :: 'CO m ~> (I :: COK kk a a) Source Comments #

delta :: 'CO m ~> O ('CO m) ('CO m) Source Comments #

Comonad m => Monad ('CO m :: COK kk a a) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

eta :: (I :: COK kk a a) ~> 'CO m Source Comments #

mu :: O ('CO m) ('CO m) ~> 'CO m Source Comments #

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
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
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 #

CategoryOf (kk j k2) => CategoryOf (COK kk j k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Associated Types

type (~>) 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type (~>) = Co :: COK kk j k2 -> COK kk j k2 -> Type
CategoryOf (kk j k2) => Promonad (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

id :: forall (a :: COK kk j k2). Ob a => Co a a Source Comments #

(.) :: forall (b :: COK kk j k2) (c :: COK kk j k2) (a :: COK kk j k2). Co b c -> Co a b -> Co a c Source Comments #

CategoryOf (kk j k2) => Profunctor (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

dimap :: forall (c :: COK kk j k2) (a :: COK kk j k2) (b :: COK kk j k2) (d :: COK kk j k2). (c ~> a) -> (b ~> d) -> Co a b -> Co c d Source Comments #

(\\) :: forall (a :: COK kk j k2) (b :: COK kk j k2) r. ((Ob a, Ob b) => r) -> Co a b -> r Source Comments #

type Ob0 (COK kk :: k2 -> k2 -> Type) (k3 :: k1) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Ob0 (COK kk :: k2 -> k2 -> Type) (k3 :: k1) = Ob0 kk k3
type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Lan ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Ran j2 f)
type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Lift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Rift j f)
type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Ran ('CO j2 :: COK kk j1 d) ('CO f :: COK kk j1 e) = 'CO (Lan j2 f)
type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Rift ('CO j :: COK kk d k2) ('CO f :: COK kk e k2) = 'CO (Lift j f)
type I Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type I = 'CO (I :: kk i i)
type O (a :: COK kk j1 j2) (b :: COK kk j2 k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type O (a :: COK kk j1 j2) (b :: COK kk j2 k2) = 'CO (O (UN ('CO :: kk j1 j2 -> COK kk j1 j2) a) (UN ('CO :: kk j2 k2 -> COK kk j2 k2) b))
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 # 
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
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 # 
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
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 # 
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
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 # 
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
type UN ('CO :: kk j k2 -> COK kk j k2) ('CO k3 :: COK kk j k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type UN ('CO :: kk j k2 -> COK kk j k2) ('CO k3 :: COK kk j k2) = k3
type (~>) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type (~>) = Co :: COK kk j k2 -> COK kk j k2 -> Type
type Ob (a :: COK kk j k2) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

type Ob (a :: COK kk j k2) = (Is ('CO :: kk j k2 -> COK kk j k2) a, Ob (UN ('CO :: kk j k2 -> COK kk j k2) a))

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

Instances details
CategoryOf (kk j k2) => Promonad (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

id :: forall (a :: COK kk j k2). Ob a => Co a a Source Comments #

(.) :: forall (b :: COK kk j k2) (c :: COK kk j k2) (a :: COK kk j k2). Co b c -> Co a b -> Co a c Source Comments #

CategoryOf (kk j k2) => Profunctor (Co :: COK kk j k2 -> COK kk j k2 -> Type) Source Comments # 
Instance details

Defined in Proarrow.Category.Bicategory.Co

Methods

dimap :: forall (c :: COK kk j k2) (a :: COK kk j k2) (b :: COK kk j k2) (d :: COK kk j k2). (c ~> a) -> (b ~> d) -> Co a b -> Co c d Source Comments #

(\\) :: forall (a :: COK kk j k2) (b :: COK kk j k2) r. ((Ob a, Ob b) => r) -> Co a b -> r Source Comments #

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 #