Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Equipment.BiAsEquipment

Documentation

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

Constructors

WK (kk i j)

Instances

Instances details

Bicategory kk => Bicategory (WKK kk :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

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

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

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

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

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

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

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

associator :: forall {h :: s} {i :: s} {j :: s} {k :: s} (a :: WKK kk j k) (b :: WKK kk i j) (c :: WKK kk h i). (Ob0 (WKK kk) h, Ob0 (WKK kk) i, Ob0 (WKK kk) j, Ob0 (WKK 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 :: WKK kk j k) (b :: WKK kk i j) (c :: WKK kk h i). (Ob0 (WKK kk) h, Ob0 (WKK kk) i, Ob0 (WKK kk) j, Ob0 (WKK kk) k, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Comments #

Bicategory kk => Equipment (WKK kk :: s -> s -> Type) (DiscreteK (Ob0' kk :: s -> Constraint) :: s -> s -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

mapConjoint :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j k). (f ~> g) -> Conjoint (WKK kk) g ~> Conjoint (WKK kk) f Source Comments #

conjToId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => Conjoint (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) ~> (I :: WKK kk k k) Source Comments #

conjFromId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => (I :: WKK kk k k) ~> Conjoint (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) Source Comments #

conjToCompose :: forall {k1 :: s} {j :: s} {k2 :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k2) (g :: DiscreteK (Ob0' kk :: s -> Constraint) k1 j). Obj f -> Obj g -> Conjoint (WKK kk) (O f g) ~> O (Conjoint (WKK kk) g) (Conjoint (WKK kk) f) Source Comments #

conjFromCompose :: forall {j1 :: s} {j2 :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j2 k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j1 j2). Obj f -> Obj g -> O (Conjoint (WKK kk) g) (Conjoint (WKK kk) f) ~> Conjoint (WKK kk) (O f g) Source Comments #

comConUnit :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k). Obj f -> (I :: WKK kk j j) ~> O (Conjoint (WKK kk) f) (Companion (WKK kk) f) Source Comments #

comConCounit :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k). Obj f -> O (Companion (WKK kk) f) (Conjoint (WKK kk) f) ~> (I :: WKK kk k k) Source Comments #

Bicategory kk => HasCompanions (WKK kk :: s -> s -> Type) (DiscreteK (Ob0' kk :: s -> Constraint) :: s -> s -> Type) Source Comments #

A bicategory as a proarrow equipment with only identity arrows vertically.

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

mapCompanion :: forall {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j k). (f ~> g) -> Companion (WKK kk) f ~> Companion (WKK kk) g Source Comments #

compToId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => Companion (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) ~> (I :: WKK kk k k) Source Comments #

compFromId :: forall (k :: s). Ob0 (DiscreteK (Ob0' kk :: s -> Constraint)) k => (I :: WKK kk k k) ~> Companion (WKK kk) (I :: DiscreteK (Ob0' kk :: s -> Constraint) k k) Source Comments #

compToCompose :: forall {i :: s} {j :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) i j). Obj f -> Obj g -> Companion (WKK kk) (O f g) ~> O (Companion (WKK kk) f) (Companion (WKK kk) g) Source Comments #

compFromCompose :: forall {j1 :: s} {j2 :: s} {k :: s} (f :: DiscreteK (Ob0' kk :: s -> Constraint) j2 k) (g :: DiscreteK (Ob0' kk :: s -> Constraint) j1 j2). Obj f -> Obj g -> O (Companion (WKK kk) f) (Companion (WKK kk) g) ~> Companion (WKK kk) (O f g) Source Comments #

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

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Equipment.BiAsEquipment type (~>) = W :: WKK kk i j -> WKK kk i j -> Type

CategoryOf (kk i j) => Promonad (W :: WKK kk i j -> WKK kk i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

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

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

CategoryOf (kk i j) => Profunctor (W :: WKK kk i j -> WKK kk i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

Methods

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

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

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

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

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

type Companion (WKK kk :: s -> s -> Type) ('DK :: DiscreteK (Ob0' kk :: s -> Constraint) j j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

type Companion (WKK kk :: s -> s -> Type) ('DK :: DiscreteK (Ob0' kk :: s -> Constraint) j j) = 'WK (I :: kk j j)

type Conjoint (WKK kk :: s -> s -> Type) ('DK :: DiscreteK (Ob0' kk :: s -> Constraint) j j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

type Conjoint (WKK kk :: s -> s -> Type) ('DK :: DiscreteK (Ob0' kk :: s -> Constraint) j j) = 'WK (I :: kk j j)

type I Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

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

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

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

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

type UN ('WK :: kk i j -> WKK kk i j) ('WK p :: WKK kk i j) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

type UN ('WK :: kk i j -> WKK kk i j) ('WK p :: WKK kk i j) = p

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

type (~>) = W :: WKK kk i j -> WKK kk i j -> Type

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

Instance details

Defined in Proarrow.Category.Equipment.BiAsEquipment

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

data W (a :: WKK kk i j) (b :: WKK kk i j) where Source Comments #

Constructors

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

Instances

Instances details

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