Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Equipment.Quintet

Synopsis

data QKK (kk :: k -> k1 -> Type) (i :: k) (j :: k1) = QK (kk i j)
type QuintetSq (f :: kk a b) (g :: kk a c) (h :: kk b d) (k1 :: kk c d) = Sq '('QK f, h) '('QK k1, g)
data Q2 (a :: QKK kk i j) (b :: QKK kk i j) where
- 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)
type BiParaSq (a :: k) (b :: k) (p :: k) (q :: k) = QuintetSq ('MK p :: MonK k '() '()) ('MK b :: MonK k '() '()) ('MK a :: MonK k '() '()) ('MK q :: MonK k '() '())
bipara :: forall {k} (p :: k) (q :: k) (a :: k) (b :: k). (Ob p, Ob q, Ob a, Ob b) => ((a ** p) ~> (q ** b)) -> BiParaSq a b p q
reparam :: forall {k} (a :: k) (b :: k). Monoidal k => (a ~> b) -> BiParaSq a b (Unit :: k) (Unit :: k)

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 :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Quintet

Methods

iObj :: forall (i :: s). Ob0 (QKK kk) i => Obj (I :: QKK kk i i) Source Comments #

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

(\\\) :: forall (i :: s) (j :: s) (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 :: s} {j :: s} (a :: QKK kk i j). (Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob a) => O (I :: QKK kk j j) a ~> a Source Comments #

leftUnitorInv :: forall {i :: s} {j :: s} (a :: QKK kk i j). (Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob a) => a ~> O (I :: QKK kk j j) a Source Comments #

rightUnitor :: forall {i :: s} {j :: s} (a :: QKK kk i j). (Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob a) => O a (I :: QKK kk i i) ~> a Source Comments #

rightUnitorInv :: forall {i :: s} {j :: s} (a :: QKK kk i j). (Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob a) => a ~> O a (I :: QKK kk i i) Source Comments #

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: QKK kk j k) (b :: QKK kk i j) (c :: QKK kk h i). (Ob0 (QKK kk) h, Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob0 (QKK kk) k, Ob a, Ob b, Ob c) => O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: QKK kk j k) (b :: QKK kk i j) (c :: QKK kk h i). (Ob0 (QKK kk) h, Ob0 (QKK kk) i, Ob0 (QKK kk) j, Ob0 (QKK kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

Bicategory kk => HasCompanions (QKK kk :: c -> c -> Type) (kk :: CAT c) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Quintet

Methods

mapCompanion :: forall {j :: c} {k :: c} (f :: kk j k) (g :: kk j k). (f ~> g) -> Companion (QKK kk) f ~> Companion (QKK kk) g Source Comments #

compToId :: forall (k :: c). Ob0 kk k => Companion (QKK kk) (I :: kk k k) ~> (I :: QKK kk k k) Source Comments #

compFromId :: forall (k :: c). Ob0 kk k => (I :: QKK kk k k) ~> Companion (QKK kk) (I :: kk k k) Source Comments #

compToCompose :: forall {i :: c} {j :: c} {k :: c} (f :: kk j k) (g :: kk i j). Obj f -> Obj g -> Companion (QKK kk) (O f g) ~> O (Companion (QKK kk) f) (Companion (QKK kk) g) Source Comments #

compFromCompose :: forall {j1 :: c} {j2 :: c} {k :: c} (f :: kk j2 k) (g :: kk j1 j2). Obj f -> Obj g -> O (Companion (QKK kk) f) (Companion (QKK kk) g) ~> Companion (QKK kk) (O f g) Source Comments #

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

Instance details

Defined in Proarrow.Category.Equipment.Quintet

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Equipment.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.Equipment.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.Equipment.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 Companion (QKK kk :: c -> c -> Type) (f :: kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Quintet

type Companion (QKK kk :: c -> c -> Type) (f :: kk i j) = 'QK f

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

Instance details

Defined in Proarrow.Category.Equipment.Quintet

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

type I Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Quintet

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

type O (a :: QKK kk j1 j2) (b :: QKK kk i j1) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.Quintet

type O (a :: QKK kk j1 j2) (b :: QKK kk i j1) = 'QK (O (UN ('QK :: kk j1 j2 -> QKK kk j1 j2) a) (UN ('QK :: kk i j1 -> QKK kk i j1) b))

type UN ('QK :: kk i j -> QKK kk i j) ('QK p :: QKK kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.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.Equipment.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.Equipment.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))

type QuintetSq (f :: kk a b) (g :: kk a c) (h :: kk b d) (k1 :: kk c d) = Sq '('QK f, h) '('QK k1, g) Source Comments #

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.Equipment.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.Equipment.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 BiParaSq (a :: k) (b :: k) (p :: k) (q :: k) = QuintetSq ('MK p :: MonK k '() '()) ('MK b :: MonK k '() '()) ('MK a :: MonK k '() '()) ('MK q :: MonK k '() '()) Source Comments #

BiPara as a quintet construction.

bipara :: forall {k} (p :: k) (q :: k) (a :: k) (b :: k). (Ob p, Ob q, Ob a, Ob b) => ((a ** p) ~> (q ** b)) -> BiParaSq a b p q Source Comments #

reparam :: forall {k} (a :: k) (b :: k). Monoidal k => (a ~> b) -> BiParaSq a b (Unit :: k) (Unit :: k) Source Comments #