limes of a diagram, i.e. a distinguished cone over a given diagram having the following universal property

Property Let a be a Multiplicative structure and u in Limes s p t n m a then holds: Let l = universalCone u in

1. l is valid.
2. eligibleCone u l.
3. eligibleFactor u l (one (tip l)).

4. For all c in Cone s p t n m a with eligibleCone u c holds: Let f = universalFactor u c in

   1. f is valid.
   2. eligibleFactor u c f.
   3. For all x in a with eligibleFactor u c x holds: x == f.

Note

1. 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.
2. 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.

the universal point of a limes, i.e. the tip of the universal cone.

the underlying universal cone of a limes.

the shell of the universal cone.

the universal factor of a Limes l to a given eligible cone.

Property Let l be in Limes s p t n m a then holds: For all c in Cone s p t n m a with eligibleCone l c holds: eligibleFactor l c (universalFactor l c).

the underlying diagram of a limes.

reflexivity of the underlying diagram type.

eligibility of a cone with respect to a limes.

Property Let u be in Limes s p t n m a and c in Cone s p t n m a then holds: eligibleCone u c is true if and only if diagram u == cnDiagram c is true.

eligibility of a factor with respect to a limes and a cone.

Property Let u be in Limes s p t n m a, c in Cone s p t n m a with eligibleCone u c and x in a then holds:

1. If u matches LimesProjective l _ then holds: eligibleFactor u c x is true if and only if cnEligibleFactor x c l is true.
2. If u matches LimesInjective l _ then holds: eligibleFactor u c x is true if and only if cnEligibleFactor x l c is true.

mapping between limits.

to g (Op a).

from g (Op a).

Op-duality between limes types.

the co limes with its inverse coLimesInv.

the inverse of coLimes.

from Op . Op.

projective limes on oriented structures.

injective limes on oriented structures.

validity of a Limes.

limes exceptions which are sub exceptions from SomeOAlgException.