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

OAlg.Entity.Diagram.Diagrammatic

Contents

Diagrammatic
Natural
Duality

Description

objects with a naturally underlying Diagram. They serve to generalize the concept of limits according to a diagram (see OAlg.Limes.Limits).

Synopsis

class Diagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) where
- diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x. d t n m x -> Diagram t n m x
newtype DiagramG (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x = DiagramG (d t n m x)
dmap :: forall d (t :: DiagramType) (n :: N') (m :: N') h x y. ApplicativeG (DiagramG d t n m) h (->) => h x y -> d t n m x -> d t n m y
sdbToDgmObj :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. Dual1 (d t n m) ~ d (Dual t) n m => SDualBi (DiagramG d t n m) x -> SDualBi (d t n m) x
sdbFromDgmObj :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. Dual1 (d t n m) ~ d (Dual t) n m => SDualBi (d t n m) x -> SDualBi (DiagramG d t n m) x
class (Diagrammatic d, CategoryDisjunctive h, HomOrientedDisjunctive h, FunctorialOriented h, NaturalTransformable h (->) (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)), t ~ Dual (Dual t)) => NaturalDiagrammatic (h :: Type -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N')
drohS :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. Diagrammatic d => SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG Diagram t n m) x
data NaturalDiagrammaticW (h :: Type -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N')
type NaturalDiagrammaticBi (h :: Type -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') = (NaturalDiagrammatic h d t n m, NaturalDiagrammatic h d (Dual t) n m)
prpNaturalDiagrammatic :: forall (h :: Type -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') q. NaturalDiagrammatic h d t n m => q h d t n m -> X (SomeNaturalApplication h (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m))) -> Statement

Diagrammatic

class Diagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) where Source #

object d having an underlying Diagram.

Methods

diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x. d t n m x -> Diagram t n m x Source #

Instances

Instances details

Diagrammatic Diagram Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic Methods diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x. Diagram t n m x -> Diagram t n m x Source #
Diagrammatic DiagramFree Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x. DiagramFree t n m x -> Diagram t n m x Source #
Diagrammatic SomeFreeSliceDiagram Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x. SomeFreeSliceDiagram t n m x -> Diagram t n m x Source #
Diagrammatic (SliceDiagram i) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction Methods diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x. SliceDiagram i t n m x -> Diagram t n m x Source #

newtype DiagramG (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x Source #

wrapper for Diagrammatic-objects.

Constructors

DiagramG (d t n m x)

Instances

Instances details

Diagrammatic d => Natural s (->) (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic Methods roh :: Struct s x -> SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG Diagram t n m) x Source #
(HomOrientedDisjunctive h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalTransformable h (->) (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic
(CategoryDisjunctive h, HomSlicedOriented i h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalTransformable h (->) (SDualBi (DiagramG (SliceDiagram i) t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction
(HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalTransformable h (->) (SDualBi (DiagramG DiagramFree t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
Diagrammatic d => Natural s (->) (DiagramG d t n m) (DiagramG Diagram t n m) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic Methods roh :: Struct s x -> DiagramG d t n m x -> DiagramG Diagram t n m x Source #
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 #
Oriented x => EqDual1 (DiagramG Diagram t n m :: Type -> Type) (x :: Type) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic
Oriented x => ShowDual1 (DiagramG Diagram t n m :: Type -> Type) (x :: Type) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic
(HomOrientedDisjunctive h, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (DiagramG Diagram t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic Methods amapG :: h x y -> SDualBi (DiagramG Diagram t n m) x -> SDualBi (DiagramG Diagram t n m) y Source #
(HomSlicedOriented i h, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (DiagramG (SliceDiagram i) t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction Methods amapG :: h x y -> SDualBi (DiagramG (SliceDiagram i) t n m) x -> SDualBi (DiagramG (SliceDiagram i) t n m) y Source #
(HomOrientedSlicedFree h, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (DiagramG DiagramFree t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: h x y -> SDualBi (DiagramG DiagramFree t n m) x -> SDualBi (DiagramG DiagramFree t n m) y Source #
(HomOrientedDisjunctive h, FunctorialOriented h, t ~ Dual (Dual t)) => FunctorialG (SDualBi (DiagramG Diagram t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic
(CategoryDisjunctive h, HomSlicedOriented i h, FunctorialOriented h, t ~ Dual (Dual t)) => FunctorialG (SDualBi (DiagramG (SliceDiagram i) t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction
(HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t)) => FunctorialG (SDualBi (DiagramG DiagramFree t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
Show (d t n m x) => Show (DiagramG d t n m x) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic Methods showsPrec :: Int -> DiagramG d t n m x -> ShowS # show :: DiagramG d t n m x -> String # showList :: [DiagramG d t n m x] -> ShowS #
Eq (d t n m x) => Eq (DiagramG d t n m x) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic Methods (==) :: DiagramG d t n m x -> DiagramG d t n m x -> Bool # (/=) :: DiagramG d t n m x -> DiagramG d t n m x -> Bool #
Validable (d t n m x) => Validable (DiagramG d t n m x) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic Methods valid :: DiagramG d t n m x -> Statement Source #
type Dual1 (DiagramG d t n m :: Type -> Type) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic type Dual1 (DiagramG d t n m :: Type -> Type) = DiagramG d (Dual t) n m

dmap :: forall d (t :: DiagramType) (n :: N') (m :: N') h x y. ApplicativeG (DiagramG d t n m) h (->) => h x y -> d t n m x -> d t n m y Source #

the induced mapping between the Diagrammatic objects.

Property Let ApplicativeG ('DiagramG d t n m) h__ (->) and h in h, then holds:

DiagramG . dmap h .=. amapG h . DiagramG.

sdbToDgmObj :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. Dual1 (d t n m) ~ d (Dual t) n m => SDualBi (DiagramG d t n m) x -> SDualBi (d t n m) x Source #

canonical mapping to its underlying diagrammatic object.

sdbFromDgmObj :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. Dual1 (d t n m) ~ d (Dual t) n m => SDualBi (d t n m) x -> SDualBi (DiagramG d t n m) x Source #

canonical mapping from its underlying diagrammatic object.

Natural

class (Diagrammatic d, CategoryDisjunctive h, HomOrientedDisjunctive h, FunctorialOriented h, NaturalTransformable h (->) (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)), t ~ Dual (Dual t)) => NaturalDiagrammatic (h :: Type -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') Source #

natural transformation on Diagrammatic objects from SDualBi (DiagramG d t n m) to SDualBi (Diagram t n m), respecting the canonical application of h on SDualBi (Diagram t n m).

Property Let NaturalDiagrammatic s h d t n m, then for all x, y and h in h x y holds:

amapG h .=. dgMapS h.

Note This property is required if incoherent instances are permitted.

Instances

Instances details

(CategoryDisjunctive h, HomOrientedDisjunctive h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalDiagrammatic h Diagram t n m Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic
(CategoryDisjunctive h, HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalDiagrammatic h DiagramFree t n m Source #
Instance details Defined in OAlg.Entity.Slice.Free
(CategoryDisjunctive h, HomSlicedOriented i h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalDiagrammatic h (SliceDiagram i) t n m Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction

drohS :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. Diagrammatic d => SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG Diagram t n m) x Source #

natural assocition induced by droh betewwn SDualBi (DiagramG d t n m) and SDualBi (Diagram t n m).

data NaturalDiagrammaticW (h :: Type -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') Source #

whiteness of a NaturalDiagrammatic.

Duality

type NaturalDiagrammaticBi (h :: Type -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') = (NaturalDiagrammatic h d t n m, NaturalDiagrammatic h d (Dual t) n m) Source #

natural diagrammatic for t and Dual t.

prpNaturalDiagrammatic :: forall (h :: Type -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') q. NaturalDiagrammatic h d t n m => q h d t n m -> X (SomeNaturalApplication h (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m))) -> Statement Source #

validity according to NaturalDiagrammatic.