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

OAlg.Limes.ProductsAndSums

Contents

Products
- Construction
  - Orientation
Sums
- Duality
- Construction
  - Orientation

Description

products and sums, i.e. limits of Diagram Discrete.

Synopsis

type Products (n :: N') = ProductsG Cone Diagram n
type ProductsG (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 'Discrete n N0
type Product (n :: N') = ProductG Cone Diagram n
type ProductG (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 'Discrete n N0
type ProductCone (n :: N') = ProductConic Cone Diagram n
type ProductConic (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 'Discrete n N0
type ProductDiagram (n :: N') = ProductDiagrammatic Diagram n
type ProductDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d 'Discrete n N0
prdDiagram :: forall x d (n :: N'). (Oriented x, Diagrammatic d) => d ('Star 'From) (n + 1) n x -> ProductDiagram n x
prdCone :: forall x d (n :: N'). (Multiplicative x, Diagrammatic d) => d ('Star 'From) (n + 1) n x -> ProductCone n x
products :: forall x (n :: N'). Multiplicative x => Products N0 x -> Products N2 x -> Products n x
products0 :: Multiplicative x => TerminalPoint x -> Products N0 x
products1 :: Multiplicative x => Products N1 x
products2 :: forall x (n :: N'). Multiplicative x => Products N2 x -> Products (n + 2) x
prdConeOrnt :: forall p (n :: N'). Entity p => p -> FinList n p -> ProductCone n (Orientation p)
productOrnt :: forall p (n :: N'). Entity p => p -> FinList n p -> Product n (Orientation p)
productsOrnt :: forall p (n :: N'). Entity p => p -> Products n (Orientation p)
type Sums (n :: N') = SumsG Cone Diagram n
type SumsG (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 'Discrete n N0
type Sum (n :: N') = SumG Cone Diagram n
type SumG (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 'Discrete n N0
type SumCone (n :: N') = SumConic Cone Diagram n
type SumConic (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 'Discrete n N0
type SumDiagram (n :: N') = SumDiagrammatic Diagram n
type SumDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d 'Discrete n N0
type DualisableGDiscrete (p :: Perspective) (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 'Discrete n N0
coProducts :: forall x o (n :: N'). (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => Products n x -> Sums n (o x)
coProductsG :: 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, DualisableGDiscrete 'Projective o c d n) => ProductsG c d n x -> SumsG c d n (o x)
sumDiagram :: forall a (n :: N'). Oriented a => Diagram ('Star 'To) (n + 1) n a -> SumDiagram n a
sumCone :: forall a (n :: N'). Multiplicative a => Diagram ('Star 'To) (n + 1) n a -> SumCone n a
sums :: forall a (n :: N'). Multiplicative a => Sums N0 a -> Sums N2 a -> Sums n a
sums' :: forall a p (n :: N'). Multiplicative a => p n -> Sums N0 a -> Sums N2 a -> Sums n a
sums0 :: Multiplicative x => InitialPoint x -> Sums N0 x
sums1 :: Multiplicative x => Sums N1 x
sums2 :: forall a (n :: N'). Multiplicative a => Sums N2 a -> Sums (n + 2) a
sumConeOrnt :: forall p (n :: N'). Entity p => p -> FinList n p -> SumCone n (Orientation p)
sumOrnt :: forall p (n :: N'). Entity p => p -> FinList n p -> Sum n (Orientation p)
sumsOrnt :: forall p (n :: N'). Entity p => p -> Sums n (Orientation p)

Products

type Products (n :: N') = ProductsG Cone Diagram n Source #

products for a Multiplicative structure.

type ProductsG (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 'Discrete n N0 Source #

generic products for a Multiplicative structure.

type Product (n :: N') = ProductG Cone Diagram n Source #

product as a Limes.

type ProductG (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 'Discrete n N0 Source #

generic product as a LimesG.

type ProductCone (n :: N') = ProductConic Cone Diagram n Source #

Cone for a product.

type ProductConic (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 'Discrete n N0 Source #

Conic object for a product.

type ProductDiagram (n :: N') = ProductDiagrammatic Diagram n Source #

Diagram for a product.

type ProductDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d 'Discrete n N0 Source #

Diagrammatic object for a product.

Construction

prdDiagram :: forall x d (n :: N'). (Oriented x, Diagrammatic d) => d ('Star 'From) (n + 1) n x -> ProductDiagram n x Source #

the underlying product diagram.

prdCone :: forall x d (n :: N'). (Multiplicative x, Diagrammatic d) => d ('Star 'From) (n + 1) n x -> ProductCone n x Source #

the product cone.

products :: forall x (n :: N'). Multiplicative x => Products N0 x -> Products N2 x -> Products n x Source #

products of n points given by products of zero and two points.

products0 :: Multiplicative x => TerminalPoint x -> Products N0 x Source #

products of zero points given by a terminal point.

products1 :: Multiplicative x => Products N1 x Source #

products of one point, i.e. Minima.

products2 :: forall x (n :: N'). Multiplicative x => Products N2 x -> Products (n + 2) x Source #

products of at least two points given by products of two points.

Orientation

prdConeOrnt :: forall p (n :: N'). Entity p => p -> FinList n p -> ProductCone n (Orientation p) Source #

product cone for Orientation.

productOrnt :: forall p (n :: N'). Entity p => p -> FinList n p -> Product n (Orientation p) Source #

product for Orientation.

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

products for Orientation.

Sums

type Sums (n :: N') = SumsG Cone Diagram n Source #

sums for a Multiplicative structure.

type SumsG (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 'Discrete n N0 Source #

generic sums for a Multiplicative structure.

type Sum (n :: N') = SumG Cone Diagram n Source #

sum as a Limes.

type SumG (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 'Discrete n N0 Source #

generic sum as a LimesG.

type SumCone (n :: N') = SumConic Cone Diagram n Source #

Cone for a sum.

type SumConic (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 'Discrete n N0 Source #

Conic object for a sum.

type SumDiagram (n :: N') = SumDiagrammatic Diagram n Source #

Diagram for a sum.

type SumDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') = d 'Discrete n N0 Source #

Diagrammatic object for a sum.

Duality

type DualisableGDiscrete (p :: Perspective) (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 'Discrete n N0 Source #

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

coProducts :: forall x o (n :: N'). (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => Products n x -> Sums n (o x) Source #

the co-object of Products.

coProductsG :: 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, DualisableGDiscrete 'Projective o c d n) => ProductsG c d n x -> SumsG c d n (o x) Source #

the co-object of ProductsG.

Construction

sumDiagram :: forall a (n :: N'). Oriented a => Diagram ('Star 'To) (n + 1) n a -> SumDiagram n a Source #

the underlying sum diagram given by a sink diagram.

sumCone :: forall a (n :: N'). Multiplicative a => Diagram ('Star 'To) (n + 1) n a -> SumCone n a Source #

the sum cone given by a sink diagram.

sums :: forall a (n :: N'). Multiplicative a => Sums N0 a -> Sums N2 a -> Sums n a Source #

sums of n points given by sums of zero and two points.

sums' :: forall a p (n :: N'). Multiplicative a => p n -> Sums N0 a -> Sums N2 a -> Sums n a Source #

sums given by a proxy type for n.

sums0 :: Multiplicative x => InitialPoint x -> Sums N0 x Source #

sums of zero points given by a initial point.

sums1 :: Multiplicative x => Sums N1 x Source #

sums of one point, i.e. Maxima.

sums2 :: forall a (n :: N'). Multiplicative a => Sums N2 a -> Sums (n + 2) a Source #

sums of at least two points given by sums of two points.

Orientation

sumConeOrnt :: forall p (n :: N'). Entity p => p -> FinList n p -> SumCone n (Orientation p) Source #

sum cone for Orientation.

sumOrnt :: forall p (n :: N'). Entity p => p -> FinList n p -> Sum n (Orientation p) Source #

sum for Orientation.

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

sums for Orientation.