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

OAlg.Limes.Definition.Core

Contents

Limes
Constructions

Description

basic definition of a Limes over a Diagrammatic object yielding a Conic object.

Synopsis

type Limes s (p :: Perspective) = LimesG Cone s p Diagram
data LimesG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x where
- LimesProjective :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. c s 'Projective d t n m x -> (Cone s 'Projective d t n m x -> x) -> LimesG c s 'Projective d t n m x
- LimesInjective :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. c s 'Injective d t n m x -> (Cone s 'Injective d t n m x -> x) -> LimesG c s 'Injective d t n m x
universalCone :: forall c s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. LimesG c s p d t n m x -> c s p d t n m x
universalFactor :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalDiagram :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) d (t :: DiagramType) (n :: N') (m :: N') x. Conic c => LimesG c s p d t n m x -> d t n m x
eligibleCone :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x s (p :: Perspective). (Conic c, Eq (d t n m x)) => LimesG c s p d t n m x -> Cone s p d t n m x -> Bool
eligibleFactor :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') x. (Conic c, Diagrammatic d) => LimesG c s p d t n m x -> Cone s p d t n m x -> x -> Bool
lmDiagramTypeRefl :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') x. (Conic c, Diagrammatic d) => LimesG c s p d t n m x -> Dual (Dual t) :~: t
lmMltPrjOrnt :: forall p x (t :: DiagramType) (n :: N') (m :: N'). (Entity p, x ~ Orientation p) => p -> Diagram t n m x -> Limes Mlt 'Projective t n m x
lmMltInjOrnt :: forall p x (t :: DiagramType) (n :: N') (m :: N'). (Entity p, x ~ Orientation p) => p -> Diagram t n m x -> Limes Mlt 'Injective t n m x

Limes

type Limes s (p :: Perspective) = LimesG Cone s p Diagram Source #

limes for Cones over Diagrams.

data LimesG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x where Source #

limes of a Diagrammatic object, i.e. a distinguished Conic object over a the underlying diagrammaticObject having the following universal property

Property Let Conic c, Diagrammatic _d, Multiplicative x and l in LimesG s p c d t n m x then holds: Let u = universalCone l in

For all c in Cone s p d t n m x with eligibleCone l c holds: Let f = universalFactor l c in
1. eligibleFactor l c f.
2. For all x in x with eligibleFactor l c x holds: x == f.

Note

As the function universalFactor l for a given limes l is uniquely determined by the underlying cone of l, it is permissible to test equality of two limits just by there underling cones. In every computation equal limits can be safely replaced by each other.
It is not required that the evaluation of universal factor on a non eligible cone yield an exception! The implementation of the general algorithms for limits do not check for eligibility.

Constructors

LimesProjective :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. c s 'Projective d t n m x -> (Cone s 'Projective d t n m x -> x) -> LimesG c s 'Projective d t n m x
LimesInjective :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. c s 'Injective d t n m x -> (Cone s 'Injective d t n m x -> x) -> LimesG c s 'Injective d t n m x

Instances

Instances details

NaturalConicBi (Inv2 h) c s p d t n m => ApplicativeG (SDualBi (LimesG c s p d t n m)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Limes.Definition.Duality Methods amapG :: Inv2 h x y -> SDualBi (LimesG c s p d t n m) x -> SDualBi (LimesG c s p d t n m) y Source #
NaturalConicBi (Inv2 h) c s p d t n m => FunctorialG (SDualBi (LimesG c s p d t n m)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Limes.Definition.Duality
Show (c s p d t n m x) => Show (LimesG c s p d t n m x) Source #
Instance details Defined in OAlg.Limes.Definition.Core Methods showsPrec :: Int -> LimesG c s p d t n m x -> ShowS # show :: LimesG c s p d t n m x -> String # showList :: [LimesG c s p d t n m x] -> ShowS #
(Conic c, Diagrammatic d, XStandardEligibleConeG c s p d t n m x, XStandardEligibleConeFactorG c s p d t n m x, Show (c s p d t n m x), Validable (c s p d t n m x), Entity (d t n m x), Entity x) => Validable (LimesG c s p d t n m x) Source #
Instance details Defined in OAlg.Limes.Definition.Proposition Methods valid :: LimesG c s p d t n m x -> Statement Source #
type Dual1 (LimesG c s p d t n m :: Type -> Type) Source #
Instance details Defined in OAlg.Limes.Definition.Duality type Dual1 (LimesG c s p d t n m :: Type -> Type) = LimesG c s (Dual p) d (Dual t) n m

universalCone :: forall c s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. LimesG c s p d t n m x -> c s p d t n m x Source #

the unviersal Conic object given by the LimesG.

universalFactor :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. LimesG c s p d t n m x -> Cone s p d t n m x -> x Source #

the unviersal factor given by the LimesG.

universalDiagram :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) d (t :: DiagramType) (n :: N') (m :: N') x. Conic c => LimesG c s p d t n m x -> d t n m x Source #

the diagrammatic object given by the universal cone of the LimesG.

eligibleCone :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x s (p :: Perspective). (Conic c, Eq (d t n m x)) => LimesG c s p d t n m x -> Cone s p d t n m x -> Bool Source #

eligibility of a Cone according to the given LimesG.

eligibleFactor :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') x. (Conic c, Diagrammatic d) => LimesG c s p d t n m x -> Cone s p d t n m x -> x -> Bool Source #

eligibility of a factor according to the given LimesG and Cone,

lmDiagramTypeRefl :: forall (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') x. (Conic c, Diagrammatic d) => LimesG c s p d t n m x -> Dual (Dual t) :~: t Source #

reflexivity for DiagramType.

Constructions

lmMltPrjOrnt :: forall p x (t :: DiagramType) (n :: N') (m :: N'). (Entity p, x ~ Orientation p) => p -> Diagram t n m x -> Limes Mlt 'Projective t n m x Source #

projective limes on oriented structures.

lmMltInjOrnt :: forall p x (t :: DiagramType) (n :: N') (m :: N'). (Entity p, x ~ Orientation p) => p -> Diagram t n m x -> Limes Mlt 'Injective t n m x Source #

injective limes on oriented structures.