Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.CategoryAsBi

Documentation

data PLAINK k (i :: k) (j :: k) Source Github #

Constructors

PLAIN

Instances

Instances details

CategoryOf k => Bicategory (PLAINK k :: k -> k -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

Methods

o :: forall {i :: k} (j :: k) (k0 :: k) (a :: PLAINK k j k0) (b :: PLAINK k j k0) (c :: PLAINK k i j) (d :: PLAINK k i j). (a ~> b) -> (c ~> d) -> O a c ~> O b d Source Github #

withOb2 :: forall {i :: k} {j :: k} {k0 :: k} (a :: PLAINK k j k0) (b :: PLAINK k i j) r. (Ob a, Ob b, Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob0 (PLAINK k) k0) => (Ob (O a b) => r) -> r Source Github #

withOb0s :: forall {j :: k} {k0 :: k} (a :: PLAINK k j k0) r. Ob a => ((Ob0 (PLAINK k) j, Ob0 (PLAINK k) k0) => r) -> r Source Github #

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

leftUnitor :: forall {i :: k} {j :: k} (a :: PLAINK k i j). (Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob a) => O (I :: PLAINK k j j) a ~> a Source Github #

leftUnitorInv :: forall {i :: k} {j :: k} (a :: PLAINK k i j). (Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob a) => a ~> O (I :: PLAINK k j j) a Source Github #

rightUnitor :: forall {i :: k} {j :: k} (a :: PLAINK k i j). (Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob a) => O a (I :: PLAINK k i i) ~> a Source Github #

rightUnitorInv :: forall {i :: k} {j :: k} (a :: PLAINK k i j). (Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob a) => a ~> O a (I :: PLAINK k i i) Source Github #

associator :: forall {h :: k} {i :: k} {j :: k} {k0 :: k} (a :: PLAINK k j k0) (b :: PLAINK k i j) (c :: PLAINK k h i). (Ob0 (PLAINK k) h, Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob0 (PLAINK k) k0, Ob a, Ob b, Ob c) => O (O a b) c ~> O a (O b c) Source Github #

associatorInv :: forall {h :: k} {i :: k} {j :: k} {k0 :: k} (a :: PLAINK k j k0) (b :: PLAINK k i j) (c :: PLAINK k h i). (Ob0 (PLAINK k) h, Ob0 (PLAINK k) i, Ob0 (PLAINK k) j, Ob0 (PLAINK k) k0, Ob a, Ob b, Ob c) => O a (O b c) ~> O (O a b) c Source Github #

(CategoryOf k, Ob i, Ob j) => CategoryOf (PLAINK k i j) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

Associated Types

type (~>)
Instance details Defined in Proarrow.Category.Bicategory.CategoryAsBi type (~>) = Category :: PLAINK k i j -> PLAINK k i j -> Type

(CategoryOf k, Ob i, Ob j) => Promonad (Category :: PLAINK k i j -> PLAINK k i j -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

Methods

id :: forall (a :: PLAINK k i j). Ob a => Category a a Source Github #

(.) :: forall (b :: PLAINK k i j) (c :: PLAINK k i j) (a :: PLAINK k i j). Category b c -> Category a b -> Category a c Source Github #

(CategoryOf k, Ob i, Ob j) => Profunctor (Category :: PLAINK k i j -> PLAINK k i j -> Type) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

Methods

dimap :: forall (c :: PLAINK k i j) (a :: PLAINK k i j) (b :: PLAINK k i j) (d :: PLAINK k i j). (c ~> a) -> (b ~> d) -> Category a b -> Category c d Source Github #

(\\) :: forall (a :: PLAINK k i j) (b :: PLAINK k i j) r. ((Ob a, Ob b) => r) -> Category a b -> r Source Github #

type Ob0 (PLAINK k2 :: k2 -> k2 -> Type) (a :: k1) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

type Ob0 (PLAINK k2 :: k2 -> k2 -> Type) (a :: k1) = Ob a

type I Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

type I = 'PLAIN :: PLAINK k i i

type O ('PLAIN :: PLAINK k1 j k2) ('PLAIN :: PLAINK k1 i j) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

type O ('PLAIN :: PLAINK k1 j k2) ('PLAIN :: PLAINK k1 i j) = 'PLAIN :: PLAINK k1 i k2

type (~>) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

type (~>) = Category :: PLAINK k i j -> PLAINK k i j -> Type

type Ob (a :: PLAINK k i j) Source Github #

Instance details

Defined in Proarrow.Category.Bicategory.CategoryAsBi

type Ob (a :: PLAINK k i j) = (a ~ ('PLAIN :: PLAINK k i j), Ob i, Ob j)

data Category (as :: PLAINK k i j) (bs :: PLAINK k i j) where Source Github #

Constructors

Id :: forall {k} (i :: k) (j :: k). (Ob i, Ob j) => Maybe (i ~> j) -> Category ('PLAIN :: PLAINK k i j) ('PLAIN :: PLAINK k i j)

Instances

Instances details

(CategoryOf k, Ob i, Ob j) => Promonad (Category :: PLAINK k i j -> PLAINK k i j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.CategoryAsBi Methods id :: forall (a :: PLAINK k i j). Ob a => Category a a Source Github # (.) :: forall (b :: PLAINK k i j) (c :: PLAINK k i j) (a :: PLAINK k i j). Category b c -> Category a b -> Category a c Source Github #
(CategoryOf k, Ob i, Ob j) => Profunctor (Category :: PLAINK k i j -> PLAINK k i j -> Type) Source Github #
Instance details Defined in Proarrow.Category.Bicategory.CategoryAsBi Methods dimap :: forall (c :: PLAINK k i j) (a :: PLAINK k i j) (b :: PLAINK k i j) (d :: PLAINK k i j). (c ~> a) -> (b ~> d) -> Category a b -> Category c d Source Github # (\\) :: forall (a :: PLAINK k i j) (b :: PLAINK k i j) r. ((Ob a, Ob b) => r) -> Category a b -> r Source Github #