OAlg.Limes.Limits.Core

Contents

Description

basic definition for a LimesG of diagrammatic object.

Synopsis

limes :: 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. LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
newtype LimitsG (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 = LimitsG (d t n m x -> LimesG c s p d t n m x)
type Limits s (p :: Perspective) = LimitsG Cone s p Diagram
limesCone :: 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 => LimitsG c s p d t n m x -> d t n m x -> LimesG Cone s p d t n m x
limitsCone :: 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. Conic c => LimitsG c s p d t n m x -> LimitsG Cone s p d t n m x
lmsMltPrjOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N'). Entity p => p -> Limits Mlt 'Projective t n m (Orientation p)
lmsMltInjOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N'). Entity p => p -> Limits Mlt 'Injective t n m (Orientation p)

Limits

limes :: 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. LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x Source #

the limes over the given diagram.

limes of a diagrammatic object, i.e. assigning to each diagrammatic object d a limes over the d.

Property Let l be in LimitsG c s p d t n m x for a Conic c and a Diagrammatic d, then holds:

Constructors

LimitsG (d t n m x -> LimesG c s p d t n m x)

Instances details

NaturalConicBi (Inv2 h) c s p d t n m => ApplicativeG (SDualBi (LimitsG c s p d t n m)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Limes.Limits.Duality Methods amapG :: Inv2 h x y -> SDualBi (LimitsG c s p d t n m) x -> SDualBi (LimitsG c s p d t n m) y Source #
NaturalConicBi (Inv2 h) c s p d t n m => FunctorialG (SDualBi (LimitsG c s p d t n m)) (Inv2 h) (->) Source #
Instance details Defined in OAlg.Limes.Limits.Duality
(Conic c, Diagrammatic d, XStandardEligibleConeG c s p d t n m x, XStandardEligibleConeFactorG c s p d t n m x, XStandard (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 (LimitsG c s p d t n m x) Source #
Instance details Defined in OAlg.Limes.Limits.Proposition Methods valid :: LimitsG c s p d t n m x -> Statement Source #
type Dual1 (LimitsG c s p d t n m :: Type -> Type) Source #
Instance details Defined in OAlg.Limes.Limits.Duality type Dual1 (LimitsG c s p d t n m :: Type -> Type) = LimitsG c s (Dual p) d (Dual t) n m

limits for Cones over Diagrams.

limesCone :: 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 => LimitsG c s p d t n m x -> d t n m x -> LimesG Cone s p d t n m x Source #

the underlying limes according to Cone , given by a diagrammatic object of d t n m x.

limitsCone :: 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. Conic c => LimitsG c s p d t n m x -> LimitsG Cone s p d t n m x Source #

the underlying limits according to Cone.

Constructions

projective limits for Multiplicative structures over Orientation p .

injective limits for Multiplicative structures over Orientation p.