Safe Haskell	None
Language	GHC2024

Proarrow.Category.Colimit

Synopsis

type Unweighted = TerminalProfunctor :: k -> j -> Type
class Corepresentable (Colimit j1 d) => IsCorepresentableColimit (j1 :: k +-> i) (d :: j +-> i)
class (Profunctor j, forall (d :: k +-> i). Corepresentable d => IsCorepresentableColimit 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
leftAdjointPreservesColimits :: forall {k} {k'} {i} {a} (f :: k' +-> k) (g :: k +-> k') (d :: k +-> i) (j :: a +-> i). (Adjunction f g, Corepresentable d, Corepresentable f, HasColimits j k, HasColimits j k') => Colimit j (d :.: f) :~> (Colimit j d :.: f)
leftAdjointPreservesColimitsInv :: forall {k} {k'} {i} {a} (f :: k' +-> k) (d :: k +-> i) (j :: a +-> i). (Corepresentable d, Corepresentable f, HasColimits j k, HasColimits j k') => (Colimit j d :.: f) :~> Colimit j (d :.: f)
data InitialLimit (d :: k +-> VOID) (a :: ()) (b :: k) where
- InitialLimit :: forall {k} (d :: k +-> VOID) (b :: k). ((InitialObject :: k) ~> b) -> InitialLimit d '() b
data CoproductColimit (d :: k +-> COPRODUCT () ()) (a :: ()) (b :: k) where
- CoproductColimit :: forall {k} (d :: k +-> COPRODUCT () ()) (b :: k). (((d %% ('L '() :: COPRODUCT () ())) || (d %% ('R '() :: COPRODUCT () ()))) ~> b) -> CoproductColimit d '() b
cochoose :: forall k (d :: k +-> COPRODUCT () ()) (b :: COPRODUCT () ()). (HasBinaryCoproducts k, Corepresentable d) => Obj b -> (d %% b) ~> ((d %% ('L '() :: COPRODUCT () ())) || (d %% ('R '() :: COPRODUCT () ())))
data CopowerLimit n (d :: k +-> ()) (a :: ()) (b :: k) where
- CopowerLimit :: forall {k} n (d :: k +-> ()) (b :: k). Ob n => ((CopowerLimit n d %% '()) ~> b) -> CopowerLimit n d '() b
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 CoendLimit (d :: Type +-> (OPPOSITE k, k)) (a :: ()) b where
- CoendLimit :: forall {k} (d :: Type +-> (OPPOSITE k, k)) b. (Coend d -> b) -> CoendLimit d '() b
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) => IsCorepresentableColimit (j1 :: k +-> i) (d :: j +-> i) Source Comments #

Instances

Instances details

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

class (Profunctor j, forall (d :: k +-> i). Corepresentable d => IsCorepresentableColimit 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 #

leftAdjointPreservesColimits :: forall {k} {k'} {i} {a} (f :: k' +-> k) (g :: k +-> k') (d :: k +-> i) (j :: a +-> i). (Adjunction f g, Corepresentable d, Corepresentable f, HasColimits j k, HasColimits j k') => Colimit j (d :.: f) :~> (Colimit j d :.: f) Source Comments #

leftAdjointPreservesColimitsInv :: forall {k} {k'} {i} {a} (f :: k' +-> k) (d :: k +-> i) (j :: a +-> i). (Corepresentable d, Corepresentable f, HasColimits j k, HasColimits j k') => (Colimit j d :.: f) :~> Colimit j (d :.: f) Source Comments #

data InitialLimit (d :: k +-> VOID) (a :: ()) (b :: k) where Source Comments #

Constructors

InitialLimit :: forall {k} (d :: k +-> VOID) (b :: k). ((InitialObject :: k) ~> b) -> InitialLimit d '() b

Instances

Instances details

HasInitialObject k => Profunctor (InitialLimit d :: () -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods dimap :: forall (c :: ()) (a :: ()) (b :: k) (d0 :: k). (c ~> a) -> (b ~> d0) -> InitialLimit d a b -> InitialLimit d c d0 Source Comments # (\\) :: forall (a :: ()) (b :: k) r. ((Ob a, Ob b) => r) -> InitialLimit d a b -> r Source Comments #
HasInitialObject k => Corepresentable (InitialLimit d :: () -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods coindex :: forall (a :: ()) (b :: k). InitialLimit d a b -> (InitialLimit d %% a) ~> b Source Comments # cotabulate :: forall (a :: ()) (b :: k). Ob a => ((InitialLimit d %% a) ~> b) -> InitialLimit d a b Source Comments # corepMap :: forall (a :: ()) (b :: ()). (a ~> b) -> (InitialLimit d %% a) ~> (InitialLimit d %% b) Source Comments #
type (InitialLimit d :: () -> k -> Type) %% '() Source Comments #
Instance details Defined in Proarrow.Category.Colimit type (InitialLimit d :: () -> k -> Type) %% '() = InitialObject :: k

data CoproductColimit (d :: k +-> COPRODUCT () ()) (a :: ()) (b :: k) where Source Comments #

Constructors

CoproductColimit :: forall {k} (d :: k +-> COPRODUCT () ()) (b :: k). (((d %% ('L '() :: COPRODUCT () ())) || (d %% ('R '() :: COPRODUCT () ()))) ~> b) -> CoproductColimit d '() b

Instances

Instances details

CategoryOf k => Profunctor (CoproductColimit d :: () -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods dimap :: forall (c :: ()) (a :: ()) (b :: k) (d0 :: k). (c ~> a) -> (b ~> d0) -> CoproductColimit d a b -> CoproductColimit d c d0 Source Comments # (\\) :: forall (a :: ()) (b :: k) r. ((Ob a, Ob b) => r) -> CoproductColimit d a b -> r Source Comments #
(HasBinaryCoproducts k, Corepresentable d) => Corepresentable (CoproductColimit d :: () -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods coindex :: forall (a :: ()) (b :: k). CoproductColimit d a b -> (CoproductColimit d %% a) ~> b Source Comments # cotabulate :: forall (a :: ()) (b :: k). Ob a => ((CoproductColimit d %% a) ~> b) -> CoproductColimit d a b Source Comments # corepMap :: forall (a :: ()) (b :: ()). (a ~> b) -> (CoproductColimit d %% a) ~> (CoproductColimit d %% b) Source Comments #
type (CoproductColimit d :: () -> k -> Type) %% '() Source Comments #
Instance details Defined in Proarrow.Category.Colimit type (CoproductColimit d :: () -> k -> Type) %% '() = (d %% ('L '() :: COPRODUCT () ())) \|\| (d %% ('R '() :: COPRODUCT () ()))

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

data CopowerLimit n (d :: k +-> ()) (a :: ()) (b :: k) where Source Comments #

Constructors

CopowerLimit :: forall {k} n (d :: k +-> ()) (b :: k). Ob n => ((CopowerLimit n d %% '()) ~> b) -> CopowerLimit n d '() b

Instances

Instances details

(Corepresentable d, Copowered Type k) => Profunctor (CopowerLimit n d :: () -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods dimap :: forall (c :: ()) (a :: ()) (b :: k) (d0 :: k). (c ~> a) -> (b ~> d0) -> CopowerLimit n d a b -> CopowerLimit n d c d0 Source Comments # (\\) :: forall (a :: ()) (b :: k) r. ((Ob a, Ob b) => r) -> CopowerLimit n d a b -> r Source Comments #
(Corepresentable d, Copowered Type k) => Corepresentable (CopowerLimit n d :: () -> k -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods coindex :: forall (a :: ()) (b :: k). CopowerLimit n d a b -> (CopowerLimit n d %% a) ~> b Source Comments # cotabulate :: forall (a :: ()) (b :: k). Ob a => ((CopowerLimit n d %% a) ~> b) -> CopowerLimit n d a b Source Comments # corepMap :: forall (a :: ()) (b :: ()). (a ~> b) -> (CopowerLimit n d %% a) ~> (CopowerLimit n d %% b) Source Comments #
type (CopowerLimit n d :: () -> k -> Type) %% '() Source Comments #
Instance details Defined in Proarrow.Category.Colimit type (CopowerLimit n d :: () -> k -> Type) %% '() = 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 CoendLimit (d :: Type +-> (OPPOSITE k, k)) (a :: ()) b where Source Comments #

Constructors

CoendLimit :: forall {k} (d :: Type +-> (OPPOSITE k, k)) b. (Coend d -> b) -> CoendLimit d '() b

Instances

Instances details

Corepresentable d => Profunctor (CoendLimit d :: () -> Type -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods dimap :: forall (c :: ()) (a :: ()) b d0. (c ~> a) -> (b ~> d0) -> CoendLimit d a b -> CoendLimit d c d0 Source Comments # (\\) :: forall (a :: ()) b r. ((Ob a, Ob b) => r) -> CoendLimit d a b -> r Source Comments #
Corepresentable d => Corepresentable (CoendLimit d :: () -> Type -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods coindex :: forall (a :: ()) b. CoendLimit d a b -> (CoendLimit d %% a) ~> b Source Comments # cotabulate :: forall (a :: ()) b. Ob a => ((CoendLimit d %% a) ~> b) -> CoendLimit d a b Source Comments # corepMap :: forall (a :: ()) (b :: ()). (a ~> b) -> (CoendLimit d %% a) ~> (CoendLimit d %% b) Source Comments #
type (CoendLimit d :: () -> Type -> Type) %% '() Source Comments #
Instance details Defined in Proarrow.Category.Colimit type (CoendLimit d :: () -> Type -> 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)) = CoendLimit d