Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Equipment.Limit

Synopsis

class (HasCompanions hk vk, Ob j) => HasLimits (vk :: CAT s) (j :: hk i a) (k :: s) where
- type Limit (j :: hk i a) (d :: vk i k) :: vk a k
- limitObj :: forall (d :: vk i k). Ob d => Obj (Limit j d)
- limit :: forall (d :: vk i k). Ob d => O (Companion hk (Limit j d)) j ~> Companion hk d
- limitUniv :: forall (d :: vk i k) (p :: vk a k). (Ob d, Ob p) => (O (Companion hk p) j ~> Companion hk d) -> p ~> Limit j d
rightAdjointPreservesLimitsInv :: forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {k :: s} {k' :: s} {i :: s} {a :: s} (g :: vk k k') (d :: vk i k) (j :: hk i a). (Ob d, Ob g, HasLimits vk j k, HasLimits vk j k', Ob0 vk i, Ob0 vk k, Ob0 vk k', Ob0 vk a) => O g (Limit j d) ~> Limit j (O g d)
class (HasCompanions hk vk, Ob j) => HasColimits (vk :: CAT s) (j :: hk a i) (k :: s) where
- type Colimit (j :: hk a i) (d :: vk i k) :: vk a k
- colimit :: forall (d :: vk i k). Ob d => O (Companion hk d) j ~> Companion hk (Colimit j d)
- colimitUniv :: forall (d :: vk i k) (p :: vk a k). (Ob d, Ob p) => (O (Companion hk d) j ~> Companion hk p) -> Colimit j d ~> p

Documentation

class (HasCompanions hk vk, Ob j) => HasLimits (vk :: CAT s) (j :: hk i a) (k :: s) where Source Comments #

weighted limits

Associated Types

type Limit (j :: hk i a) (d :: vk i k) :: vk a k Source Comments #

Methods

limitObj :: forall (d :: vk i k). Ob d => Obj (Limit j d) Source Comments #

limit :: forall (d :: vk i k). Ob d => O (Companion hk (Limit j d)) j ~> Companion hk d Source Comments #

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

Instances details

(HasLimits j k, Ob j) => HasLimits FUNK ('PK j :: PROFK i a) (k :: Kind) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods limitObj :: forall (d :: FUNK i k). Ob d => Obj (Limit ('PK j) d) Source Comments # limit :: forall (d :: FUNK i k). Ob d => O (Companion PROFK (Limit ('PK j) d)) ('PK j) ~> Companion PROFK d Source Comments # limitUniv :: forall (d :: FUNK i k) (p :: FUNK a k). (Ob d, Ob p) => (O (Companion PROFK p) ('PK j) ~> Companion PROFK d) -> p ~> Limit ('PK j) d 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 #

rightAdjointPreservesLimitsInv :: forall {s} {hk :: s -> s -> Type} {vk :: s -> s -> Type} {k :: s} {k' :: s} {i :: s} {a :: s} (g :: vk k k') (d :: vk i k) (j :: hk i a). (Ob d, Ob g, HasLimits vk j k, HasLimits vk j k', Ob0 vk i, Ob0 vk k, Ob0 vk k', Ob0 vk a) => O g (Limit j d) ~> Limit j (O g d) Source Comments #

class (HasCompanions hk vk, Ob j) => HasColimits (vk :: CAT s) (j :: hk a i) (k :: s) where Source Comments #

weighted colimits

Associated Types

type Colimit (j :: hk a i) (d :: vk i k) :: vk a k Source Comments #

Methods

colimit :: forall (d :: vk i k). Ob d => O (Companion hk d) j ~> Companion hk (Colimit j d) Source Comments #

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

Instances details

(HasColimits j k, Ob j) => HasColimits FUNK ('PK j :: PROFK a i) (k :: Kind) Source Comments #
Instance details Defined in Proarrow.Category.Bicategory.Prof Methods colimit :: forall (d :: FUNK i k). Ob d => O (Companion PROFK d) ('PK j) ~> Companion PROFK (Colimit ('PK j) d) Source Comments # colimitUniv :: forall (d :: FUNK i k) (p :: FUNK a k). (Ob d, Ob p) => (O (Companion PROFK d) ('PK j) ~> Companion PROFK p) -> Colimit ('PK j) d ~> p 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 #