Safe Haskell	None
Language	GHC2024

Proarrow.Category.Bicategory.MonoidalAsBi

Documentation

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

Constructors

MK k

Instances

Instances details

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

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: MonK k j k0) (b :: MonK k i j) r. (Ob a, Ob b, IsOb Cotight a, IsOb Cotight b) => ((IsOb Cotight (O a b), Ob (O a b)) => r) -> r Source Comments #

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

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

withObO2 :: forall {i :: ()} {j :: ()} {k0 :: ()} (a :: MonK k j k0) (b :: MonK k i j) r. (Ob a, Ob b, IsOb Tight a, IsOb Tight b) => ((IsOb Tight (O a b), Ob (O a b)) => r) -> r Source Comments #

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 {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 #

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

withOb0s :: forall {j :: ()} {k0 :: ()} (a :: MonK k j k0) r. Ob a => ((Ob0 (MonK k) j, Ob0 (MonK k) k0) => r) -> r 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 #

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

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

withCotightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: MonK k j k1) r. IsTight f => ((Adjunction_ f (CotightAdjoint f), IsCotight (CotightAdjoint f)) => r) -> r Source Comments #

withTightAdjoint :: forall {j :: ()} {k1 :: ()} (f :: MonK k j k1) r. IsCotight f => ((Adjunction_ (TightAdjoint f) f, IsTight (TightAdjoint f)) => r) -> r 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 #

(CompactClosed k, Ob j) => HasColimits ('MK j :: MonK k i0 i1) '() Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

withObColimit :: forall (d :: MonK k '() i1) r. IsCotight d => (IsCotight (Colimit ('MK j :: MonK k i0 i1) d) => r) -> r Source Comments #

colimit :: forall (d :: MonK k '() i1). IsCotight d => O ('MK j :: MonK k i0 i1) (Colimit ('MK j :: MonK k i0 i1) d) ~> d Source Comments #

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

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

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

withObLimit :: forall (d :: MonK k i '()) r. IsTight d => (IsTight (Limit ('MK j :: MonK k i a) d) => r) -> r Source Comments #

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

limitUniv :: forall (d :: MonK k i '()) (p :: MonK k a '()). (IsTight d, Ob p) => (O p ('MK j :: MonK k i a) ~> d) -> p ~> Limit ('MK j :: MonK k i a) 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 #

CategoryOf k => Functor ('MK :: k -> MonK k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

Methods

map :: forall (a :: k) (b :: k). (a ~> b) -> ('MK a :: MonK k i j) ~> ('MK b :: MonK k i j) 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 IsOb Cotight ('MK a :: MonK k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type IsOb Cotight ('MK a :: MonK k i j) = ()

type IsOb Tight ('MK a :: MonK k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type IsOb Tight ('MK a :: MonK k i j) = ()

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 CotightAdjoint (a :: MonK k i j) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type CotightAdjoint (a :: MonK k i j) = Dual a :: MonK k j i

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

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type TightAdjoint (a :: MonK k i j) = Dual a :: MonK k j 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 i0 i1) ('MK d :: MonK k '() i1) Source Comments #

Instance details

Defined in Proarrow.Category.Bicategory.MonoidalAsBi

type Colimit ('MK j :: MonK k i0 i1) ('MK d :: MonK k '() i1) = 'MK (Dual j ** d) :: MonK k '() i0

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 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 #

dualAdj :: forall {c :: ()} {d :: ()} {k} (a :: k). (CompactClosed k, Ob a) => Adj ('MK (Dual a) :: MonK k c d) ('MK a :: MonK k d c) Source Comments #

dualAdj' :: forall {c :: ()} {d :: ()} {k} (a :: k). (CompactClosed k, Ob a) => Adj ('MK a :: MonK k c d) ('MK (Dual a) :: MonK k d c) Source Comments #

type Dual (a :: MonK k i1 j1) = 'MK (Dual (UN ('MK :: k -> MonK k i1 j1) a)) :: MonK k i j Source Comments #