Safe Haskell	None
Language	Haskell2010

Proarrow.Category.Colimit

Synopsis

type Unweighted = TerminalProfunctor :: k -> j -> Type
class Representable (Colimit j1 d) => IsRepresentableColimit (j1 :: j +-> i) (d :: i +-> k)
class (forall (d :: i +-> k). Representable d => IsRepresentableColimit j d) => HasColimits (j :: a +-> i) k where
- type Colimit (j :: a +-> i) (d :: i +-> k) :: a +-> k
- colimit :: forall (d :: i +-> k). Representable d => (d :.: j) :~> Colimit j d
- colimitUniv :: forall (d :: i +-> k) (p :: a +-> k). (Representable d, Representable p) => ((d :.: j) :~> p) -> Colimit j d :~> p
leftAdjointPreservesColimits :: forall {k} {k'} {i} {a} (f :: k +-> k') (g :: PRO k k') (d :: i +-> k) (j :: a +-> i). (Adjunction f g, Representable d, Representable f, Representable g, HasColimits j k, HasColimits j k') => (f :.: Colimit j d) :~> Colimit j (f :.: d)
leftAdjointPreservesColimitsInv :: forall {k} {k'} {i} {a} (f :: k +-> k') (d :: i +-> k) (j :: a +-> i). (Representable d, Representable f, HasColimits j k, HasColimits j k') => Colimit j (f :.: d) :~> (f :.: Colimit j d)
data InitialLimit (d :: VOID +-> k) (a :: k) (b :: ()) where
- InitialLimit :: forall {k} (d :: VOID +-> k) (a :: k). (a ~> (InitialObject :: k)) -> InitialLimit d a '()
data CoproductColimit (d :: COPRODUCT () () +-> k) (a :: k) (b :: ()) where
- CoproductColimit :: forall {k} (d :: COPRODUCT () () +-> k) (a :: k). (a ~> ((d % ('L '() :: COLLAGE (InitialProfunctor :: () -> () -> Type))) || (d % ('R '() :: COLLAGE (InitialProfunctor :: () -> () -> Type))))) -> CoproductColimit d a '()
cochoose :: forall k (d :: COPRODUCT () () +-> k) (b :: COPRODUCT () ()). (HasBinaryCoproducts k, Representable d) => Obj b -> (d % b) ~> ((d % ('L '() :: COLLAGE (InitialProfunctor :: () -> () -> Type))) || (d % ('R '() :: COLLAGE (InitialProfunctor :: () -> () -> Type))))

Documentation

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

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

Instances

Instances details

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

class (forall (d :: i +-> k). Representable d => IsRepresentableColimit j d) => HasColimits (j :: a +-> i) k where Source Comments #

profunctor-weighted colimits

Associated Types

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

Methods

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

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

Instances

Instances details

HasInitialObject k => HasColimits (Unweighted :: VOID -> () -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: VOID +-> k). Representable d => (d :.: (Unweighted :: VOID -> () -> Type)) :~> Colimit (Unweighted :: VOID -> () -> Type) d Source Comments # colimitUniv :: forall (d :: VOID +-> k) (p :: () +-> k). (Representable d, Representable p) => ((d :.: (Unweighted :: VOID -> () -> Type)) :~> p) -> Colimit (Unweighted :: VOID -> () -> Type) d :~> p Source Comments #
HasBinaryCoproducts k => HasColimits (Unweighted :: COPRODUCT () () -> () -> Type) k Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods colimit :: forall (d :: COPRODUCT () () +-> k). Representable d => (d :.: (Unweighted :: COPRODUCT () () -> () -> Type)) :~> Colimit (Unweighted :: COPRODUCT () () -> () -> Type) d Source Comments # colimitUniv :: forall (d :: COPRODUCT () () +-> k) (p :: () +-> k). (Representable d, Representable p) => ((d :.: (Unweighted :: COPRODUCT () () -> () -> Type)) :~> p) -> Colimit (Unweighted :: COPRODUCT () () -> () -> Type) d :~> p Source Comments #

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

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

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

Constructors

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

Instances

Instances details

HasInitialObject k => Profunctor (InitialLimit d :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods dimap :: forall (c :: k) (a :: k) (b :: ()) (d0 :: ()). (c ~> a) -> (b ~> d0) -> InitialLimit d a b -> InitialLimit d c d0 Source Comments # (\\) :: forall (a :: k) (b :: ()) r. ((Ob a, Ob b) => r) -> InitialLimit d a b -> r Source Comments #
HasInitialObject k => Representable (InitialLimit d :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods index :: forall (a :: k) (b :: ()). InitialLimit d a b -> a ~> (InitialLimit d % b) Source Comments # tabulate :: forall (b :: ()) (a :: k). Ob b => (a ~> (InitialLimit d % b)) -> InitialLimit d a b Source Comments # repMap :: 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 :: COPRODUCT () () +-> k) (a :: k) (b :: ()) where Source Comments #

Constructors

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

Instances

Instances details

(HasBinaryCoproducts k, Representable d) => Profunctor (CoproductColimit d :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods dimap :: forall (c :: k) (a :: k) (b :: ()) (d0 :: ()). (c ~> a) -> (b ~> d0) -> CoproductColimit d a b -> CoproductColimit d c d0 Source Comments # (\\) :: forall (a :: k) (b :: ()) r. ((Ob a, Ob b) => r) -> CoproductColimit d a b -> r Source Comments #
(HasBinaryCoproducts k, Representable d) => Representable (CoproductColimit d :: k -> () -> Type) Source Comments #
Instance details Defined in Proarrow.Category.Colimit Methods index :: forall (a :: k) (b :: ()). CoproductColimit d a b -> a ~> (CoproductColimit d % b) Source Comments # tabulate :: forall (b :: ()) (a :: k). Ob b => (a ~> (CoproductColimit d % b)) -> CoproductColimit d a b Source Comments # repMap :: 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 '() :: COLLAGE (InitialProfunctor :: () -> () -> Type))) \|\| (d % ('R '() :: COLLAGE (InitialProfunctor :: () -> () -> Type)))

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