| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
OAlg.Limes.EqualizersAndCoequalizers
Synopsis
- type Equalizers (n :: N') = EqualizersG Cone Diagram n
- type EqualizersG (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 ('Parallel 'LeftToRight) N2 n
- type Equalizer (n :: N') = EqualizerG Cone Diagram n
- type EqualizerG (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 ('Parallel 'LeftToRight) N2 n
- type EqualizerCone (n :: N') = EqualizerConic Cone Diagram n
- type EqualizerConic (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 ('Parallel 'LeftToRight) N2 n
- type EqualizerDiagram (n :: N') = EqualizerDiagrammatic Diagram n
- type EqualizerDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Parallel 'LeftToRight) N2 n
- equalizers :: forall x (n :: N'). Multiplicative x => Products N2 x -> Equalizers N2 x -> Equalizers n x
- equalizers0 :: Multiplicative x => Products N2 x -> Equalizers N0 x
- equalizers1 :: Multiplicative x => Equalizers N1 x
- equalizers2 :: forall x (n :: N'). Multiplicative x => Equalizers N2 x -> Equalizers (n + 2) x
- equalizersOrnt :: forall p (n :: N'). Entity p => p -> Equalizers n (Orientation p)
- type Coequalizers (n :: N') = CoequalizersG Cone Diagram n
- type CoequalizersG (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 ('Parallel 'RightToLeft) N2 n
- type Coequalizer (n :: N') = CoequalizerG Cone Diagram n
- type CoequalizerG (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 ('Parallel 'RightToLeft) N2 n
- type CoequalizerCone (n :: N') = CoequalizerConic Cone Diagram n
- type CoequalizerConic (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 ('Parallel 'RightToLeft) N2 n
- type CoequalizerDiagram (n :: N') = CoequalizerDiagrammatic Diagram n
- type CoequalizerDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Parallel 'RightToLeft) N2 n
- coequalizers :: forall x (n :: N'). Multiplicative x => Sums N2 x -> Coequalizers N2 x -> Coequalizers n x
- coequalizers' :: forall x p (n :: N'). Multiplicative x => p n -> Sums N2 x -> Coequalizers N2 x -> Coequalizers n x
- coequalizersOrnt :: forall p (n :: N'). Entity p => p -> Coequalizers n (Orientation p)
Equalizers
type Equalizers (n :: N') = EqualizersG Cone Diagram n Source #
equalizers for a Multiplicative structures.
type EqualizersG (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 ('Parallel 'LeftToRight) N2 n Source #
generic equalizers for a Multiplicative structures.
type EqualizerG (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 ('Parallel 'LeftToRight) N2 n Source #
generic equalizer as LimesG.
type EqualizerCone (n :: N') = EqualizerConic Cone Diagram n Source #
Cone for a equalizer.
type EqualizerConic (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 ('Parallel 'LeftToRight) N2 n Source #
Conic object for a equalizer.
type EqualizerDiagram (n :: N') = EqualizerDiagrammatic Diagram n Source #
Diagram for a equalizer.
type EqualizerDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Parallel 'LeftToRight) N2 n Source #
Diagrammatic object for a equalizer.
Construction
equalizers :: forall x (n :: N'). Multiplicative x => Products N2 x -> Equalizers N2 x -> Equalizers n x Source #
equalizers of n arrows given by products of two points and equalizers of two arrows.
equalizers0 :: Multiplicative x => Products N2 x -> Equalizers N0 x Source #
the induced equalizers of zero parallel arrows.
equalizers1 :: Multiplicative x => Equalizers N1 x Source #
equalizers of one parallel arrow, i.e. Minima.
equalizers2 :: forall x (n :: N'). Multiplicative x => Equalizers N2 x -> Equalizers (n + 2) x Source #
promoting equalizers.
Orientation
equalizersOrnt :: forall p (n :: N'). Entity p => p -> Equalizers n (Orientation p) Source #
equalizers for Orientation
Coequalizers
type Coequalizers (n :: N') = CoequalizersG Cone Diagram n Source #
coequalizers for a Multiplicative structures.
type CoequalizersG (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 ('Parallel 'RightToLeft) N2 n Source #
generic coequalizers for a Multiplicative structures.
type Coequalizer (n :: N') = CoequalizerG Cone Diagram n Source #
coequalizer as Limes.
type CoequalizerG (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 ('Parallel 'RightToLeft) N2 n Source #
generic coequalizer as LimesG.
type CoequalizerCone (n :: N') = CoequalizerConic Cone Diagram n Source #
Cone for a coequalizer.
type CoequalizerConic (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 ('Parallel 'RightToLeft) N2 n Source #
Conic object for a coequalizer.
type CoequalizerDiagram (n :: N') = CoequalizerDiagrammatic Diagram n Source #
Diagram for a coequalizer.
type CoequalizerDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d ('Parallel 'RightToLeft) N2 n Source #
Diagrammatic object for a coequalizer.
Construction
coequalizers :: forall x (n :: N'). Multiplicative x => Sums N2 x -> Coequalizers N2 x -> Coequalizers n x Source #
coequalizers of n arrows given by sums of two points and coequalizers of two arrows.
coequalizers' :: forall x p (n :: N'). Multiplicative x => p n -> Sums N2 x -> Coequalizers N2 x -> Coequalizers n x Source #
coequalizers given by a proxy for n.
Orientation
coequalizersOrnt :: forall p (n :: N'). Entity p => p -> Coequalizers n (Orientation p) Source #
coequalizers for Orientation.