Safe Haskell	None
Language	GHC2024

Proarrow.Category.Colimit

Synopsis

type Unweighted = TerminalProfunctor :: k -> j -> Type
class Corepresentable (Colimit j1 d) => IsCorepColimit (j1 :: k +-> i) (d :: j +-> i)
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
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 InitialLimit :: (k +-> VOID) -> () +-> k
data family CoproductColimit :: (k +-> COPRODUCT () ()) -> () +-> k
cochoose :: forall {k} (d :: k +-> COPRODUCT () ()) (b :: COPRODUCT () ()). (HasBinaryCoproducts k, Corepresentable d, Ob b) => (d %% b) ~> ((d %% ('L '() :: COPRODUCT () ())) || (d %% ('R '() :: COPRODUCT () ())))
data family CopowerLimit :: Type -> (k +-> ()) -> () +-> 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)) -> () +-> Type
data Hom (a :: (OPPOSITE k, k)) (b :: ()) where
- Hom :: forall {k} (a1 :: k) (b1 :: k). (a1 ~> b1) -> Hom '('OP b1, a1) '()

Documentation

type Unweighted = TerminalProfunctor :: k -> j -> Type Source Comments #

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

Instances

Instances details

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

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

profunctor-weighted colimits

Associated Types

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

Methods

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

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

Instances

Instances details

CategoryOf j => HasColimits (Id :: j -> j -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: k +-> j). Corepresentable d => ((Id :: j -> j -> Type) :.: Colimit (Id :: j -> j -> Type) d) :~> d Source Comments # 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 Comments #
HasInitialObject k => HasColimits (Unweighted :: VOID -> () -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: k +-> VOID). Corepresentable d => ((Unweighted :: VOID -> () -> Type) :.: Colimit (Unweighted :: VOID -> () -> Type) d) :~> d Source Comments # colimitUniv :: forall (d :: k +-> VOID) (p :: k +-> ()). (Corepresentable d, Profunctor p) => (((Unweighted :: VOID -> () -> Type) :.: p) :~> d) -> p :~> Colimit (Unweighted :: VOID -> () -> Type) d Source Comments #
Copowered Type k => HasColimits (HaskValue n :: () -> () -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: k +-> ()). Corepresentable d => ((HaskValue n :: () -> () -> Type) :.: Colimit (HaskValue n :: () -> () -> Type) d) :~> d Source Comments # colimitUniv :: forall (d :: k +-> ()) (p :: k +-> ()). (Corepresentable d, Profunctor p) => (((HaskValue n :: () -> () -> Type) :.: p) :~> d) -> p :~> Colimit (HaskValue n :: () -> () -> Type) d Source Comments #
Representable j => HasColimits (Wrapped j :: i -> a -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: k +-> i). Corepresentable d => (Wrapped j :.: Colimit (Wrapped j) d) :~> d Source Comments # colimitUniv :: forall (d :: k +-> i) (p :: k +-> a). (Corepresentable d, Profunctor p) => ((Wrapped j :.: p) :~> d) -> p :~> Colimit (Wrapped j) d Source Comments #
(Corepresentable j2, HasColimits j1 k, HasColimits j2 k) => HasColimits (j1 :.: j2 :: i -> a -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: k +-> i). Corepresentable d => ((j1 :.: j2) :.: Colimit (j1 :.: j2) d) :~> d Source Comments # colimitUniv :: forall (d :: k +-> i) (p :: k +-> a). (Corepresentable d, Profunctor p) => (((j1 :.: j2) :.: p) :~> d) -> p :~> Colimit (j1 :.: j2) d Source Comments #
CategoryOf k => HasColimits (Hom :: (OPPOSITE k, k) -> () -> Type) Type Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: Type +-> (OPPOSITE k, k)). Corepresentable d => ((Hom :: (OPPOSITE k, k) -> () -> Type) :.: Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) d) :~> d Source Comments # colimitUniv :: forall (d :: Type +-> (OPPOSITE k, k)) (p :: Type +-> ()). (Corepresentable d, Profunctor p) => (((Hom :: (OPPOSITE k, k) -> () -> Type) :.: p) :~> d) -> p :~> Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) d Source Comments #
HasBinaryCoproducts k => HasColimits (Unweighted :: COPRODUCT () () -> () -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: k +-> COPRODUCT () ()). Corepresentable d => ((Unweighted :: COPRODUCT () () -> () -> Type) :.: Colimit (Unweighted :: COPRODUCT () () -> () -> Type) d) :~> d Source Comments # colimitUniv :: forall (d :: k +-> COPRODUCT () ()) (p :: k +-> ()). (Corepresentable d, Profunctor p) => (((Unweighted :: COPRODUCT () () -> () -> Type) :.: p) :~> d) -> p :~> Colimit (Unweighted :: COPRODUCT () () -> () -> Type) d Source Comments #

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 Comments #

data family InitialLimit :: (k +-> VOID) -> () +-> k Source Comments #

Instances

Instances details

HasInitialObject k => FunctorForRep (InitialLimit d :: () +-> k) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (InitialLimit d @ a) ~> (InitialLimit d @ b) Source Comments #
type (InitialLimit d :: () +-> k) @ '() Source Comments #
Instance details Defined in Proarrow.Category.Colimit type (InitialLimit d :: () +-> k) @ '() = InitialObject :: k

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

Instances

Instances details

(HasBinaryCoproducts k, Corepresentable d) => FunctorForRep (CoproductColimit d :: () +-> k) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods fmap :: forall (a :: ()) (b :: ()). (a ~> b) -> (CoproductColimit d @ a) ~> (CoproductColimit d @ b) Source Comments #
type (CoproductColimit d :: () +-> k) @ '() Source Comments #
Instance details Defined in Proarrow.Category.Colimit type (CoproductColimit d :: () +-> k) @ '() = (d %% ('L '() :: COPRODUCT () ())) \|\| (d %% ('R '() :: COPRODUCT () ()))

cochoose :: forall {k} (d :: k +-> COPRODUCT () ()) (b :: COPRODUCT () ()). (HasBinaryCoproducts k, Corepresentable d, Ob b) => (d %% b) ~> ((d %% ('L '() :: COPRODUCT () ())) || (d %% ('R '() :: COPRODUCT () ()))) Source Comments #

data family CopowerLimit :: Type -> (k +-> ()) -> () +-> k Source Comments #

Instances

Instances details

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

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

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)) -> () +-> Type Source Comments #

Instances

Instances details

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

data Hom (a :: (OPPOSITE k, k)) (b :: ()) where Source Comments #

Constructors

Hom :: forall {k} (a1 :: k) (b1 :: k). (a1 ~> b1) -> Hom '('OP b1, a1) '()

Instances

Instances details

CategoryOf k => Profunctor (Hom :: (OPPOSITE k, k) -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods dimap :: forall (c :: (OPPOSITE k, k)) (a :: (OPPOSITE k, k)) (b :: ()) (d :: ()). (c ~> a) -> (b ~> d) -> Hom a b -> Hom c d Source Comments # (\\) :: forall (a :: (OPPOSITE k, k)) (b :: ()) r. ((Ob a, Ob b) => r) -> Hom a b -> r Source Comments #
CategoryOf k => HasColimits (Hom :: (OPPOSITE k, k) -> () -> Type) Type Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: Type +-> (OPPOSITE k, k)). Corepresentable d => ((Hom :: (OPPOSITE k, k) -> () -> Type) :.: Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) d) :~> d Source Comments # colimitUniv :: forall (d :: Type +-> (OPPOSITE k, k)) (p :: Type +-> ()). (Corepresentable d, Profunctor p) => (((Hom :: (OPPOSITE k, k) -> () -> Type) :.: p) :~> d) -> p :~> Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) d Source Comments #
type Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) (d :: Type +-> (OPPOSITE k, k)) Source Comments #
Instance details Defined in Proarrow.Category.Colimit type Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) (d :: Type +-> (OPPOSITE k, k)) = Corep (CoendLimit d)