OAlg.Limes.Limits

Contents

Description

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

Synopsis

newtype Limits s p t n m a = Limits (Diagram t n m a -> Limes s p t n m a)
limes :: Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
lmsMap :: IsoOrt s h => h a b -> Limits s p t n m a -> Limits s p t n m b
lmsToOp :: LimitsDuality s f g a -> f a -> g (Op a)
lmsFromOp :: LimitsDuality s f g a -> g (Op a) -> f a
data LimitsDuality s f g a where
- 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)
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
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
lmsToPrjOrnt :: Entity p => p -> Limits Mlt Projective t n m (Orientation p)
lmsFromInjOrnt :: Entity p => p -> Limits Mlt Injective t n m (Orientation p)
prpLimits :: ConeStruct s a -> Limits s p t n m a -> X (Diagram t n m a) -> XOrtPerspective p a -> Statement
prpLimitsDiagram :: ConeStruct s a -> XOrtPerspective p a -> Limits s p t n m a -> Diagram t n m a -> Statement

Limits

newtype Limits s p t n m a Source #

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 details

IsoDistributive h => Applicative1 h (Limits Dst p t n m) Source #
Instance details Defined in OAlg.Limes.Limits Methods amap1 :: h a b -> Limits Dst p t n m a -> Limits Dst p t n m b Source #
IsoMultiplicative h => Applicative1 h (Limits Mlt p t n m) Source #
Instance details Defined in OAlg.Limes.Limits Methods amap1 :: h a b -> Limits Mlt p t n m a -> Limits Mlt p t n m b Source #
(Distributive a, XStandard (Diagram t n m a), XStandardOrtPerspective p a) => Validable (Limits Dst p t n m a) Source #
Instance details Defined in OAlg.Limes.Limits Methods valid :: Limits Dst p t n m a -> Statement Source #
(Multiplicative a, XStandard (Diagram t n m a), XStandardOrtPerspective p a) => Validable (Limits Mlt p t n m a) Source #
Instance details Defined in OAlg.Limes.Limits Methods valid :: Limits Mlt p t n m a -> Statement Source #
type Dual (Limits s p t n m a :: TYPE LiftedRep) Source #
Instance details 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 Source #

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 Source #

mapping of limits.

Duality

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

to g (Op a).

from g (Op a).

data LimitsDuality s f g a where Source #

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) Source #

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 Source #

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 Source #

from the bidual.

projective limits for Orientation p.

injective limits for Orientation p.

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

validity according to Limits.