Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Bicategory.MonoidalAsBi

Documentation

newtype MonK k (i :: ()) (j :: ()) Source Comments #

Constructors

MK k

Instances

Instances details

Monoidal k => Bicategory (MonK k :: () -> () -> Type) Source Comments #

A monoidal category as a bicategory.

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

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

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

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

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

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

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

associator :: forall {j1 :: ()} {k1 :: ()} (i :: ()) (j2 :: ()) (a :: MonK k i j2) (b :: MonK k j2 j1) (c :: MonK k j1 k1). Obj a -> Obj b -> Obj c -> O (O a b) c ~> O a (O b c) Source Comments #

associatorInv :: forall {j1 :: ()} {k1 :: ()} (i :: ()) (j2 :: ()) (a :: MonK k i j2) (b :: MonK k j2 j1) (c :: MonK k j1 k1). Obj a -> Obj b -> Obj c -> O a (O b c) ~> O (O a b) c Source Comments #

(Functor j, Functor f) => LeftKanExtension ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Kan

Associated Types

type Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e)
Instance details Defined in Proarrow.Category.Bicategory.Kan type Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) = 'MK (HaskLan j f) :: MonK (Type -> Type) d e

Methods

lan :: ('MK f :: MonK (Type -> Type) c e) ~> O ('MK j :: MonK (Type -> Type) c d) (Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e)) Source Comments #

lanUniv :: forall (g :: MonK (Type -> Type) d e). Ob g => (('MK f :: MonK (Type -> Type) c e) ~> O ('MK j :: MonK (Type -> Type) c d) g) -> Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) ~> g Source Comments #

(Functor j, Functor f) => RightKanExtension ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Kan

Associated Types

type Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e)
Instance details Defined in Proarrow.Category.Bicategory.Kan type Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) = 'MK (HaskRan j f) :: MonK (Type -> Type) d e

Methods

ran :: O ('MK j :: MonK (Type -> Type) c d) (Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e)) ~> ('MK f :: MonK (Type -> Type) c e) Source Comments #

ranUniv :: forall (g :: MonK (Type -> Type) d e). Ob g => (O ('MK j :: MonK (Type -> Type) c d) g ~> ('MK f :: MonK (Type -> Type) c e)) -> g ~> Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) Source Comments #

Comonoid m => Comonad ('MK m :: MonK k a a) Source Comments #

Comonoids in a monoidal category are comonads when the monoidal category is seen as a bicategory.

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

epsilon :: ('MK m :: MonK k a a) ~> (I :: MonK k a a) Source Comments #

delta :: ('MK m :: MonK k a a) ~> O ('MK m :: MonK k a a) ('MK m :: MonK k a a) Source Comments #

Monoid m => Monad ('MK m :: MonK k a a) Source Comments #

Monoids in a monoidal category are monads when the monoidal category is seen as a bicategory.

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

eta :: (I :: MonK k a a) ~> ('MK m :: MonK k a a) Source Comments #

mu :: O ('MK m :: MonK k a a) ('MK m :: MonK k a a) ~> ('MK m :: MonK k a a) Source Comments #

CategoryOf k => CategoryOf (MonK k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Associated Types

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

CategoryOf k => Promonad (Mon2 :: MonK k i j -> MonK k i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

id :: forall (a :: MonK k i j). Ob a => Mon2 a a Source Comments #

(.) :: forall (b :: MonK k i j) (c :: MonK k i j) (a :: MonK k i j). Mon2 b c -> Mon2 a b -> Mon2 a c Source Comments #

CategoryOf k => Profunctor (Mon2 :: MonK k i j -> MonK k i j -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

dimap :: forall (c :: MonK k i j) (a :: MonK k i j) (b :: MonK k i j) (d :: MonK k i j). (c ~> a) -> (b ~> d) -> Mon2 a b -> Mon2 c d Source Comments #

(\\) :: forall (a :: MonK k i j) (b :: MonK k i j) r. ((Ob a, Ob b) => r) -> Mon2 a b -> r Source Comments #

type Ob0 (MonK k :: () -> () -> Type) (j :: k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Ob0 (MonK k :: () -> () -> Type) (j :: k1) = Any j

type Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Kan

type Lan ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) = 'MK (HaskLan j f) :: MonK (Type -> Type) d e

type Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.Kan

type Ran ('MK j :: MonK (Type -> Type) c d) ('MK f :: MonK (Type -> Type) c e) = 'MK (HaskRan j f) :: MonK (Type -> Type) d e

type I Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type I = 'MK (Unit :: k) :: MonK k i i

type O ('MK a :: MonK k i j) ('MK b :: MonK k j k1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type O ('MK a :: MonK k i j) ('MK b :: MonK k j k1) = 'MK (b ** a) :: MonK k i k1

type Arr (MonK Type) ('CK a :: CATK k exta) ('CK b :: CATK k extb) Source Comments #

Instance details

Defined in Proarrow.Category.Enriched

type Arr (MonK Type) ('CK a :: CATK k exta) ('CK b :: CATK k extb) = 'MK (a ~> b) :: MonK Type exta extb

type Arr (MonK (PRO k k) :: () -> () -> Type) ('BIPARA a :: BIPARAK k exta) ('BIPARA b :: BIPARAK k extb) Source Comments #

Instance details

Defined in Proarrow.Category.Enriched.Bipara

type Arr (MonK (PRO k k) :: () -> () -> Type) ('BIPARA a :: BIPARAK k exta) ('BIPARA b :: BIPARAK k extb) = 'MK (Bipara a b) :: MonK (k -> k -> Type) exta extb

type UN ('MK :: j1 -> MonK j1 i j2) ('MK k :: MonK j1 i j2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type UN ('MK :: j1 -> MonK j1 i j2) ('MK k :: MonK j1 i j2) = k

type (~>) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type (~>) = Mon2 :: MonK k i j -> MonK k i j -> Type

type Ob (a :: MonK k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Ob (a :: MonK k i j) = (Is ('MK :: k -> MonK k i j) a, Ob (UN ('MK :: k -> MonK k i j) a))

data Mon2 (a :: MonK k i j) (b :: MonK k i j) where Source Comments #

Constructors

Mon2 :: forall {k} {i :: ()} {j :: ()} (a1 :: k) (b1 :: k). (a1 ~> b1) -> Mon2 ('MK a1 :: MonK k i j) ('MK b1 :: MonK k i j)

Instances

Instances details

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