Safe Haskell | None |
---|---|
Language | GHC2024 |
Proarrow.Category.Limit
Synopsis
- class Representable (Limit j1 d) => IsRepresentableLimit (j1 :: i +-> j) (d :: i +-> k)
- class (Profunctor j, forall (d :: i +-> k). Representable d => IsRepresentableLimit j d) => HasLimits (j :: i +-> a) k where
- rightAdjointPreservesLimits :: forall {k} {k'} {i} {a} (f :: k' +-> k) (g :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Adjunction f g, Representable d, Representable f, Representable g, HasLimits j k, HasLimits j k') => Limit j (g :.: d) :~> (g :.: Limit j d)
- rightAdjointPreservesLimitsInv :: forall {k} {k'} {i} {a} (g :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Representable d, Representable g, HasLimits j k, HasLimits j k') => (g :.: Limit j d) :~> Limit j (g :.: d)
- type Unweighted = TerminalProfunctor :: k -> j -> Type
- data family TerminalLimit :: (VOID +-> k) -> () +-> k
- data family ProductLimit :: (COPRODUCT () () +-> k) -> () +-> k
- choose :: forall k (d :: COPRODUCT () () +-> k) (b :: COPRODUCT () ()). (HasBinaryProducts k, Representable d) => Obj b -> ((d % ('L '() :: COPRODUCT () ())) && (d % ('R '() :: COPRODUCT () ()))) ~> (d % b)
- data family PowerLimit :: v -> (() +-> k) -> () +-> k
- newtype End (d :: (OPPOSITE k, k) +-> Type) = End {}
- data family EndLimit :: ((OPPOSITE k, k) +-> Type) -> () +-> Type
- data Hom (a :: ()) (b :: (OPPOSITE k, k)) where
Documentation
class Representable (Limit j1 d) => IsRepresentableLimit (j1 :: i +-> j) (d :: i +-> k) Source Comments #
Instances
Representable (Limit j2 d) => IsRepresentableLimit (j2 :: i +-> j1) (d :: i +-> k) Source Comments # | |
Defined in Proarrow.Category.Limit |
class (Profunctor j, forall (d :: i +-> k). Representable d => IsRepresentableLimit j d) => HasLimits (j :: i +-> a) k where Source Comments #
profunctor-weighted limits
Methods
limit :: forall (d :: i +-> k). Representable d => (Limit j d :.: j) :~> d Source Comments #
limitUniv :: forall (d :: i +-> k) (p :: a +-> k). (Representable d, Profunctor p) => ((p :.: j) :~> d) -> p :~> Limit j d Source Comments #
Instances
rightAdjointPreservesLimits :: forall {k} {k'} {i} {a} (f :: k' +-> k) (g :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Adjunction f g, Representable d, Representable f, Representable g, HasLimits j k, HasLimits j k') => Limit j (g :.: d) :~> (g :.: Limit j d) Source Comments #
rightAdjointPreservesLimitsInv :: forall {k} {k'} {i} {a} (g :: k +-> k') (d :: i +-> k) (j :: i +-> a). (Representable d, Representable g, HasLimits j k, HasLimits j k') => (g :.: Limit j d) :~> Limit j (g :.: d) Source Comments #
type Unweighted = TerminalProfunctor :: k -> j -> Type Source Comments #
data family TerminalLimit :: (VOID +-> k) -> () +-> k Source Comments #
Instances
HasTerminalObject k => FunctorForRep (TerminalLimit d :: () +-> k) Source Comments # | |
Defined in Proarrow.Category.Limit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (TerminalLimit d @ a) ~> (TerminalLimit d @ b) Source Comments # | |
type (TerminalLimit d :: () +-> k) @ (a :: ()) Source Comments # | |
Defined in Proarrow.Category.Limit |
data family ProductLimit :: (COPRODUCT () () +-> k) -> () +-> k Source Comments #
Instances
(HasBinaryProducts k, Representable d) => FunctorForRep (ProductLimit d :: () +-> k) Source Comments # | |
Defined in Proarrow.Category.Limit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (ProductLimit d @ a) ~> (ProductLimit d @ b) Source Comments # | |
type (ProductLimit d :: () +-> k) @ '() Source Comments # | |
choose :: forall k (d :: COPRODUCT () () +-> k) (b :: COPRODUCT () ()). (HasBinaryProducts k, Representable d) => Obj b -> ((d % ('L '() :: COPRODUCT () ())) && (d % ('R '() :: COPRODUCT () ()))) ~> (d % b) Source Comments #
data family PowerLimit :: v -> (() +-> k) -> () +-> k Source Comments #
Instances
(Representable d, Powered v k, Ob n) => FunctorForRep (PowerLimit n d :: () +-> k) Source Comments # | |
Defined in Proarrow.Category.Limit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (PowerLimit n d @ a) ~> (PowerLimit n d @ b) Source Comments # | |
type (PowerLimit n d :: () +-> k) @ '() Source Comments # | |
Defined in Proarrow.Category.Limit |
data family EndLimit :: ((OPPOSITE k, k) +-> Type) -> () +-> Type Source Comments #
data Hom (a :: ()) (b :: (OPPOSITE k, k)) where Source Comments #
Instances
CategoryOf k => HasLimits (Hom :: () -> (OPPOSITE k, k) -> Type) Type Source Comments # | |
Defined in Proarrow.Category.Limit Methods limit :: forall (d :: (OPPOSITE k, k) +-> Type). Representable d => (Limit (Hom :: () -> (OPPOSITE k, k) -> Type) d :.: (Hom :: () -> (OPPOSITE k, k) -> Type)) :~> d Source Comments # limitUniv :: forall (d :: (OPPOSITE k, k) +-> Type) (p :: () +-> Type). (Representable d, Profunctor p) => ((p :.: (Hom :: () -> (OPPOSITE k, k) -> Type)) :~> d) -> p :~> Limit (Hom :: () -> (OPPOSITE k, k) -> Type) d Source Comments # | |
CategoryOf k => Profunctor (Hom :: () -> (OPPOSITE k, k) -> Type) Source Comments # | |
type Limit (Hom :: () -> (OPPOSITE k, k) -> Type) (d :: (OPPOSITE k, k) +-> Type) Source Comments # | |