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

OAlg.Limes.Cone.Core

Contents

Cone

Description

basic definition of Cones over Diagrammatic objects.

Synopsis

data Cone s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') a where
- ConeProjective :: forall a (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). Multiplicative a => d t n m a -> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
- ConeInjective :: forall a (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). Multiplicative a => d t n m a -> Point a -> FinList n a -> Cone Mlt 'Injective d t n m a
- ConeKernel :: forall a (d :: DiagramType -> N' -> N' -> Type -> Type) (m :: N'). Distributive a => d ('Parallel 'LeftToRight) N2 m a -> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m a
- ConeCokernel :: forall a (d :: DiagramType -> N' -> N' -> Type -> Type) (m :: N'). Distributive a => d ('Parallel 'RightToLeft) N2 m a -> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) m a
diagrammaticObject :: forall s (p :: Perspective) d (t :: DiagramType) (n :: N') (m :: N') a. Cone s p d t n m a -> d t n m a
coneDiagram :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a. Diagrammatic d => Cone s p d t n m a -> Cone s p Diagram t n m a
data Perspective
- = Projective
- | Injective
cnMltOrDst :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') a. Cone s p d t n m a -> Either (s :~: Mlt) (s :~: Dst)
coneStruct :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') a. Cone s p d t n m a -> ConeStruct s a
cnDiagramTypeRefl :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a. Diagrammatic d => Cone s p d t n m a -> Dual (Dual t) :~: t
tip :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') a. Cone s p d t n m a -> Point a
shell :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a. Diagrammatic d => Cone s p d t n m a -> FinList n a
cnArrows :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a. Diagrammatic d => Cone s p d t n m a -> FinList m a
cnPoints :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) a s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N'). (Diagrammatic d, Oriented a) => Cone s p d t n m a -> FinList n (Point a)

Cone

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

cone over a diagram.

Properties Let c be in Cone s p d t n m a for a Diagrammatic d, then holds:

If c matches ConeProjective d t cs for a Multiplicative structure a then holds:
1. For all ci in cs holds: start ci == t and end ci == pi where pi in dgPoints (diagram d).
2. For all aij in dgArrows (diagram d) holds: aij * ci == cj where ci, cj in cs.
If c matches ConeInjective d t cs for a Multiplicative structure a then holds:
1. For all ci in cs holds: end ci == t and start ci == pi where pi in dgPoints (diagram d).
2. For all aij in dgArrows (diagram d) holds: cj * aij == ci where ci, cj in cs.
If c matches ConeKernel p k for a Distributive structure a then holds:
1. end k == p0 where p0 in dgPoints (diagram p)
2. For all a in dgArrows (diagram p) holds: a * k == zero (t :> p1) where t = start k and p0, p1 in dgPoints (diagram p).
If c matches ConeCokernel p k for a Distributive structure a then holds:
1. start k == p0 where p0 in dgPoints (diagram p)
2. For all a in dgArrows (diagram p) holds: k * a == zero (p1 :> t) where t = end k and p0, p1 in dgPoints (diagram p).

Note

Let HomMultiplicativeDisjunctive h and NaturalDiagrammatic h d t n m,then holds: NaturalTransformable h (->) (DiagramG d t n m) (Diagram t n m) (as required by the definition of NaturalDiagrammatic h d t n m) and NaturalTransformable h (->) (Cone Mlt p d t n m) (DiagramG d t n m) (see comment in source code of its instance declaration and the property of dmap) and therefore this establish a natural transformation according to h from Cone Mlt p d t n m to Diagram t n m.
The same holds for HomMultiplicativeDisjunctive h and Cone Dst p d t n m.

Constructors

ConeProjective :: forall a (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). Multiplicative a => d t n m a -> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeInjective :: forall a (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). Multiplicative a => d t n m a -> Point a -> FinList n a -> Cone Mlt 'Injective d t n m a
ConeKernel :: forall a (d :: DiagramType -> N' -> N' -> Type -> Type) (m :: N'). Distributive a => d ('Parallel 'LeftToRight) N2 m a -> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m a
ConeCokernel :: forall a (d :: DiagramType -> N' -> N' -> Type -> Type) (m :: N'). Distributive a => d ('Parallel 'RightToLeft) N2 m a -> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) m a

Instances

Instances details

Conic Cone Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Core Methods cone :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. Cone s p d t n m x -> Cone s p d t n m x Source #
(HomDistributiveDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => NaturalConic h Cone Dst p d t n m Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality
(HomMultiplicativeDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => NaturalConic h Cone Mlt p d t n m Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality
Conic c => Natural r (->) (SDualBi (ConeG c s p d t n m)) (SDualBi (ConeG Cone s p d t n m)) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Core Methods roh :: Struct r x -> SDualBi (ConeG c s p d t n m) x -> SDualBi (ConeG Cone s p d t n m) x Source #
(HomDistributiveDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => NaturalTransformable h (->) (SDualBi (ConeG Cone Dst p d t n m)) (SDualBi (ConeG Cone Dst p d t n m)) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality
(HomMultiplicativeDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => NaturalTransformable h (->) (SDualBi (ConeG Cone Mlt p d t n m)) (SDualBi (ConeG Cone Mlt p d t n m)) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality
(HomDistributiveDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => NaturalTransformable h (->) (SDualBi (ConeG ConeZeroHead Mlt p d t n m)) (SDualBi (ConeG Cone Mlt p d t n m)) Source #
Instance details Defined in OAlg.Limes.Cone.ZeroHead.Duality
Natural r (->) (Cone s p d t n m) (DiagramG d t n m) Source #
Instance details Defined in OAlg.Limes.Cone.Core Methods roh :: Struct r x -> Cone s p d t n m x -> DiagramG d t n m x Source #
Conic c => Natural r (->) (ConeG c s p d t n m) (ConeG Cone s p d t n m) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Core Methods roh :: Struct r x -> ConeG c s p d t n m x -> ConeG Cone s p d t n m x Source #
(Eq x, EqPoint x) => EqDual1 (Cone s p Diagram t n m :: Type -> Type) (x :: Type) Source #
Instance details Defined in OAlg.Limes.Cone.Duality
(Show x, ShowPoint x) => ShowDual1 (Cone s p Diagram t n m :: Type -> Type) (x :: Type) Source #
Instance details Defined in OAlg.Limes.Cone.Duality
(HomDistributiveDisjunctive h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p), t ~ Dual (Dual t)) => ApplicativeG (SDualBi (ConeG Cone Dst p d t n m)) h (->) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality Methods amapG :: h x y -> SDualBi (ConeG Cone Dst p d t n m) x -> SDualBi (ConeG Cone Dst p d t n m) y Source #
(HomMultiplicativeDisjunctive h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p), t ~ Dual (Dual t)) => ApplicativeG (SDualBi (ConeG Cone Mlt p d t n m)) h (->) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality Methods amapG :: h x y -> SDualBi (ConeG Cone Mlt p d t n m) x -> SDualBi (ConeG Cone Mlt p d t n m) y Source #
(HomDistributiveDisjunctive h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => ApplicativeG (SDualBi (Cone Dst p d t n m)) h (->) Source #
Instance details Defined in OAlg.Limes.Cone.Duality Methods amapG :: h x y -> SDualBi (Cone Dst p d t n m) x -> SDualBi (Cone Dst p d t n m) y Source #
(HomMultiplicativeDisjunctive h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => ApplicativeG (SDualBi (Cone Mlt p d t n m)) h (->) Source #
Instance details Defined in OAlg.Limes.Cone.Duality Methods amapG :: h x y -> SDualBi (Cone Mlt p d t n m) x -> SDualBi (Cone Mlt p d t n m) y Source #
(HomDistributiveDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p), t ~ Dual (Dual t)) => FunctorialG (SDualBi (ConeG Cone Dst p d t n m)) h (->) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality
(HomMultiplicativeDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p), t ~ Dual (Dual t)) => FunctorialG (SDualBi (ConeG Cone Mlt p d t n m)) h (->) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality
(HomDistributiveDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => FunctorialG (SDualBi (Cone Dst p d t n m)) h (->) Source #
Instance details Defined in OAlg.Limes.Cone.Duality
(HomMultiplicativeDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => FunctorialG (SDualBi (Cone Mlt p d t n m)) h (->) Source #
Instance details Defined in OAlg.Limes.Cone.Duality
(CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t), s ~ Dst) => NaturalTransformable (Inv2 h) (->) (SDualBi (ConeG (LiftableCone i) s p Diagram t n m)) (SDualBi (ConeG Cone s p Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable
(Distributive x, XStandardEligibleConeKernel N1 x, XStandardEligibleConeFactorKernel N1 x, XStandardEligibleConeCokernel N1 x, XStandardEligibleConeFactorCokernel N1 x) => Validable (VarianceG t Cone Cone Diagram n x) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation Methods valid :: VarianceG t Cone Cone Diagram n x -> Statement Source #
(Distributive x, XStandardEligibleConeKernel N1 x, XStandardEligibleConeFactorKernel N1 x, XStandardEligibleConeCokernel N1 x, XStandardEligibleConeFactorCokernel N1 x, Typeable t, Typeable n) => Validable (VarianceGHom t Cone Cone Diagram n x) Source #
Instance details Defined in OAlg.Limes.Exact.Deviation Methods valid :: VarianceGHom t Cone Cone Diagram n x -> Statement Source #
Show (d t n m a) => Show (Cone s p d t n m a) Source #
Instance details Defined in OAlg.Limes.Cone.Core Methods showsPrec :: Int -> Cone s p d t n m a -> ShowS # show :: Cone s p d t n m a -> String # showList :: [Cone s p d t n m a] -> ShowS #
Eq (d t n m a) => Eq (Cone s p d t n m a) Source #
Instance details Defined in OAlg.Limes.Cone.Core Methods (==) :: Cone s p d t n m a -> Cone s p d t n m a -> Bool # (/=) :: Cone s p d t n m a -> Cone s p d t n m a -> Bool #
(Diagrammatic d, Validable (d t n m a)) => Validable (Cone s p d t n m a) Source #
Instance details Defined in OAlg.Limes.Cone.Definition Methods valid :: Cone s p d t n m a -> Statement Source #
(Entity p, t ~ 'Parallel 'RightToLeft, n ~ N2, Diagrammatic d, XStandard p, XStandard (d t n m (Orientation p))) => XStandard (Cone Dst 'Injective d t n m (Orientation p)) Source #
Instance details Defined in OAlg.Limes.Cone.Definition Methods xStandard :: X (Cone Dst 'Injective d t n m (Orientation p)) Source #
(Entity p, t ~ 'Parallel 'LeftToRight, n ~ N2, Diagrammatic d, XStandard p, XStandard (d t n m (Orientation p))) => XStandard (Cone Dst 'Projective d t n m (Orientation p)) Source #
Instance details Defined in OAlg.Limes.Cone.Definition Methods xStandard :: X (Cone Dst 'Projective d t n m (Orientation p)) Source #
(Entity p, Diagrammatic d, XStandard p, XStandard (d t n m (Orientation p))) => XStandard (Cone Mlt 'Injective d t n m (Orientation p)) Source #
Instance details Defined in OAlg.Limes.Cone.Definition Methods xStandard :: X (Cone Mlt 'Injective d t n m (Orientation p)) Source #
(Entity p, Diagrammatic d, XStandard p, XStandard (d t n m (Orientation p))) => XStandard (Cone Mlt 'Projective d t n m (Orientation p)) Source #
Instance details Defined in OAlg.Limes.Cone.Definition Methods xStandard :: X (Cone Mlt 'Projective d t n m (Orientation p)) Source #
(Oriented a, Diagrammatic d, Entity (d ('Parallel t) N2 m a), Typeable d, Typeable s, Typeable p, Typeable t, Typeable m) => Oriented (Cone s p d ('Parallel t) N2 m a) Source #
Instance details Defined in OAlg.Limes.Cone.Definition Methods orientation :: Cone s p d ('Parallel t) N2 m a -> Orientation (Point (Cone s p d ('Parallel t) N2 m a)) Source # start :: Cone s p d ('Parallel t) N2 m a -> Point (Cone s p d ('Parallel t) N2 m a) Source # end :: Cone s p d ('Parallel t) N2 m a -> Point (Cone s p d ('Parallel t) N2 m a) Source #
EqPoint a => EqPoint (Cone s p d ('Parallel t) N2 m a) Source #
Instance details Defined in OAlg.Limes.Cone.Definition
ShowPoint a => ShowPoint (Cone s p d ('Parallel t) N2 m a) Source #
Instance details Defined in OAlg.Limes.Cone.Definition
TypeablePoint a => TypeablePoint (Cone s p d ('Parallel t) N2 m a) Source #
Instance details Defined in OAlg.Limes.Cone.Definition
ValidablePoint a => ValidablePoint (Cone s p d ('Parallel t) N2 m a) Source #
Instance details Defined in OAlg.Limes.Cone.Definition
type Dual1 (Cone s p d t n m :: Type -> Type) Source #
Instance details Defined in OAlg.Limes.Cone.Duality type Dual1 (Cone s p d t n m :: Type -> Type) = Cone s (Dual p) d (Dual t) n m
type Point (Cone s p d ('Parallel t) N2 m a) Source #
Instance details Defined in OAlg.Limes.Cone.Definition type Point (Cone s p d ('Parallel t) N2 m a) = Point a

diagrammaticObject :: forall s (p :: Perspective) d (t :: DiagramType) (n :: N') (m :: N') a. Cone s p d t n m a -> d t n m a Source #

the underlying Diagrammatic object.

coneDiagram :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a. Diagrammatic d => Cone s p d t n m a -> Cone s p Diagram t n m a Source #

mapping a Diagrammatic-Cone to a Diagram-Cone.

data Perspective Source #

concept of Projective and Injective.

Constructors

Projective
Injective

Instances

Instances details

Bounded Perspective Source #
Instance details Defined in OAlg.Limes.Perspective Methods minBound :: Perspective # maxBound :: Perspective #
Enum Perspective Source #
Instance details Defined in OAlg.Limes.Perspective Methods succ :: Perspective -> Perspective # pred :: Perspective -> Perspective # toEnum :: Int -> Perspective # fromEnum :: Perspective -> Int # enumFrom :: Perspective -> [Perspective] # enumFromThen :: Perspective -> Perspective -> [Perspective] # enumFromTo :: Perspective -> Perspective -> [Perspective] # enumFromThenTo :: Perspective -> Perspective -> Perspective -> [Perspective] #
Show Perspective Source #
Instance details Defined in OAlg.Limes.Perspective Methods showsPrec :: Int -> Perspective -> ShowS # show :: Perspective -> String # showList :: [Perspective] -> ShowS #
Eq Perspective Source #
Instance details Defined in OAlg.Limes.Perspective Methods (==) :: Perspective -> Perspective -> Bool # (/=) :: Perspective -> Perspective -> Bool #
Ord Perspective Source #
Instance details Defined in OAlg.Limes.Perspective Methods compare :: Perspective -> Perspective -> Ordering # (<) :: Perspective -> Perspective -> Bool # (<=) :: Perspective -> Perspective -> Bool # (>) :: Perspective -> Perspective -> Bool # (>=) :: Perspective -> Perspective -> Bool # max :: Perspective -> Perspective -> Perspective # min :: Perspective -> Perspective -> Perspective #
type Dual 'Injective Source #
Instance details Defined in OAlg.Limes.Perspective type Dual 'Injective = 'Projective
type Dual 'Projective Source #
Instance details Defined in OAlg.Limes.Perspective type Dual 'Projective = 'Injective
type ToSite 'Injective Source #
Instance details Defined in OAlg.Limes.Perspective type ToSite 'Injective = 'From
type ToSite 'Projective Source #
Instance details Defined in OAlg.Limes.Perspective type ToSite 'Projective = 'To

cnMltOrDst :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') a. Cone s p d t n m a -> Either (s :~: Mlt) (s :~: Dst) Source #

proof of s being either Mlt or Dst.

coneStruct :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') a. Cone s p d t n m a -> ConeStruct s a Source #

the associated ConeStruct.

cnDiagramTypeRefl :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a. Diagrammatic d => Cone s p d t n m a -> Dual (Dual t) :~: t Source #

reflexivity of the underlying diagram type.

tip :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') a. Cone s p d t n m a -> Point a Source #

the tip of a cone.

Property Let c be in Cone s p t n m a for a Oriented structure then holds:

If p is equal to Projective then holds: start ci == tip c for all ci in shell c.
If p is equal to Injective then holds: end ci == tip c for all ci in shell c.

shell :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a. Diagrammatic d => Cone s p d t n m a -> FinList n a Source #

the shell of a cone.

Property Let c be in Cone s p t n m a for a Oriented structure then holds:

If p is equal to Projective then holds: amap end (shell c) == cnPoints c.
If p is equal to Injective then holds: amap start (shell c) == cnPoints c.

cnArrows :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a. Diagrammatic d => Cone s p d t n m a -> FinList m a Source #

the arrows of the underlying diagram.

cnPoints :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) a s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N'). (Diagrammatic d, Oriented a) => Cone s p d t n m a -> FinList n (Point a) Source #

the points of the underlying diagram.