Safe Haskell	None
Language	GHC2024

Proarrow.Limit

Description

Profunctor-weighted limits: HasLimits j k says k has limits of i +-> k-diagrams weighted by j, given by the Limit profunctor with limit and limitUniv. The TerminalProfunctor weight recovers ordinary conical limits, e.g. terminal objects, binary products and powers as special shapes.

The helpers that state those instances (Unweighted, O1/O2, At1/At2, Hom, Ran) are not exported, since they clash with names in Proarrow.Colimit, Proarrow.Core and Proarrow.Profunctor.Instance.Ran.

Synopsis

class (Profunctor j, forall (d :: i +-> k). Representable d => IsRepresentableLimit j d) => HasLimits (j :: i +-> a) k where
- type Limit (j :: i +-> a) (d :: i +-> k) :: a +-> k
- limit :: forall (d :: i +-> k). Representable d => (Limit j d :.: j) :~> d
- limitUniv :: forall (d :: i +-> k) (p :: a +-> k). (Representable d, Profunctor p) => ((p :.: j) :~> d) -> p :~> Limit j d
class Representable (Limit j1 d) => IsRepresentableLimit (j1 :: i +-> j) (d :: i +-> k)
mapLimit :: forall {a} {i} (j :: i +-> a) k (p :: i +-> k) (q :: i +-> k). (HasLimits j k, Representable p, Representable q) => (p ~> q) -> Limit j p ~> Limit j q
data family ProductLimit :: (COPRODUCT () () +-> k) -> Presheaf k
data family PowerLimit :: v -> Presheaf k -> Presheaf k
newtype End (d :: (OPPOSITE k, k) +-> Type) = End {
- unEnd :: forall (a :: k) (b :: k). (a ~> b) -> d % '('OP a, b)
}
data family EndLimit :: ((OPPOSITE k, k) +-> Type) -> Presheaf Type
newtype AnyLimit (j :: k -> k1 -> Type) (a :: k) (b :: k1) = AnyLimit (j a b)

Documentation

class (Profunctor j, forall (d :: i +-> k). Representable d => IsRepresentableLimit j d) => HasLimits (j :: i +-> a) k where Source Github #

profunctor-weighted limits

Associated Types

type Limit (j :: i +-> a) (d :: i +-> k) :: a +-> k Source Github #

Methods

limit :: forall (d :: i +-> k). Representable d => (Limit j d :.: j) :~> d Source Github #

limitUniv :: forall (d :: i +-> k) (p :: a +-> k). (Representable d, Profunctor p) => ((p :.: j) :~> d) -> p :~> Limit j d Source Github #

Instances

Instances details

CategoryOf j => HasLimits (Id :: j -> j -> Type) k Source Github #
Instance details Defined in Proarrow.Limit Methods limit :: forall (d :: j +-> k). Representable d => (Limit (Id :: j -> j -> Type) d :.: (Id :: j -> j -> Type)) :~> d Source Github # limitUniv :: forall (d :: j +-> k) (p :: j +-> k). (Representable d, Profunctor p) => ((p :.: (Id :: j -> j -> Type)) :~> d) -> p :~> Limit (Id :: j -> j -> Type) d Source Github #
Powered Type k => HasLimits (HaskValue n :: () -> () -> Type) k Source Github #
Instance details Defined in Proarrow.Limit Methods limit :: forall (d :: () +-> k). Representable d => (Limit (HaskValue n :: () -> () -> Type) d :.: (HaskValue n :: () -> () -> Type)) :~> d Source Github # limitUniv :: forall (d :: () +-> k) (p :: () +-> k). (Representable d, Profunctor p) => ((p :.: (HaskValue n :: () -> () -> Type)) :~> d) -> p :~> Limit (HaskValue n :: () -> () -> Type) d Source Github #
Profunctor j => HasLimits (AnyLimit j :: a -> i -> Type) Type Source Github #
Instance details Defined in Proarrow.Limit Methods limit :: forall (d :: i +-> Type). Representable d => (Limit (AnyLimit j) d :.: AnyLimit j) :~> d Source Github # limitUniv :: forall (d :: i +-> Type) (p :: a +-> Type). (Representable d, Profunctor p) => ((p :.: AnyLimit j) :~> d) -> p :~> Limit (AnyLimit j) d Source Github #
FunctorForRep f => HasLimits (Corep f :: a -> i -> Type) k Source Github #
Instance details Defined in Proarrow.Limit Methods limit :: forall (d :: i +-> k). Representable d => (Limit (Corep f) d :.: Corep f) :~> d Source Github # limitUniv :: forall (d :: i +-> k) (p :: a +-> k). (Representable d, Profunctor p) => ((p :.: Corep f) :~> d) -> p :~> Limit (Corep f) d Source Github #
(Representable j1, HasLimits j1 k, HasLimits j2 k) => HasLimits (j1 :.: j2 :: a -> i -> Type) k Source Github #
Instance details Defined in Proarrow.Limit Methods limit :: forall (d :: i +-> k). Representable d => (Limit (j1 :.: j2) d :.: (j1 :.: j2)) :~> d Source Github # limitUniv :: forall (d :: i +-> k) (p :: a +-> k). (Representable d, Profunctor p) => ((p :.: (j1 :.: j2)) :~> d) -> p :~> Limit (j1 :.: j2) d Source Github #

class Representable (Limit j1 d) => IsRepresentableLimit (j1 :: i +-> j) (d :: i +-> k) Source Github #

Instances

Instances details

Representable (Limit j2 d) => IsRepresentableLimit (j2 :: i +-> j1) (d :: i +-> k) Source Github #
Instance details Defined in Proarrow.Limit

mapLimit :: forall {a} {i} (j :: i +-> a) k (p :: i +-> k) (q :: i +-> k). (HasLimits j k, Representable p, Representable q) => (p ~> q) -> Limit j p ~> Limit j q Source Github #

data family ProductLimit :: (COPRODUCT () () +-> k) -> Presheaf k Source Github #

Instances

Instances details

(HasBinaryProducts k, Representable d) => FunctorForRep (ProductLimit d :: Presheaf k) Source Github #
Instance details Defined in Proarrow.Limit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (ProductLimit d @ a) ~> (ProductLimit d @ b) Source Github #
type (ProductLimit d :: Presheaf k) @ '() Source Github #
Instance details Defined in Proarrow.Limit type (ProductLimit d :: Presheaf k) @ '()

data family PowerLimit :: v -> Presheaf k -> Presheaf k Source Github #

Instances

Instances details

(Representable d, Powered v k, Ob n) => FunctorForRep (PowerLimit n d :: Presheaf k) Source Github #
Instance details Defined in Proarrow.Limit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (PowerLimit n d @ a) ~> (PowerLimit n d @ b) Source Github #
type (PowerLimit n d :: Presheaf k) @ '() Source Github #
Instance details Defined in Proarrow.Limit type (PowerLimit n d :: Presheaf k) @ '() = (d % '()) ^ n

newtype End (d :: (OPPOSITE k, k) +-> Type) Source Github #

Constructors

End
Fields unEnd :: forall (a :: k) (b :: k). (a ~> b) -> d % '('OP a, b)

data family EndLimit :: ((OPPOSITE k, k) +-> Type) -> Presheaf Type Source Github #

Instances

Instances details

Representable d => FunctorForRep (EndLimit d :: Presheaf Type) Source Github #
Instance details Defined in Proarrow.Limit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (EndLimit d @ a) ~> (EndLimit d @ b) Source Github #
type (EndLimit d :: Presheaf Type) @ '() Source Github #
Instance details Defined in Proarrow.Limit type (EndLimit d :: Presheaf Type) @ '() = End d

newtype AnyLimit (j :: k -> k1 -> Type) (a :: k) (b :: k1) Source Github #

Constructors

AnyLimit (j a b)

Instances

Instances details

Profunctor j2 => Profunctor (AnyLimit j2 :: k -> j1 -> Type) Source Github #
Instance details Defined in Proarrow.Limit Methods dimap :: forall (c :: k) (a :: k) (b :: j1) (d :: j1). (c ~> a) -> (b ~> d) -> AnyLimit j2 a b -> AnyLimit j2 c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: j1). (c ~> a) -> AnyLimit j2 a b -> AnyLimit j2 c b Source Github # rmap :: forall (b :: j1) (d :: j1) (a :: k). (b ~> d) -> AnyLimit j2 a b -> AnyLimit j2 a d Source Github # (\\) :: forall (a :: k) (b :: j1) r. ((Ob a, Ob b) => r) -> AnyLimit j2 a b -> r Source Github #
Profunctor j => HasLimits (AnyLimit j :: a -> i -> Type) Type Source Github #
Instance details Defined in Proarrow.Limit Methods limit :: forall (d :: i +-> Type). Representable d => (Limit (AnyLimit j) d :.: AnyLimit j) :~> d Source Github # limitUniv :: forall (d :: i +-> Type) (p :: a +-> Type). (Representable d, Profunctor p) => ((p :.: AnyLimit j) :~> d) -> p :~> Limit (AnyLimit j) d Source Github #
type Limit (AnyLimit j :: a -> i -> Type) (d :: i +-> Type) Source Github #
Instance details Defined in Proarrow.Limit type Limit (AnyLimit j :: a -> i -> Type) (d :: i +-> Type)