Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	None
Language	Haskell2010

OAlg.Limes.PullbacksAndPushouts

Contents

Description

pullbacks and pushouts, i.e. limits of Diagram (Star d).

Synopsis

type Pullbacks (n :: N') = PullbacksG Cone Diagram n
type PullbacksG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimitsG c Mlt 'Projective d ('Star 'To) (n + 1) n
type Pullback (n :: N') = PullbackG Cone Diagram n
type PullbackG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimesG c Mlt 'Projective d ('Star 'To) (n + 1) n
type PullbackCone (n :: N') = PullbackConic Cone Diagram n
type PullbackConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = c Mlt 'Projective d ('Star 'To) (n + 1) n
type PullbackDiagram (n :: N') = PullbackDiagrammatic Diagram n
type PullbackDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Star 'To) (n + 1) n
pullbacks :: forall x (n :: N'). Multiplicative x => Pullbacks N2 x -> Pullbacks n x
pullbacks0 :: Multiplicative x => Pullbacks N0 x
pullbacks1 :: Multiplicative x => Pullbacks N1 x
plbPrdEql2 :: Multiplicative x => Products N2 x -> Equalizers N2 x -> Pullbacks N2 x
pullbacksOrnt :: forall p (n :: N'). Entity p => p -> Pullbacks n (Orientation p)
type Pushouts (n :: N') = PushoutsG Cone Diagram n
type PushoutsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimitsG c Mlt 'Injective d ('Star 'From) (n + 1) n
type Pushout (n :: N') = PushoutG Cone Diagram n
type PushoutG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimesG c Mlt 'Injective d ('Star 'From) (n + 1) n
type PushoutCone (n :: N') = PushoutConic Cone Diagram n
type PushoutConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = c Mlt 'Injective d ('Star 'From) (n + 1) n
type PushoutDiagram (n :: N') = PushoutDiagrammatic Diagram n
type PushoutDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Star 'From) (n + 1) n
pushouts :: forall x (n :: N'). Multiplicative x => Pushouts N2 x -> Pushouts n x
pushouts' :: forall x p (n :: N'). Multiplicative x => p n -> Pushouts N2 x -> Pushouts n x
pshSumCoeql2 :: Multiplicative x => Sums N2 x -> Coequalizers N2 x -> Pushouts N2 x
pushoutsOrnt :: forall p (n :: N'). Entity p => p -> Pushouts n (Orientation p)

Pullbacks

type Pullbacks (n :: N') = PullbacksG Cone Diagram n Source #

pullbacks for Multiplicative structures.

type PullbacksG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimitsG c Mlt 'Projective d ('Star 'To) (n + 1) n Source #

generic pullbacks for Multiplicative structures.

type Pullback (n :: N') = PullbackG Cone Diagram n Source #

pullback as PullbackG.

type PullbackG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimesG c Mlt 'Projective d ('Star 'To) (n + 1) n Source #

generic pullback as LimesG.

type PullbackCone (n :: N') = PullbackConic Cone Diagram n Source #

Cone for a pullback.

type PullbackConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = c Mlt 'Projective d ('Star 'To) (n + 1) n Source #

Conic object for a pullback.

type PullbackDiagram (n :: N') = PullbackDiagrammatic Diagram n Source #

Diagram for a pullback.

type PullbackDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Star 'To) (n + 1) n Source #

Diagrammatic object for a pullback.

Construction

pullbacks :: forall x (n :: N'). Multiplicative x => Pullbacks N2 x -> Pullbacks n x Source #

promotion of pullbacks.

image pullback

pullbacks0 :: Multiplicative x => Pullbacks N0 x Source #

pullbacks for zero arrows as Minima.

pullbacks1 :: Multiplicative x => Pullbacks N1 x Source #

pullbacks of one arrow, i.e. Minima.

plbPrdEql2 :: Multiplicative x => Products N2 x -> Equalizers N2 x -> Pullbacks N2 x Source #

pullbacks given by products and equalizers.

Orientation

pullbacksOrnt :: forall p (n :: N'). Entity p => p -> Pullbacks n (Orientation p) Source #

pullbacks for Orientation.

Pushouts

type Pushouts (n :: N') = PushoutsG Cone Diagram n Source #

pushouts for Multiplicative structures.

type PushoutsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimitsG c Mlt 'Injective d ('Star 'From) (n + 1) n Source #

generic pushouts for Multiplicative structures.

type Pushout (n :: N') = PushoutG Cone Diagram n Source #

pushout as Limes.

type PushoutG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = LimesG c Mlt 'Injective d ('Star 'From) (n + 1) n Source #

generic pushout as LimesG.

type PushoutCone (n :: N') = PushoutConic Cone Diagram n Source #

Cone for a pushout.

type PushoutConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = c Mlt 'Injective d ('Star 'From) (n + 1) n Source #

Conic object for a pushout.

type PushoutDiagram (n :: N') = PushoutDiagrammatic Diagram n Source #

Diagram for a pushout.

type PushoutDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Star 'From) (n + 1) n Source #

Diagrammatic object for a pushout.

Construction

pushouts :: forall x (n :: N'). Multiplicative x => Pushouts N2 x -> Pushouts n x Source #

promotion of pushouts.

pushouts' :: forall x p (n :: N'). Multiplicative x => p n -> Pushouts N2 x -> Pushouts n x Source #

pushouts given by a proxy for n.

pshSumCoeql2 :: Multiplicative x => Sums N2 x -> Coequalizers N2 x -> Pushouts N2 x Source #

pushouts given by sums and coequalizers.

Orientation

pushoutsOrnt :: forall p (n :: N'). Entity p => p -> Pushouts n (Orientation p) Source #

pushouts for Orientation.