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

iObj :: forall (i :: ()). Ob0 (MonK k) i => Obj (I :: MonK k i i) Source Comments #

o :: forall {i :: ()} (j :: ()) (k0 :: ()) (a :: MonK k j k0) (b :: MonK k j k0) (c :: MonK k i j) (d :: MonK k i j). (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). (Ob0 (MonK k) i, Ob0 (MonK k) j, Ob a) => O (I :: MonK k j j) a ~> a Source Comments #

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

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

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

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

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

(Coclosed k, Ob (q <~~ p), Ob p, Ob q) => LeftKanExtension ('MK p :: MonK k c d) ('MK q :: MonK k c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Associated Types

type Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e)
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e) = 'MK (q <~~ p) :: MonK k d e

Methods

lan :: ('MK q :: MonK k c e) ~> O (Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e)) ('MK p :: MonK k c d) Source Comments #

lanUniv :: forall (g :: MonK k d e). Ob g => (('MK q :: MonK k c e) ~> O g ('MK p :: MonK k c d)) -> Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e) ~> g Source Comments #

(Coclosed k, SymMonoidal k, Ob (q <~~ p), Ob p, Ob q) => LeftKanLift ('MK p :: MonK k d c) ('MK q :: MonK k e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Associated Types

type Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c)
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c) = 'MK (q <~~ p) :: MonK k e d

Methods

lift :: ('MK q :: MonK k e c) ~> O ('MK p :: MonK k d c) (Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c)) Source Comments #

liftUniv :: forall (g :: MonK k e d). Ob g => (('MK q :: MonK k e c) ~> O ('MK p :: MonK k d c) g) -> Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c) ~> g Source Comments #

(Closed k, Ob (p ~~> q), Ob p, Ob q) => RightKanExtension ('MK p :: MonK k c d) ('MK q :: MonK k c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Associated Types

type Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e)
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e) = 'MK (p ~~> q) :: MonK k d e

Methods

ran :: O (Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e)) ('MK p :: MonK k c d) ~> ('MK q :: MonK k c e) Source Comments #

ranUniv :: forall (g :: MonK k d e). Ob g => (O g ('MK p :: MonK k c d) ~> ('MK q :: MonK k c e)) -> g ~> Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e) Source Comments #

(Closed k, SymMonoidal k, Ob (p ~~> q), Ob p, Ob q) => RightKanLift ('MK p :: MonK k d c) ('MK q :: MonK k e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Associated Types

type Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c)
Instance details Defined in Proarrow.Category.Bicategory.MonoidalAsBi type Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c) = 'MK (p ~~> q) :: MonK k e d

Methods

rift :: O ('MK p :: MonK k d c) (Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c)) ~> ('MK q :: MonK k e c) Source Comments #

riftUniv :: forall (g :: MonK k e d). Ob g => (O ('MK p :: MonK k d c) g ~> ('MK q :: MonK k e c)) -> g ~> Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c) Source Comments #

(Monoidal k, Ob j) => HasColimits (MonK k :: () -> () -> Type) ('MK j :: MonK k a i) '() Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

colimit :: forall (d :: MonK k i '()). Ob d => O (Companion (MonK k) d) ('MK j :: MonK k a i) ~> Companion (MonK k) (Colimit ('MK j :: MonK k a i) d) Source Comments #

colimitUniv :: forall (d :: MonK k i '()) (p :: MonK k a '()). (Ob d, Ob p) => (O (Companion (MonK k) d) ('MK j :: MonK k a i) ~> Companion (MonK k) p) -> Colimit ('MK j :: MonK k a i) d ~> p Source Comments #

(Closed k, Ob j) => HasLimits (MonK k :: () -> () -> Type) ('MK j :: MonK k i a) '() Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

limitObj :: forall (d :: MonK k i '()). Ob d => Obj (Limit ('MK j :: MonK k i a) d) Source Comments #

limit :: forall (d :: MonK k i '()). Ob d => O (Companion (MonK k) (Limit ('MK j :: MonK k i a) d)) ('MK j :: MonK k i a) ~> Companion (MonK k) d Source Comments #

limitUniv :: forall (d :: MonK k i '()) (p :: MonK k a '()). (Ob d, Ob p) => (O (Companion (MonK k) p) ('MK j :: MonK k i a) ~> Companion (MonK k) d) -> p ~> Limit ('MK j :: MonK k i a) d Source Comments #

(CompactClosed k, Ob a, b ~ Dual a) => Adjunction ('MK a :: MonK k c d) ('MK b :: MonK k d c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

unit :: (I :: MonK k c c) ~> O ('MK b :: MonK k d c) ('MK a :: MonK k c d) Source Comments #

counit :: O ('MK a :: MonK k c d) ('MK b :: MonK k d c) ~> (I :: MonK k d d) 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 #

CompactClosed k => Equipment (MonK k :: () -> () -> Type) (MonK k :: () -> () -> Type) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

mapConjoint :: forall {j :: ()} {k0 :: ()} (f :: MonK k j k0) (g :: MonK k j k0). (f ~> g) -> Conjoint (MonK k) g ~> Conjoint (MonK k) f Source Comments #

conjToId :: forall (k0 :: ()). Ob0 (MonK k) k0 => Conjoint (MonK k) (I :: MonK k k k) ~> (I :: MonK k k k) Source Comments #

conjFromId :: forall (k0 :: ()). Ob0 (MonK k) k0 => (I :: MonK k k k) ~> Conjoint (MonK k) (I :: MonK k k k) Source Comments #

conjToCompose :: forall {k1 :: ()} {j :: ()} {k2 :: ()} (f :: MonK k j k2) (g :: MonK k k1 j). Obj f -> Obj g -> Conjoint (MonK k) (O f g) ~> O (Conjoint (MonK k) g) (Conjoint (MonK k) f) Source Comments #

conjFromCompose :: forall {j1 :: ()} {j2 :: ()} {k0 :: ()} (f :: MonK k j2 k0) (g :: MonK k j1 j2). Obj f -> Obj g -> O (Conjoint (MonK k) g) (Conjoint (MonK k) f) ~> Conjoint (MonK k) (O f g) Source Comments #

comConUnit :: forall {j :: ()} {k0 :: ()} (f :: MonK k j k0). Obj f -> (I :: MonK k j j) ~> O (Conjoint (MonK k) f) (Companion (MonK k) f) Source Comments #

comConCounit :: forall {j :: ()} {k0 :: ()} (f :: MonK k j k0). Obj f -> O (Companion (MonK k) f) (Conjoint (MonK k) f) ~> (I :: MonK k k k) Source Comments #

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

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

mapCompanion :: forall {j :: ()} {k0 :: ()} (f :: MonK k j k0) (g :: MonK k j k0). (f ~> g) -> Companion (MonK k) f ~> Companion (MonK k) g Source Comments #

compToId :: forall (k0 :: ()). Ob0 (MonK k) k0 => Companion (MonK k) (I :: MonK k k k) ~> (I :: MonK k k k) Source Comments #

compFromId :: forall (k0 :: ()). Ob0 (MonK k) k0 => (I :: MonK k k k) ~> Companion (MonK k) (I :: MonK k k k) Source Comments #

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

compFromCompose :: forall {j1 :: ()} {j2 :: ()} {k0 :: ()} (f :: MonK k j2 k0) (g :: MonK k j1 j2). Obj f -> Obj g -> O (Companion (MonK k) f) (Companion (MonK k) g) ~> Companion (MonK k) (O f g) 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 k1 :: () -> () -> Type) (j :: k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

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

type Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Lan ('MK p :: MonK k c d) ('MK q :: MonK k c e) = 'MK (q <~~ p) :: MonK k d e

type Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Lift ('MK p :: MonK k d c) ('MK q :: MonK k e c) = 'MK (q <~~ p) :: MonK k e d

type Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Ran ('MK p :: MonK k c d) ('MK q :: MonK k c e) = 'MK (p ~~> q) :: MonK k d e

type Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Rift ('MK p :: MonK k d c) ('MK q :: MonK k e c) = 'MK (p ~~> q) :: MonK k e d

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 k1 j k2) ('MK b :: MonK k1 i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

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

type Colimit ('MK j :: MonK k a i) ('MK d :: MonK k i '()) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Colimit ('MK j :: MonK k a i) ('MK d :: MonK k i '()) = 'MK (d ** j) :: MonK k a '()

type Limit ('MK j :: MonK k i a) ('MK d :: MonK k i '()) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Limit ('MK j :: MonK k i a) ('MK d :: MonK k i '()) = 'MK (j ~~> d) :: MonK k a '()

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 Companion (MonK k1 :: () -> () -> Type) ('MK a :: MonK k1 j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Companion (MonK k1 :: () -> () -> Type) ('MK a :: MonK k1 j k2) = 'MK a :: MonK k1 j k2

type Conjoint (MonK k1 :: () -> () -> Type) ('MK a :: MonK k1 j k2) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Conjoint (MonK k1 :: () -> () -> Type) ('MK a :: MonK k1 j k2) = 'MK (Dual a) :: MonK k1 k2 j

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 #