OAlg.Limes.Limits

Limits of Diagrams, i.e. assigning to each diagram a Limes over the given diagram.

Limits

newtype Limits s p t n m a

limes of a diagram, i.e. assigning to each diagram a limes over the given diagram.

Property Let lms be in Limits s p t n m a and d in Diagram t n m a then holds: diagram (limes lms d) == d.

Constructors

Limits (Diagram t n m a -> Limes s p t n m a)

Instances

IsoDistributive h => Applicative1 h (Limits Dst p t n m)

Defined in OAlg.Limes.Limits

Methods

amap1 :: h a b -> Limits Dst p t n m a -> Limits Dst p t n m b

IsoMultiplicative h => Applicative1 h (Limits Mlt p t n m)

Defined in OAlg.Limes.Limits

Methods

amap1 :: h a b -> Limits Mlt p t n m a -> Limits Mlt p t n m b

(Distributive a, XStandard (Diagram t n m a), XStandardOrtPerspective p a) => Validable (Limits Dst p t n m a)

Defined in OAlg.Limes.Limits

Methods

valid :: Limits Dst p t n m a -> Statement

(Multiplicative a, XStandard (Diagram t n m a), XStandardOrtPerspective p a) => Validable (Limits Mlt p t n m a)

Defined in OAlg.Limes.Limits

Methods

valid :: Limits Mlt p t n m a -> Statement

type Dual (Limits s p t n m a :: TYPE LiftedRep)

Defined in OAlg.Limes.Limits

type Dual (Limits s p t n m a :: TYPE LiftedRep) = Limits s (Dual p) (Dual t) n m (Op a)

limes :: Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a

the limes over the given diagram.

lmsMap :: IsoOrt s h => h a b -> Limits s p t n m a -> Limits s p t n m b

mapping of limits.

Duality

lmsToOp :: LimitsDuality s f g a -> f a -> g (Op a)

to g (Op a).

lmsFromOp :: LimitsDuality s f g a -> g (Op a) -> f a

from g (Op a).

data LimitsDuality s f g a where

Op-duality between limits types.

Constructors

LimitsDuality :: ConeStruct s a -> (f a :~: Limits s p t n m a) -> (g (Op a) :~: Dual (Limits s p t n m a)) -> (Dual (Dual p) :~: p) -> (Dual (Dual t) :~: t) -> LimitsDuality s f g a

coLimits :: ConeStruct s a -> (Dual (Dual p) :~: p) -> (Dual (Dual t) :~: t) -> Limits s p t n m a -> Dual (Limits s p t n m a)

the co limits wit its inverse coLimitsInv.

coLimitsInv :: ConeStruct s a -> (Dual (Dual p) :~: p) -> (Dual (Dual t) :~: t) -> Dual (Limits s p t n m a) -> Limits s p t n m a

from the co limits, with its inverse of coLimits.

lmsFromOpOp :: ConeStruct s a -> (Dual (Dual p) :~: p) -> (Dual (Dual t) :~: t) -> Limits s p t n m (Op (Op a)) -> Limits s p t n m a

from the bidual.

Construction

lmsToPrjOrnt :: Entity p => p -> Limits Mlt Projective t n m (Orientation p)

projective limits for Orientation p.

lmsFromInjOrnt :: Entity p => p -> Limits Mlt Injective t n m (Orientation p)

injective limits for Orientation p.

Proposition

prpLimits :: ConeStruct s a -> Limits s p t n m a -> X (Diagram t n m a) -> XOrtPerspective p a -> Statement

validity according to Limits, relative to the given random variable for Diagrams.

prpLimitsDiagram :: ConeStruct s a -> XOrtPerspective p a -> Limits s p t n m a -> Diagram t n m a -> Statement

validity according to Limits.