Safe Haskell	None
Language	GHC2024

Proarrow.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
type O1 = 'L '() :: COPRODUCT () k
type O2 = 'R '() :: COPRODUCT j ()
type At1 (d :: k +-> COPRODUCT () k1) = d %% (O1 :: COPRODUCT () k1)
type At2 (d :: k +-> COPRODUCT j ()) = d %% (O2 :: COPRODUCT j ())
data family CoproductColimit :: (k +-> COPRODUCT () ()) -> () +-> k
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) '()
newtype AnyColimit (j :: k -> k1 -> Type) (a :: k) (b :: k1) = AnyColimit (j a b)
data Lan (j :: a +-> i) (d :: Type +-> i) (a1 :: a) where
- Lan :: forall {a} {i} (j :: a +-> i) (b :: i) (a1 :: a) (d :: Type +-> i). j b a1 -> (d %% b) -> Lan j d a1

Documentation

type Unweighted = TerminalProfunctor :: k -> j -> Type 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

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 #
HasInitialObject k => HasColimits (Unweighted :: VOID -> () -> Type) k Source Github #
Instance details Defined in Proarrow.Colimit Methods colimit :: forall (d :: k +-> VOID). Corepresentable d => ((Unweighted :: VOID -> () -> Type) :.: Colimit (Unweighted :: VOID -> () -> Type) d) :~> d Source Github # colimitUniv :: forall (d :: k +-> VOID) (p :: k +-> ()). (Corepresentable d, Profunctor p) => (((Unweighted :: VOID -> () -> Type) :.: p) :~> d) -> p :~> Colimit (Unweighted :: VOID -> () -> 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 #
CategoryOf k => HasColimits (Hom :: (OPPOSITE k, k) -> () -> Type) Type Source Github #
Instance details Defined in Proarrow.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 Github # 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 Github #
HasBinaryCoproducts k => HasColimits (Unweighted :: COPRODUCT () () -> () -> Type) k Source Github #
Instance details Defined in Proarrow.Colimit Methods colimit :: forall (d :: k +-> COPRODUCT () ()). Corepresentable d => ((Unweighted :: COPRODUCT () () -> () -> Type) :.: Colimit (Unweighted :: COPRODUCT () () -> () -> Type) d) :~> d Source Github # colimitUniv :: forall (d :: k +-> COPRODUCT () ()) (p :: k +-> ()). (Corepresentable d, Profunctor p) => (((Unweighted :: COPRODUCT () () -> () -> Type) :.: p) :~> d) -> p :~> Colimit (Unweighted :: COPRODUCT () () -> () -> Type) d Source Github #

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 #

type O1 = 'L '() :: COPRODUCT () k Source Github #

type O2 = 'R '() :: COPRODUCT j () Source Github #

type At1 (d :: k +-> COPRODUCT () k1) = d %% (O1 :: COPRODUCT () k1) Source Github #

type At2 (d :: k +-> COPRODUCT j ()) = d %% (O2 :: COPRODUCT j ()) Source Github #

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

Instances

Instances details

(HasBinaryCoproducts k, Corepresentable d) => FunctorForRep (CoproductColimit d :: () +-> 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 :: () +-> k) @ '() Source Github #
Instance details Defined in Proarrow.Colimit type (CoproductColimit d :: () +-> k) @ '() = At1 d \|\| At2 d

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

Instances

Instances details

(Corepresentable d, Copowered Type k) => FunctorForRep (CopowerLimit n d :: () +-> 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 :: () +-> k) @ '() Source Github #
Instance details Defined in Proarrow.Colimit type (CopowerLimit n d :: () +-> 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)) -> () +-> Type Source Github #

Instances

Instances details

Corepresentable d => FunctorForRep (CoendLimit d :: () +-> 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 :: () +-> Type) @ '() Source Github #
Instance details Defined in Proarrow.Colimit type (CoendLimit d :: () +-> Type) @ '() = Coend d

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

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 Github #
Instance details Defined in Proarrow.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 Github # lmap :: forall (c :: (OPPOSITE k, k)) (a :: (OPPOSITE k, k)) (b :: ()). (c ~> a) -> Hom a b -> Hom c b Source Github # rmap :: forall (b :: ()) (d :: ()) (a :: (OPPOSITE k, k)). (b ~> d) -> Hom a b -> Hom a d Source Github # (\\) :: forall (a :: (OPPOSITE k, k)) (b :: ()) r. ((Ob a, Ob b) => r) -> Hom a b -> r Source Github #
CategoryOf k => HasColimits (Hom :: (OPPOSITE k, k) -> () -> Type) Type Source Github #
Instance details Defined in Proarrow.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 Github # 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 Github #
type Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) (d :: Type +-> (OPPOSITE k, k)) Source Github #
Instance details Defined in Proarrow.Colimit type Colimit (Hom :: (OPPOSITE k, k) -> () -> Type) (d :: Type +-> (OPPOSITE k, k)) = Corep (CoendLimit 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) = Costar (Lan j d)

data Lan (j :: a +-> i) (d :: Type +-> i) (a1 :: a) where Source Github #

Constructors

Lan :: forall {a} {i} (j :: a +-> i) (b :: i) (a1 :: a) (d :: Type +-> i). j b a1 -> (d %% b) -> Lan j d a1

Instances

Instances details

(Profunctor j, Corepresentable d) => Functor (Lan j d :: k1 -> Type) Source Github #
Instance details Defined in Proarrow.Colimit Methods map :: forall (a :: k1) (b :: k1). (a ~> b) -> Lan j d a ~> Lan j d b Source Github #