Safe Haskell	None
Language	GHC2024

Proarrow.Category.Equipment.Limit

Synopsis

class (Equipment kk, Ob j) => HasLimits (j :: kk i a) (k :: s) where
- type Limit (j :: kk i a) (d :: kk i k) :: kk a k
- withObLimit :: forall (d :: kk i k) r. IsTight d => (IsTight (Limit j d) => r) -> r
- limit :: forall (d :: kk i k). IsTight d => O (Limit j d) j ~> d
- limitUniv :: forall (d :: kk i k) (p :: kk a k). (IsTight d, Ob p) => (O p j ~> d) -> p ~> Limit j d
limitToLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s} (j :: kk a b) (c :: kk k b) (r :: kk a k). (Equipment kk, HasLimits j k, IsTight r, IsCotight c) => ((I :: kk b b) ~> O c (Limit j r)) -> j ~> O c r
limitFromLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s} (j :: kk a b) (c :: kk k b) (r :: kk a k). (Equipment kk, HasLimits j k, IsTight r, IsCotight c) => (j ~> O c r) -> (I :: kk b b) ~> O c (Limit j r)
mapLimit :: forall {s} {kk :: s -> s -> Type} {i :: s} {a :: s} (j :: kk i a) (k :: s) (p :: kk i k) (q :: kk i k). (HasLimits j k, IsTight p, IsTight q) => (p ~> q) -> Limit j p ~> Limit j q
class (Equipment kk, Ob j) => HasColimits (j :: kk a i) (k :: s) where
- type Colimit (j :: kk a i) (d :: kk k i) :: kk k a
- withObColimit :: forall (d :: kk k i) r. IsCotight d => (IsCotight (Colimit j d) => r) -> r
- colimit :: forall (d :: kk k i). IsCotight d => O j (Colimit j d) ~> d
- colimitUniv :: forall (d :: kk k i) (p :: kk k a). (IsCotight d, Ob p) => (O j p ~> d) -> p ~> Colimit j d
colimitToLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s} (j :: kk a b) (c :: kk k b) (r :: kk a k). (Equipment kk, HasColimits j k, IsTight r, IsCotight c) => ((I :: kk a a) ~> O (Colimit j c) r) -> j ~> O c r
colimitFromLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s} (j :: kk a b) (c :: kk k b) (r :: kk a k). (Equipment kk, HasColimits j k, IsTight r, IsCotight c) => (j ~> O c r) -> (I :: kk a a) ~> O (Colimit j c) r
mapColimit :: forall {s} {kk :: s -> s -> Type} {i :: s} {a :: s} (j :: kk a i) (k :: s) (p :: kk k i) (q :: kk k i). (HasColimits j k, IsCotight p, IsCotight q) => (p ~> q) -> Colimit j p ~> Colimit j q

Documentation

class (Equipment kk, Ob j) => HasLimits (j :: kk i a) (k :: s) where Source Comments #

weighted limits

Associated Types

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

Methods

withObLimit :: forall (d :: kk i k) r. IsTight d => (IsTight (Limit j d) => r) -> r Source Comments #

limit :: forall (d :: kk i k). IsTight d => O (Limit j d) j ~> d Source Comments #

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

Instances

Instances details

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

limitToLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s} (j :: kk a b) (c :: kk k b) (r :: kk a k). (Equipment kk, HasLimits j k, IsTight r, IsCotight c) => ((I :: kk b b) ~> O c (Limit j r)) -> j ~> O c r Source Comments #

limitFromLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s} (j :: kk a b) (c :: kk k b) (r :: kk a k). (Equipment kk, HasLimits j k, IsTight r, IsCotight c) => (j ~> O c r) -> (I :: kk b b) ~> O c (Limit j r) Source Comments #

mapLimit :: forall {s} {kk :: s -> s -> Type} {i :: s} {a :: s} (j :: kk i a) (k :: s) (p :: kk i k) (q :: kk i k). (HasLimits j k, IsTight p, IsTight q) => (p ~> q) -> Limit j p ~> Limit j q Source Comments #

class (Equipment kk, Ob j) => HasColimits (j :: kk a i) (k :: s) where Source Comments #

weighted colimits

Associated Types

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

Methods

withObColimit :: forall (d :: kk k i) r. IsCotight d => (IsCotight (Colimit j d) => r) -> r Source Comments #

colimit :: forall (d :: kk k i). IsCotight d => O j (Colimit j d) ~> d Source Comments #

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

Instances

Instances details

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

colimitToLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s} (j :: kk a b) (c :: kk k b) (r :: kk a k). (Equipment kk, HasColimits j k, IsTight r, IsCotight c) => ((I :: kk a a) ~> O (Colimit j c) r) -> j ~> O c r Source Comments #

colimitFromLimitAdj :: forall {s} {kk :: s -> s -> Type} {k :: s} {a :: s} {b :: s} (j :: kk a b) (c :: kk k b) (r :: kk a k). (Equipment kk, HasColimits j k, IsTight r, IsCotight c) => (j ~> O c r) -> (I :: kk a a) ~> O (Colimit j c) r Source Comments #

mapColimit :: forall {s} {kk :: s -> s -> Type} {i :: s} {a :: s} (j :: kk a i) (k :: s) (p :: kk k i) (q :: kk k i). (HasColimits j k, IsCotight p, IsCotight q) => (p ~> q) -> Colimit j p ~> Colimit j q Source Comments #