Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Double.Quintet

Documentation

data QKK (kk :: k -> k1 -> Type) (i :: k) (j :: k1) Source Comments #

Constructors

QK (kk i j)

Instances

Instances details

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

Instance details

Defined in Proarrow.Category.Double.Quintet

Methods

o :: forall {k1 :: k} (i :: k) (j :: k) (a :: QKK kk i j) (b :: QKK kk i j) (c :: QKK kk j k1) (d :: QKK kk j k1). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Comments #

(\\\) :: forall (i :: k) (j :: k) (ps :: QKK kk i j) (qs :: QKK kk i j) r. ((Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob ps, Ob qs) => r) -> (ps ~> qs) -> r Source Comments #

leftUnitor :: forall (i :: k) (j :: k) (a :: QKK kk i j). Obj a -> O (I :: QKK kk i i) a ~> a Source Comments #

leftUnitorInv :: forall (i :: k) (j :: k) (a :: QKK kk i j). Obj a -> a ~> O (I :: QKK kk i i) a Source Comments #

rightUnitor :: forall (i :: k) (j :: k) (a :: QKK kk i j). Obj a -> O a (I :: QKK kk j j) ~> a Source Comments #

rightUnitorInv :: forall (i :: k) (j :: k) (a :: QKK kk i j). Obj a -> a ~> O a (I :: QKK kk j j) Source Comments #

associator :: forall {j1 :: k} {k1 :: k} (i :: k) (j2 :: k) (a :: QKK kk i j2) (b :: QKK kk j2 j1) (c :: QKK 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 :: QKK kk i j2) (b :: QKK kk j2 j1) (c :: QKK kk j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c 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 #

CategoryOf (kk i j) => CategoryOf (QKK kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Double.Quintet

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Double.Quintet type (~>) = Q2 :: QKK kk i j -> QKK kk i j -> Type

CategoryOf (kk i j) => Promonad (Q2 :: QKK kk i j -> QKK kk i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Double.Quintet

Methods

id :: forall (a :: QKK kk i j). Ob a => Q2 a a Source Comments #

(.) :: forall (b :: QKK kk i j) (c :: QKK kk i j) (a :: QKK kk i j). Q2 b c -> Q2 a b -> Q2 a c Source Comments #

CategoryOf (kk i j) => Profunctor (Q2 :: QKK kk i j -> QKK kk i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Double.Quintet

Methods

dimap :: forall (c :: QKK kk i j) (a :: QKK kk i j) (b :: QKK kk i j) (d :: QKK kk i j). (c ~> a) -> (b ~> d) -> Q2 a b -> Q2 c d Source Comments #

(\\) :: forall (a :: QKK kk i j) (b :: QKK kk i j) r. ((Ob a, Ob b) => r) -> Q2 a b -> r Source Comments #

type Ob0 (QKK kk :: k2 -> k2 -> Type) (k3 :: k1) Source Comments #

Instance details

Defined in Proarrow.Category.Double.Quintet

type Ob0 (QKK kk :: k2 -> k2 -> Type) (k3 :: k1) = Ob0 kk k3

type I Source Comments #

Instance details

Defined in Proarrow.Category.Double.Quintet

type I = 'QK (I :: kk i i)

type O (a :: QKK kk i1 i2) (b :: QKK kk i2 j) Source Comments #

Instance details

Defined in Proarrow.Category.Double.Quintet

type O (a :: QKK kk i1 i2) (b :: QKK kk i2 j) = 'QK (O (UN ('QK :: kk i1 i2 -> QKK kk i1 i2) a) (UN ('QK :: kk i2 j -> QKK kk i2 j) b))

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

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) 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 ('QK :: kk i j -> QKK kk i j) ('QK p :: QKK kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Double.Quintet

type UN ('QK :: kk i j -> QKK kk i j) ('QK p :: QKK kk i j) = p

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Double.Quintet

type (~>) = Q2 :: QKK kk i j -> QKK kk i j -> Type

type Ob (a :: QKK kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Double.Quintet

type Ob (a :: QKK kk i j) = (Is ('QK :: kk i j -> QKK kk i j) a, Ob (UN ('QK :: kk i j -> QKK kk i j) a))

data Q2 (a :: QKK kk i j) (b :: QKK kk i j) where Source Comments #

Constructors

Q2 :: forall {k} {k1} {kk :: k -> k1 -> Type} {i :: k} {j :: k1} (a1 :: kk i j) (b1 :: kk i j). (a1 ~> b1) -> Q2 ('QK a1) ('QK b1)

Instances

Instances details

CategoryOf (kk i j) => Promonad (Q2 :: QKK kk i j -> QKK kk i j -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Double.Quintet Methods id :: forall (a :: QKK kk i j). Ob a => Q2 a a Source Comments # (.) :: forall (b :: QKK kk i j) (c :: QKK kk i j) (a :: QKK kk i j). Q2 b c -> Q2 a b -> Q2 a c Source Comments #
CategoryOf (kk i j) => Profunctor (Q2 :: QKK kk i j -> QKK kk i j -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Double.Quintet Methods dimap :: forall (c :: QKK kk i j) (a :: QKK kk i j) (b :: QKK kk i j) (d :: QKK kk i j). (c ~> a) -> (b ~> d) -> Q2 a b -> Q2 c d Source Comments # (\\) :: forall (a :: QKK kk i j) (b :: QKK kk i j) r. ((Ob a, Ob b) => r) -> Q2 a b -> r Source Comments #

concatFoldQ :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k2). (Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k2) => SPath ps -> O (UN ('QK :: kk i j -> QKK kk i j) (Fold ps)) (UN ('QK :: kk j k2 -> QKK kk j k2) (Fold qs)) ~> UN ('QK :: kk i k2 -> QKK kk i k2) (Fold (ps +++ qs)) Source Comments #

splitFoldQ :: forall {k1} {kk :: k1 -> k1 -> Type} {i :: k1} {j :: k1} {k2 :: k1} {ps :: Path (QKK kk) i j} (qs :: Path (QKK kk) j k2). (Bicategory kk, Ob qs, Ob0 kk i, Ob0 kk j, Ob0 kk k2) => SPath ps -> UN ('QK :: kk i k2 -> QKK kk i k2) (Fold (ps +++ qs)) ~> O (UN ('QK :: kk i j -> QKK kk i j) (Fold ps)) (UN ('QK :: kk j k2 -> QKK kk j k2) (Fold qs)) Source Comments #

type Quintet (ps :: Path (QKK kk) h j) = Sq (QKK kk) (COK kk) ps Source Comments #

type Quintet1 (p :: QKK kk h j) = Sq1 (QKK kk) (COK kk) p Source Comments #