| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
OAlg.Limes.TerminalAndInitialPoint
Description
terminal and initial point within a Multiplicative structure, i.e. limits of
Diagram Empty
Synopsis
- type Terminals = TerminalsG Cone Diagram
- type TerminalsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = LimitsG c Mlt 'Projective d 'Empty N0 N0
- type TerminalPoint = TerminalPointG Cone Diagram
- type TerminalPointG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = LimesG c Mlt 'Projective d 'Empty N0 N0
- type TerminalCone = TerminalConic Cone Diagram
- type TerminalConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = c Mlt 'Projective d 'Empty N0 N0
- type TerminalDiagram = TerminalDiagrammatic Diagram
- type TerminalDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) = d 'Empty N0 N0
- trmDiagram :: TerminalDiagram x
- trmCone :: Multiplicative x => Point x -> TerminalCone x
- trmConeG :: Multiplicative x => d 'Empty N0 N0 x -> Point x -> TerminalConic Cone d x
- terminalPointOrnt :: Entity p => p -> TerminalPoint (Orientation p)
- trmsOrnt :: Entity p => p -> Terminals (Orientation p)
- type Initials = InitialsG Cone Diagram
- type InitialsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = LimitsG c Mlt 'Injective d 'Empty N0 N0
- type InitialPoint = InitialPointG Cone Diagram
- type InitialPointG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = LimesG c Mlt 'Injective d 'Empty N0 N0
- type InitialCone = InitialConic Cone Diagram
- type InitialConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = c Mlt 'Injective d 'Empty N0 N0
- type InitialDiagram = InitialDiagrammatic Diagram
- type InitialDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) = d 'Empty N0 N0
- intDiagram :: InitialDiagram x
- intCone :: Multiplicative x => Point x -> InitialCone x
- initialPointOrnt :: Entity p => p -> InitialPoint (Orientation p)
- intsOrnt :: Entity p => p -> Initials (Orientation p)
- type DualsiableGEmpty (p :: Perspective) (o :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = NaturalConicBi (IsoO Mlt o) c Mlt p d 'Empty N0 N0
- coTerminals :: (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => Terminals x -> Initials (o x)
- coTerminalPoint :: (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => TerminalPoint x -> InitialPoint (o x)
- coTerminalsG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type). (Multiplicative x, TransformableGRefl o Mlt, DualsiableGEmpty 'Projective o c d) => TerminalsG c d x -> InitialsG c d (o x)
- coTerminalPointG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type). (Multiplicative x, TransformableGRefl o Mlt, DualsiableGEmpty 'Projective o c d) => TerminalPointG c d x -> InitialPointG c d (o x)
- coInitials :: (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => Initials x -> Terminals (o x)
- coInitialPoint :: (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => InitialPoint x -> TerminalPoint (o x)
- coInitialsG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type). (Multiplicative x, TransformableGRefl o Mlt, DualsiableGEmpty 'Injective o c d) => InitialsG c d x -> TerminalsG c d (o x)
- coInitialPointG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type). (Multiplicative x, TransformableGRefl o Mlt, DualsiableGEmpty 'Injective o c d) => InitialPointG c d x -> TerminalPointG c d (o x)
- prpTerminalAndInitialPoint :: Statement
Terminal
type Terminals = TerminalsG Cone Diagram Source #
terminal points within a Multiplicative structure.
type TerminalsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = LimitsG c Mlt 'Projective d 'Empty N0 N0 Source #
generic terminal points within a Multiplicative structure.
type TerminalPoint = TerminalPointG Cone Diagram Source #
terminal point as Limes.
type TerminalPointG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = LimesG c Mlt 'Projective d 'Empty N0 N0 Source #
generic terminal point as LimesG.
type TerminalCone = TerminalConic Cone Diagram Source #
Cone for a terminal point.
type TerminalConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = c Mlt 'Projective d 'Empty N0 N0 Source #
Conic object for a terminal point.
type TerminalDiagram = TerminalDiagrammatic Diagram Source #
Diagram for a terminal point.
type TerminalDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) = d 'Empty N0 N0 Source #
Diagrammatic object for a terminal point.
trmDiagram :: TerminalDiagram x Source #
the terminal diagram.
trmCone :: Multiplicative x => Point x -> TerminalCone x Source #
the terminal cone of a given point.
trmConeG :: Multiplicative x => d 'Empty N0 N0 x -> Point x -> TerminalConic Cone d x Source #
the terminal cone of a given point according to the given diagrammatic object.
Orientation
terminalPointOrnt :: Entity p => p -> TerminalPoint (Orientation p) Source #
the terminal limes of a given point p.
trmsOrnt :: Entity p => p -> Terminals (Orientation p) Source #
terminals for Orientation.
Initial
type InitialsG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = LimitsG c Mlt 'Injective d 'Empty N0 N0 Source #
generic initial points within a Multiplicative structure.
type InitialPoint = InitialPointG Cone Diagram Source #
initial point as Limes.
type InitialPointG (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = LimesG c Mlt 'Injective d 'Empty N0 N0 Source #
initial point as LimesG.
type InitialCone = InitialConic Cone Diagram Source #
Cone for a initial point.
type InitialConic (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = c Mlt 'Injective d 'Empty N0 N0 Source #
Conic object for a initial point.
type InitialDiagram = InitialDiagrammatic Diagram Source #
Diagram for a initial point.
type InitialDiagrammatic (d :: DiagramType -> N' -> N' -> Type -> Type) = d 'Empty N0 N0 Source #
Diagrammatic object for a initial point.
intDiagram :: InitialDiagram x Source #
the initial diagram.
intCone :: Multiplicative x => Point x -> InitialCone x Source #
the initial cone of a given point.
Orientation
initialPointOrnt :: Entity p => p -> InitialPoint (Orientation p) Source #
initial point for Orientation.
Duality
type DualsiableGEmpty (p :: Perspective) (o :: Type -> Type) (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type) = NaturalConicBi (IsoO Mlt o) c Mlt p d 'Empty N0 N0 Source #
type for dualisable generic limits of Conic objects over Empty Diagrammatic objects.
type DualsiableGEmpty p o c d = NaturalConicBi (Inv2 (HomDisjEmpty Mlt o)) c Mlt p d 'Empty N0 N0
Terminal
coTerminals :: (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => Terminals x -> Initials (o x) Source #
co-terminals over x, i.e. initials over o x.
coTerminalPoint :: (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => TerminalPoint x -> InitialPoint (o x) Source #
co-terminal point over x, i.e. initial point over o x.
coTerminalsG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type). (Multiplicative x, TransformableGRefl o Mlt, DualsiableGEmpty 'Projective o c d) => TerminalsG c d x -> InitialsG c d (o x) Source #
co-terminals over x, i.e. initials over o x.
coTerminalPointG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type). (Multiplicative x, TransformableGRefl o Mlt, DualsiableGEmpty 'Projective o c d) => TerminalPointG c d x -> InitialPointG c d (o x) Source #
co-terminal point over x, i.e. initial point over o x.
Initial
coInitials :: (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => Initials x -> Terminals (o x) Source #
co-initials over x, i.e. terminals over o x.
coInitialPoint :: (Multiplicative x, TransformableGRefl o Mlt, DualisableMultiplicative Mlt o) => InitialPoint x -> TerminalPoint (o x) Source #
co-initial point over x, i.e. terminal point over o x.
coInitialsG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type). (Multiplicative x, TransformableGRefl o Mlt, DualsiableGEmpty 'Injective o c d) => InitialsG c d x -> TerminalsG c d (o x) Source #
co-initials over x, i.e. terminals over o x.
coInitialPointG :: forall x o (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) (d :: DiagramType -> N' -> N' -> Type -> Type). (Multiplicative x, TransformableGRefl o Mlt, DualsiableGEmpty 'Injective o c d) => InitialPointG c d x -> TerminalPointG c d (o x) Source #
co-initial point over x, i.e. terminal point over o x.
Proposition
prpTerminalAndInitialPoint :: Statement Source #
validity of terminals and initials over Orientation Symbol