Safe Haskell	None
Language	GHC2024

Proarrow.Colimit

Description

Profunctor-weighted colimits: HasColimits j k says k has colimits of k +-> i-diagrams weighted by j, given by the Colimit profunctor with colimit and colimitUniv. The TerminalProfunctor weight gives ordinary conical colimits, e.g. initial objects, binary coproducts and copowers.

As in Proarrow.Limit, the weight synonyms and shape helpers (Unweighted, O1/O2, At1/At2, Hom, Lan) are not exported, since their names clash with ones elsewhere.

Synopsis

class (Profunctor j, forall (d :: k +-> i). Corepresentable d => IsCorepColimit j d) => HasColimits (j :: a +-> i) k where
- type Colimit (j :: a +-> i) (d :: k +-> i) :: k +-> a
- colimit :: forall (d :: k +-> i). Corepresentable d => (j :.: Colimit j d) :~> d
- colimitUniv :: forall (d :: k +-> i) (p :: k +-> a). (Corepresentable d, Profunctor p) => ((j :.: p) :~> d) -> p :~> Colimit j d
class Corepresentable (Colimit j1 d) => IsCorepColimit (j1 :: k +-> i) (d :: j +-> i)
mapColimit :: forall {a} {i} (j :: a +-> i) k (p :: k +-> i) (q :: k +-> i). (HasColimits j k, Corepresentable p, Corepresentable q) => (p ~> q) -> Colimit j p ~> Colimit j q
data family CoproductColimit :: (k +-> COPRODUCT () ()) -> Presheaf k
data family CopowerLimit :: Type -> Copresheaf k -> Presheaf k
data Coend (d :: Type +-> (OPPOSITE k, k)) where
- Coend :: forall {k} (a :: k) (b :: k) (d :: Type +-> (OPPOSITE k, k)). (a ~> b) -> (d %% '('OP b, a)) -> Coend d
data family CoendLimit :: (Type +-> (OPPOSITE k, k)) -> Presheaf Type
newtype AnyColimit (j :: k -> k1 -> Type) (a :: k) (b :: k1) = AnyColimit (j a b)

Documentation

class (Profunctor j, forall (d :: k +-> i). Corepresentable d => IsCorepColimit j d) => HasColimits (j :: a +-> i) k where Source Github #

profunctor-weighted colimits

Associated Types

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

Methods

colimit :: forall (d :: k +-> i). Corepresentable d => (j :.: Colimit j d) :~> d Source Github #

colimitUniv :: forall (d :: k +-> i) (p :: k +-> a). (Corepresentable d, Profunctor p) => ((j :.: p) :~> d) -> p :~> Colimit j d Source Github #

Instances

Instances details

CategoryOf j => HasColimits (Id :: j -> j -> Type) k Source Github #
Instance details Defined in Proarrow.Colimit Methods colimit :: forall (d :: k +-> j). Corepresentable d => ((Id :: j -> j -> Type) :.: Colimit (Id :: j -> j -> Type) d) :~> d Source Github # colimitUniv :: forall (d :: k +-> j) (p :: k +-> j). (Corepresentable d, Profunctor p) => (((Id :: j -> j -> Type) :.: p) :~> d) -> p :~> Colimit (Id :: j -> j -> Type) d Source Github #
Copowered Type k => HasColimits (HaskValue n :: () -> () -> Type) k Source Github #
Instance details Defined in Proarrow.Colimit Methods colimit :: forall (d :: k +-> ()). Corepresentable d => ((HaskValue n :: () -> () -> Type) :.: Colimit (HaskValue n :: () -> () -> Type) d) :~> d Source Github # colimitUniv :: forall (d :: k +-> ()) (p :: k +-> ()). (Corepresentable d, Profunctor p) => (((HaskValue n :: () -> () -> Type) :.: p) :~> d) -> p :~> Colimit (HaskValue n :: () -> () -> Type) d Source Github #
Profunctor j => HasColimits (AnyColimit j :: i -> a -> Type) Type Source Github #
Instance details Defined in Proarrow.Colimit Methods colimit :: forall (d :: Type +-> i). Corepresentable d => (AnyColimit j :.: Colimit (AnyColimit j) d) :~> d Source Github # colimitUniv :: forall (d :: Type +-> i) (p :: Type +-> a). (Corepresentable d, Profunctor p) => ((AnyColimit j :.: p) :~> d) -> p :~> Colimit (AnyColimit j) d Source Github #
FunctorForRep f => HasColimits (Rep f :: i -> a -> Type) k Source Github #
Instance details Defined in Proarrow.Colimit Methods colimit :: forall (d :: k +-> i). Corepresentable d => (Rep f :.: Colimit (Rep f) d) :~> d Source Github # colimitUniv :: forall (d :: k +-> i) (p :: k +-> a). (Corepresentable d, Profunctor p) => ((Rep f :.: p) :~> d) -> p :~> Colimit (Rep f) d Source Github #
(Corepresentable j2, HasColimits j1 k, HasColimits j2 k) => HasColimits (j1 :.: j2 :: i -> a -> Type) k Source Github #
Instance details Defined in Proarrow.Colimit Methods colimit :: forall (d :: k +-> i). Corepresentable d => ((j1 :.: j2) :.: Colimit (j1 :.: j2) d) :~> d Source Github # colimitUniv :: forall (d :: k +-> i) (p :: k +-> a). (Corepresentable d, Profunctor p) => (((j1 :.: j2) :.: p) :~> d) -> p :~> Colimit (j1 :.: j2) d Source Github #

class Corepresentable (Colimit j1 d) => IsCorepColimit (j1 :: k +-> i) (d :: j +-> i) Source Github #

Instances

Instances details

Corepresentable (Colimit j2 d) => IsCorepColimit (j2 :: k +-> i) (d :: j1 +-> i) Source Github #
Instance details Defined in Proarrow.Colimit

mapColimit :: forall {a} {i} (j :: a +-> i) k (p :: k +-> i) (q :: k +-> i). (HasColimits j k, Corepresentable p, Corepresentable q) => (p ~> q) -> Colimit j p ~> Colimit j q Source Github #

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

Instances

Instances details

(HasBinaryCoproducts k, Corepresentable d) => FunctorForRep (CoproductColimit d :: Presheaf k) Source Github #
Instance details Defined in Proarrow.Colimit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (CoproductColimit d @ a) ~> (CoproductColimit d @ b) Source Github #
type (CoproductColimit d :: Presheaf k) @ '() Source Github #
Instance details Defined in Proarrow.Colimit type (CoproductColimit d :: Presheaf k) @ '()

data family CopowerLimit :: Type -> Copresheaf k -> Presheaf k Source Github #

Instances

Instances details

(Corepresentable d, Copowered Type k) => FunctorForRep (CopowerLimit n d :: Presheaf k) Source Github #
Instance details Defined in Proarrow.Colimit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (CopowerLimit n d @ a) ~> (CopowerLimit n d @ b) Source Github #
type (CopowerLimit n d :: Presheaf k) @ '() Source Github #
Instance details Defined in Proarrow.Colimit type (CopowerLimit n d :: Presheaf k) @ '() = n *. (d %% '())

data Coend (d :: Type +-> (OPPOSITE k, k)) where Source Github #

Constructors

Coend :: forall {k} (a :: k) (b :: k) (d :: Type +-> (OPPOSITE k, k)). (a ~> b) -> (d %% '('OP b, a)) -> Coend d

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

Instances

Instances details

Corepresentable d => FunctorForRep (CoendLimit d :: Presheaf Type) Source Github #
Instance details Defined in Proarrow.Colimit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (CoendLimit d @ a) ~> (CoendLimit d @ b) Source Github #
type (CoendLimit d :: Presheaf Type) @ '() Source Github #
Instance details Defined in Proarrow.Colimit type (CoendLimit d :: Presheaf Type) @ '() = Coend d

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

Constructors

AnyColimit (j a b)

Instances

Instances details

Profunctor j2 => Profunctor (AnyColimit j2 :: k -> j1 -> Type) Source Github #
Instance details Defined in Proarrow.Colimit Methods dimap :: forall (c :: k) (a :: k) (b :: j1) (d :: j1). (c ~> a) -> (b ~> d) -> AnyColimit j2 a b -> AnyColimit j2 c d Source Github # lmap :: forall (c :: k) (a :: k) (b :: j1). (c ~> a) -> AnyColimit j2 a b -> AnyColimit j2 c b Source Github # rmap :: forall (b :: j1) (d :: j1) (a :: k). (b ~> d) -> AnyColimit j2 a b -> AnyColimit j2 a d Source Github # (\\) :: forall (a :: k) (b :: j1) r. ((Ob a, Ob b) => r) -> AnyColimit j2 a b -> r Source Github #
Profunctor j => HasColimits (AnyColimit j :: i -> a -> Type) Type Source Github #
Instance details Defined in Proarrow.Colimit Methods colimit :: forall (d :: Type +-> i). Corepresentable d => (AnyColimit j :.: Colimit (AnyColimit j) d) :~> d Source Github # colimitUniv :: forall (d :: Type +-> i) (p :: Type +-> a). (Corepresentable d, Profunctor p) => ((AnyColimit j :.: p) :~> d) -> p :~> Colimit (AnyColimit j) d Source Github #
type Colimit (AnyColimit j :: i -> a -> Type) (d :: Type +-> i) Source Github #
Instance details Defined in Proarrow.Colimit type Colimit (AnyColimit j :: i -> a -> Type) (d :: Type +-> i)