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

OAlg.Limes.MinimaAndMaxima

Contents

Minima
Maxima
Duality

Description

minima and maxima within a Multiplicative structure, i.e. limits of Diagram (Chain t).

Synopsis

type Minima (t :: Site) (n :: N') = MinimaG Cone Diagram t n
type MinimaG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = LimitsG c Mlt 'Projective d ('Chain t) (n + 1) n
type Minimum (t :: Site) (n :: N') = MinimumG Cone Diagram t n
type MinimumG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = LimesG c Mlt 'Projective d ('Chain t) (n + 1) n
type MinimumCone (t :: Site) (n :: N') = MinimumConic Cone Diagram t n
type MinimumConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = c Mlt 'Projective d ('Chain t) (n + 1) n
type MinimumDiagram (t :: Site) (n :: N') = MinimumDiagrammatic Diagram t n
type MinimumDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = d ('Chain t) (n + 1) n
minimaTo :: forall x (n :: N'). Multiplicative x => Minima 'To n x
minimaGTo :: forall x (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Multiplicative x, Diagrammatic d) => MinimaG Cone d 'To n x
minimaFrom :: forall x (n :: N'). Multiplicative x => Minima 'From n x
minimaGFrom :: forall x (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Multiplicative x, Diagrammatic d) => MinimaG Cone d 'From n x
type Maxima (t :: Site) (n :: N') = MaximaG Cone Diagram t n
type MaximaG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = LimitsG c Mlt 'Injective d ('Chain t) (n + 1) n
type Maximum (t :: Site) (n :: N') = MaximumG Cone Diagram t n
type MaximumG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = LimesG c Mlt 'Injective d ('Chain t) (n + 1) n
type MaximumCone (t :: Site) (n :: N') = MaximumConic Cone Diagram t n
type MaximumConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = c Mlt 'Injective d ('Chain t) (n + 1) n
type MaximumDiagram (t :: Site) (n :: N') = MaximumDiagrammatic Diagram t n
type MaximumDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = d ('Chain t) (n + 1) n
maximaTo :: forall x (n :: N'). Multiplicative x => Maxima 'To n x
maximaFrom :: forall x (n :: N'). Multiplicative x => Maxima 'From n x
maximaTo' :: forall x p (n :: N') f. Multiplicative x => p n -> f x -> Maxima 'To n x
maximaFrom' :: forall x p (n :: N') f. Multiplicative x => p n -> f x -> Maxima 'From n x
type DualisableGChain (p :: Perspective) (t :: Site) (o :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = NaturalConicBi (IsoO Mlt o) c Mlt p d ('Chain t) (n + 1) n
coMinimaGTo :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Multiplicative x, TransformableGRefl o Mlt, DualisableGChain 'Projective 'To o c d n) => MinimaG c d 'To n x -> MaximaG c d 'From n (o x)
coMinimaGFrom :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Multiplicative x, TransformableGRefl o Mlt, DualisableGChain 'Projective 'From o c d n) => MinimaG c d 'From n x -> MaximaG c d 'To n (o x)

Minima

type Minima (t :: Site) (n :: N') = MinimaG Cone Diagram t n Source #

minima for a Multiplicative structure.

type MinimaG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = LimitsG c Mlt 'Projective d ('Chain t) (n + 1) n Source #

generic minima for a Multiplicative structure.

type Minimum (t :: Site) (n :: N') = MinimumG Cone Diagram t n Source #

minimum as Limes.

type MinimumG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = LimesG c Mlt 'Projective d ('Chain t) (n + 1) n Source #

generic minimum as LimesG.

type MinimumCone (t :: Site) (n :: N') = MinimumConic Cone Diagram t n Source #

Cone for a minimum.

type MinimumConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = c Mlt 'Projective d ('Chain t) (n + 1) n Source #

Conic object for a minimum.

type MinimumDiagram (t :: Site) (n :: N') = MinimumDiagrammatic Diagram t n Source #

Diagram for a minimum.

type MinimumDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = d ('Chain t) (n + 1) n Source #

Diagrammatic object for a minimum.

minimaTo :: forall x (n :: N'). Multiplicative x => Minima 'To n x Source #

minima according to Chain To.

minimaGTo :: forall x (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Multiplicative x, Diagrammatic d) => MinimaG Cone d 'To n x Source #

generic minima according to Chain To.

minimaFrom :: forall x (n :: N'). Multiplicative x => Minima 'From n x Source #

minima according to Chain From.

minimaGFrom :: forall x (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Multiplicative x, Diagrammatic d) => MinimaG Cone d 'From n x Source #

generic minima according to Chain From.

Maxima

type Maxima (t :: Site) (n :: N') = MaximaG Cone Diagram t n Source #

maxima for a Multiplicative structure.

type MaximaG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = LimitsG c Mlt 'Injective d ('Chain t) (n + 1) n Source #

generic maxima for a Multiplicative structure.

type Maximum (t :: Site) (n :: N') = MaximumG Cone Diagram t n Source #

maximum as Limes.

type MaximumG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = LimesG c Mlt 'Injective d ('Chain t) (n + 1) n Source #

generic maximum as LimesG.

type MaximumCone (t :: Site) (n :: N') = MaximumConic Cone Diagram t n Source #

Cone for a maximum.

type MaximumConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = c Mlt 'Injective d ('Chain t) (n + 1) n Source #

Conic object for a maximum.

type MaximumDiagram (t :: Site) (n :: N') = MaximumDiagrammatic Diagram t n Source #

Diagram for a maximum.

type MaximumDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: Site) (n :: N') = d ('Chain t) (n + 1) n Source #

Diagrammatic object for a maximum.

maximaTo :: forall x (n :: N'). Multiplicative x => Maxima 'To n x Source #

maxima according to Chain To.

maximaFrom :: forall x (n :: N'). Multiplicative x => Maxima 'From n x Source #

maxima according to Chain From.

maximaTo' :: forall x p (n :: N') f. Multiplicative x => p n -> f x -> Maxima 'To n x Source #

maxima according to Chain To given by two proxy types.

maximaFrom' :: forall x p (n :: N') f. Multiplicative x => p n -> f x -> Maxima 'From n x Source #

maxima according to Chain From given by two proxy types.

Duality

type DualisableGChain (p :: Perspective) (t :: Site) (o :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = NaturalConicBi (IsoO Mlt o) c Mlt p d ('Chain t) (n + 1) n Source #

type for dualisable generic limits of Conic objects over Chain Diagrammatic objects.

coMinimaGTo :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Multiplicative x, TransformableGRefl o Mlt, DualisableGChain 'Projective 'To o c d n) => MinimaG c d 'To n x -> MaximaG c d 'From n (o x) Source #

the co-object of MinimaG.

coMinimaGFrom :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N'). (Multiplicative x, TransformableGRefl o Mlt, DualisableGChain 'Projective 'From o c d n) => MinimaG c d 'From n x -> MaximaG c d 'To n (o x) Source #

the co-object of MinimaG.