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

OAlg.Limes.PullbacksAndPushouts

Contents

Pullbacks
- Construction
  - Orientation
Pushouts
- Construction
  - Orientation
Duality

Description

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

Synopsis

type Pullbacks n = Limits Mlt Projective (Star To) (n + 1) n
type Pullback n = Limes Mlt Projective (Star To) (n + 1) n
type PullbackCone n = Cone Mlt Projective (Star To) (n + 1) n
type PullbackDiagram n = Diagram (Star To) (n + 1) n
pullbacks :: Multiplicative a => Pullbacks N2 a -> Pullbacks n a
pullbacks0 :: Multiplicative a => Pullbacks N0 a
pullbacks1 :: Multiplicative a => Pullbacks N1 a
plbPrdEql2 :: Multiplicative a => Products N2 a -> Equalizers N2 a -> Pullbacks N2 a
pullbacksOrnt :: Entity p => p -> Pullbacks n (Orientation p)
type Pushouts n = Limits Mlt Injective (Star From) (n + 1) n
type Pushout n = Limes Mlt Injective (Star From) (n + 1) n
type PushoutCone n = Cone Mlt Injective (Star From) (n + 1) n
type PushoutDiagram n = Diagram (Star From) (n + 1) n
pushouts :: Multiplicative a => Pushouts N2 a -> Pushouts n a
pushouts' :: Multiplicative a => p n -> Pushouts N2 a -> Pushouts n a
pshSumCoeql2 :: Multiplicative a => Sums N2 a -> Coequalizers N2 a -> Pushouts N2 a
pushoutsOrnt :: Entity p => p -> Pushouts n (Orientation p)
pshLimitsDuality :: Multiplicative a => LimitsDuality Mlt (Pushouts n) (Pullbacks n) a

Pullbacks

type Pullbacks n = Limits Mlt Projective (Star To) (n + 1) n Source #

pullbacks for Multiplicative structures.

type Pullback n = Limes Mlt Projective (Star To) (n + 1) n Source #

pullback as Limes.

type PullbackCone n = Cone Mlt Projective (Star To) (n + 1) n Source #

Cone for a pullback.

type PullbackDiagram n = Diagram (Star To) (n + 1) n Source #

Diagram for a pullback.

Construction

pullbacks :: Multiplicative a => Pullbacks N2 a -> Pullbacks n a Source #

promotion of pullbacks.

image pullback

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

pullbacks for zero arrows as Minima.

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

pullbacks of one arrow, i.e. Minima.

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

pullbacks given by products and equalizers.

Orientation

pullbacksOrnt :: Entity p => p -> Pullbacks n (Orientation p) Source #

pullbacks for Orientation.

Pushouts

type Pushouts n = Limits Mlt Injective (Star From) (n + 1) n Source #

pushouts for a Multiplicative structures.

type Pushout n = Limes Mlt Injective (Star From) (n + 1) n Source #

pushout as Limes.

type PushoutCone n = Cone Mlt Injective (Star From) (n + 1) n Source #

Cone for a pushout.

type PushoutDiagram n = Diagram (Star From) (n + 1) n Source #

Diagram for a pushout.

Construction

pushouts :: Multiplicative a => Pushouts N2 a -> Pushouts n a Source #

promotion of pushouts.

pushouts' :: Multiplicative a => p n -> Pushouts N2 a -> Pushouts n a Source #

pushouts given by a proxy for n.

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

pushouts given by sums and coequalizers.

Orientation

pushoutsOrnt :: Entity p => p -> Pushouts n (Orientation p) Source #

pushouts for Orientation.

Duality

pshLimitsDuality :: Multiplicative a => LimitsDuality Mlt (Pushouts n) (Pullbacks n) a Source #

duality between pushouts and pullbacks.