{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DataKinds, ConstraintKinds #-}

-- |

-- Module      : OAlg.Limes.TerminalAndInitialPoint

-- Description : terminal and initial point

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- terminal and initial point within a 'Multiplicative' structure, i.e. limits of

-- @'Diagram' 'Empty'@.

module OAlg.Limes.TerminalAndInitialPoint
  (
    -- * Terminal

    Terminals, TerminalsG
  , TerminalPoint, TerminalPointG
  , TerminalCone, TerminalConic
  , TerminalDiagram, TerminalDiagrammatic
  , trmDiagram, trmCone, trmConeG

    -- ** Orientation

  , terminalPointOrnt, trmsOrnt
    

    -- * Initial

  , Initials, InitialsG
  , InitialPoint, InitialPointG
  , InitialCone, InitialConic
  , InitialDiagram, InitialDiagrammatic
  , intDiagram, intCone

    -- ** Orientation

  , initialPointOrnt, intsOrnt

    -- * Duality

  , DualsiableGEmpty    
    -- ** Terminal

  , coTerminals, coTerminalPoint
  , coTerminalsG, coTerminalPointG

    -- ** Initial

  , coInitials, coInitialPoint
  , coInitialsG, coInitialPointG

    -- * Proposition

  , prpTerminalAndInitialPoint
  ) where

import Data.Kind

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Either
import OAlg.Data.Variant
import OAlg.Data.Symbol

import OAlg.Entity.Natural hiding ((++))
import OAlg.Entity.FinList
import OAlg.Entity.Diagram as D

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative

import OAlg.Hom.Definition

import OAlg.Limes.Cone
import OAlg.Limes.Definition
import OAlg.Limes.Limits


import OAlg.Hom.Multiplicative

--------------------------------------------------------------------------------

-- Terminal -


-- | 'Diagrammatic' object for a terminal point.

type TerminalDiagrammatic d = d 'Empty N0 N0 :: Type -> Type

-- | 'Diagram' for a terminal point.

type TerminalDiagram = TerminalDiagrammatic Diagram

-- | 'Conic' object for a terminal point.

type TerminalConic c (d :: DiagramType -> N' -> N' -> Type -> Type)
  = c Mlt Projective d 'Empty N0 N0 :: Type -> Type 

-- | 'Cone' for a terminal point.

type TerminalCone = TerminalConic Cone Diagram

-- | generic terminal point as 'LimesG'.

type TerminalPointG c d = LimesG c Mlt Projective d 'Empty N0 N0 

-- | terminal point as 'Limes'.

type TerminalPoint = TerminalPointG Cone Diagram

-- | generic terminal points within a 'Multiplicative' structure.

type TerminalsG c d = LimitsG c Mlt Projective d 'Empty N0 N0

-- | terminal points within a 'Multiplicative' structure.

type Terminals = TerminalsG Cone Diagram

--------------------------------------------------------------------------------

-- trmDiagram -


-- | the terminal diagram.

trmDiagram :: TerminalDiagram x
trmDiagram :: forall x. TerminalDiagram x
trmDiagram = Diagram 'Empty N0 N0 x
forall x. TerminalDiagram x
DiagramEmpty

--------------------------------------------------------------------------------

-- trmConeG -


-- | the terminal cone of a given point according to the given diagrammatic object.

trmConeG :: Multiplicative x
  => d Empty N0 N0 x -> Point x -> TerminalConic Cone d x
trmConeG :: forall x (d :: DiagramType -> N' -> N' -> * -> *).
Multiplicative x =>
d 'Empty N0 N0 x -> Point x -> TerminalConic Cone d x
trmConeG d 'Empty N0 N0 x
d Point x
t = d 'Empty N0 N0 x
-> Point x -> FinList N0 x -> Cone Mlt 'Projective d 'Empty N0 N0 x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (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
ConeProjective d 'Empty N0 N0 x
d Point x
t FinList N0 x
forall a. FinList N0 a
Nil

--------------------------------------------------------------------------------

-- trmCone -


-- | the terminal cone of a given point.

trmCone :: Multiplicative x => Point x -> TerminalCone x
trmCone :: forall x. Multiplicative x => Point x -> TerminalCone x
trmCone = Diagram 'Empty N0 N0 x
-> Point x -> Cone Mlt 'Projective Diagram 'Empty N0 N0 x
forall x (d :: DiagramType -> N' -> N' -> * -> *).
Multiplicative x =>
d 'Empty N0 N0 x -> Point x -> TerminalConic Cone d x
trmConeG Diagram 'Empty N0 N0 x
forall x. TerminalDiagram x
DiagramEmpty

--------------------------------------------------------------------------------

-- trmPoinitialPointOrnt -


-- | the terminal limes of a given point @p@.

terminalPointOrnt :: Entity p => p -> TerminalPoint (Orientation p)
terminalPointOrnt :: forall p. Entity p => p -> TerminalPoint (Orientation p)
terminalPointOrnt p
p = p
-> Diagram 'Empty N0 N0 (Orientation p)
-> Limes Mlt 'Projective 'Empty N0 N0 (Orientation p)
forall p x (t :: DiagramType) (n :: N') (m :: N').
(Entity p, x ~ Orientation p) =>
p -> Diagram t n m x -> Limes Mlt 'Projective t n m x
lmMltPrjOrnt p
p Diagram 'Empty N0 N0 (Orientation p)
forall x. TerminalDiagram x
trmDiagram

--------------------------------------------------------------------------------

-- trmsOrnt -


-- | terminals for 'Orientation'.

trmsOrnt :: Entity p => p -> Terminals (Orientation p)
trmsOrnt :: forall p. Entity p => p -> Terminals (Orientation p)
trmsOrnt = p -> Limits Mlt 'Projective 'Empty N0 N0 (Orientation p)
forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsMltPrjOrnt 

--------------------------------------------------------------------------------

-- Initial -


-- | 'Diagrammatic' object for a initial point.

type InitialDiagrammatic d = d 'Empty N0 N0 :: Type -> Type

-- | 'Diagram' for a initial point.

type InitialDiagram = InitialDiagrammatic Diagram

-- | 'Conic' object for a initial point.

type InitialConic c (d :: DiagramType -> N' -> N' -> Type -> Type)
  = c Mlt Injective d 'Empty N0 N0 :: Type -> Type

-- | 'Cone' for a initial point.

type InitialCone = InitialConic Cone Diagram

-- | initial point as 'LimesG'.

type InitialPointG c d = LimesG c Mlt Injective d 'Empty N0 N0

-- | initial point as 'Limes'.

type InitialPoint = InitialPointG Cone Diagram

-- | generic initial points within a 'Multiplicative' structure.

type InitialsG c d = LimitsG c Mlt Injective d 'Empty N0 N0

-- | initial points within a 'Multiplicative' structure.

type Initials = InitialsG Cone Diagram 

--------------------------------------------------------------------------------

-- intDiagram -


-- | the initial diagram.

intDiagram :: InitialDiagram x
intDiagram :: forall x. TerminalDiagram x
intDiagram = Diagram 'Empty N0 N0 x
forall x. TerminalDiagram x
DiagramEmpty

--------------------------------------------------------------------------------

-- intCone -


-- | the initial cone of a given point.

intCone :: Multiplicative x => Point x -> InitialCone x
intCone :: forall x. Multiplicative x => Point x -> InitialCone x
intCone Point x
i = Diagram 'Empty N0 N0 x
-> Point x
-> FinList N0 x
-> Cone Mlt 'Injective Diagram 'Empty N0 N0 x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (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
ConeInjective Diagram 'Empty N0 N0 x
forall x. TerminalDiagram x
DiagramEmpty Point x
i FinList N0 x
forall a. FinList N0 a
Nil

--------------------------------------------------------------------------------

-- initialPointOrnt -


-- | initial point for 'Orientation'.

initialPointOrnt :: Entity p => p -> InitialPoint (Orientation p)
initialPointOrnt :: forall p. Entity p => p -> InitialPoint (Orientation p)
initialPointOrnt p
i = p
-> Diagram 'Empty N0 N0 (Orientation p)
-> Limes Mlt 'Injective 'Empty N0 N0 (Orientation p)
forall p x (t :: DiagramType) (n :: N') (m :: N').
(Entity p, x ~ Orientation p) =>
p -> Diagram t n m x -> Limes Mlt 'Injective t n m x
lmMltInjOrnt p
i Diagram 'Empty N0 N0 (Orientation p)
forall x. TerminalDiagram x
intDiagram

--------------------------------------------------------------------------------

-- intsOrnt -


-- | initials.

intsOrnt :: Entity p => p -> Initials (Orientation p)
intsOrnt :: forall p. Entity p => p -> Initials (Orientation p)
intsOrnt = p -> Limits Mlt 'Injective 'Empty N0 N0 (Orientation p)
forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsMltInjOrnt

--------------------------------------------------------------------------------

-- DualsiableGEmpty -


-- | type for dualisable generic limits of 'Conic' objects over t'Empty' 'Diagrammatic' objects.

-- type DualsiableGEmpty p o c d = NaturalConicBi (Inv2 (HomDisjEmpty Mlt o)) c Mlt p d 'Empty N0 N0

type DualsiableGEmpty p o c d = NaturalConicBi (IsoO Mlt o) c Mlt p d 'Empty N0 N0

--------------------------------------------------------------------------------

-- coTerminalPointG -


-- | co-terminal point over @__x__@, i.e. initial point over @__o x__@. 

coTerminalPointG ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualsiableGEmpty Projective o c d
  )
  => TerminalPointG c d x -> InitialPointG c d (o x)
coTerminalPointG :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualsiableGEmpty 'Projective o c d) =>
TerminalPointG c d x -> InitialPointG c d (o x)
coTerminalPointG TerminalPointG c d x
trm = Dual1 (LimesG c Mlt 'Projective d 'Empty N0 N0) (o x)
LimesG c Mlt 'Injective d 'Empty N0 N0 (o x)
int where
  Contravariant2 IsoO Mlt o x (o x)
i = Struct Mlt x
-> Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt o)) x (o x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO (Struct Mlt x
forall {x}. Multiplicative x => Struct Mlt x
forall s x. Structure s x => Struct s x
Struct :: Multiplicative x => Struct Mlt x)
  SDualBi (Left1 Dual1 (LimesG c Mlt 'Projective d 'Empty N0 N0) (o x)
int) = IsoO Mlt o x (o x)
-> SDualBi (LimesG c Mlt 'Projective d 'Empty N0 N0) x
-> SDualBi (LimesG c Mlt 'Projective d 'Empty N0 N0) (o x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Mlt o x (o x)
i (Either1
  (Dual1 (LimesG c Mlt 'Projective d 'Empty N0 N0))
  (LimesG c Mlt 'Projective d 'Empty N0 N0)
  x
-> SDualBi (LimesG c Mlt 'Projective d 'Empty N0 N0) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (TerminalPointG c d x
-> Either1
     (LimesG c Mlt 'Injective d 'Empty N0 N0)
     (LimesG c Mlt 'Projective d 'Empty N0 N0)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 TerminalPointG c d x
trm))

--------------------------------------------------------------------------------

-- coTerminalPoint -


-- | co-terminal point over @__x__@, i.e. initial point over @__o x__@. 

coTerminalPoint ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableMultiplicative Mlt o
  )
  => TerminalPoint x -> InitialPoint (o x)
coTerminalPoint :: forall x (o :: * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableMultiplicative Mlt o) =>
TerminalPoint x -> InitialPoint (o x)
coTerminalPoint = TerminalPointG Cone Diagram x -> InitialPointG Cone Diagram (o x)
forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualsiableGEmpty 'Projective o c d) =>
TerminalPointG c d x -> InitialPointG c d (o x)
coTerminalPointG

--------------------------------------------------------------------------------

-- coTerminalsG -


-- | co-terminals over @__x__@, i.e. initials over @__o x__@. 

coTerminalsG ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualsiableGEmpty Projective o c d
  )
  => TerminalsG c d x -> InitialsG c d (o x)
coTerminalsG :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualsiableGEmpty 'Projective o c d) =>
TerminalsG c d x -> InitialsG c d (o x)
coTerminalsG TerminalsG c d x
trms = Dual1 (LimitsG c Mlt 'Projective d 'Empty N0 N0) (o x)
LimitsG c Mlt 'Injective d 'Empty N0 N0 (o x)
ints where
  Contravariant2 IsoO Mlt o x (o x)
i = Struct Mlt x
-> Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt o)) x (o x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO (Struct Mlt x
forall {x}. Multiplicative x => Struct Mlt x
forall s x. Structure s x => Struct s x
Struct :: Multiplicative x => Struct Mlt x)
  SDualBi (Left1 Dual1 (LimitsG c Mlt 'Projective d 'Empty N0 N0) (o x)
ints) = IsoO Mlt o x (o x)
-> SDualBi (LimitsG c Mlt 'Projective d 'Empty N0 N0) x
-> SDualBi (LimitsG c Mlt 'Projective d 'Empty N0 N0) (o x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Mlt o x (o x)
i (Either1
  (Dual1 (LimitsG c Mlt 'Projective d 'Empty N0 N0))
  (LimitsG c Mlt 'Projective d 'Empty N0 N0)
  x
-> SDualBi (LimitsG c Mlt 'Projective d 'Empty N0 N0) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (TerminalsG c d x
-> Either1
     (LimitsG c Mlt 'Injective d 'Empty N0 N0)
     (LimitsG c Mlt 'Projective d 'Empty N0 N0)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 TerminalsG c d x
trms))

--------------------------------------------------------------------------------

-- coTerminals -


-- | co-terminals over @__x__@, i.e. initials over @__o x__@. 

coTerminals ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableMultiplicative Mlt o
  )
  => Terminals x -> Initials (o x)
coTerminals :: forall x (o :: * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableMultiplicative Mlt o) =>
Terminals x -> Initials (o x)
coTerminals = TerminalsG Cone Diagram x -> InitialsG Cone Diagram (o x)
forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualsiableGEmpty 'Projective o c d) =>
TerminalsG c d x -> InitialsG c d (o x)
coTerminalsG

--------------------------------------------------------------------------------

-- coInitialPoint -


-- | co-initial point over @__x__@, i.e. terminal point over @__o x__@. 

coInitialPointG ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualsiableGEmpty Injective o c d
  )
  => InitialPointG c d x -> TerminalPointG c d (o x)
coInitialPointG :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualsiableGEmpty 'Injective o c d) =>
InitialPointG c d x -> TerminalPointG c d (o x)
coInitialPointG InitialPointG c d x
int = Dual1 (LimesG c Mlt 'Injective d 'Empty N0 N0) (o x)
LimesG c Mlt 'Projective d 'Empty N0 N0 (o x)
trm where
  Contravariant2 IsoO Mlt o x (o x)
i = Struct Mlt x
-> Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt o)) x (o x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO (Struct Mlt x
forall {x}. Multiplicative x => Struct Mlt x
forall s x. Structure s x => Struct s x
Struct :: Multiplicative x => Struct Mlt x)
  SDualBi (Left1 Dual1 (LimesG c Mlt 'Injective d 'Empty N0 N0) (o x)
trm) = IsoO Mlt o x (o x)
-> SDualBi (LimesG c Mlt 'Injective d 'Empty N0 N0) x
-> SDualBi (LimesG c Mlt 'Injective d 'Empty N0 N0) (o x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Mlt o x (o x)
i (Either1
  (Dual1 (LimesG c Mlt 'Injective d 'Empty N0 N0))
  (LimesG c Mlt 'Injective d 'Empty N0 N0)
  x
-> SDualBi (LimesG c Mlt 'Injective d 'Empty N0 N0) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (InitialPointG c d x
-> Either1
     (LimesG c Mlt 'Projective d 'Empty N0 N0)
     (LimesG c Mlt 'Injective d 'Empty N0 N0)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 InitialPointG c d x
int))

--------------------------------------------------------------------------------

-- coInitialPoint -


-- | co-initial point over @__x__@, i.e. terminal point over @__o x__@. 

coInitialPoint ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableMultiplicative Mlt o
  )
  => InitialPoint x -> TerminalPoint (o x)
coInitialPoint :: forall x (o :: * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableMultiplicative Mlt o) =>
InitialPoint x -> TerminalPoint (o x)
coInitialPoint = InitialPointG Cone Diagram x -> TerminalPointG Cone Diagram (o x)
forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualsiableGEmpty 'Injective o c d) =>
InitialPointG c d x -> TerminalPointG c d (o x)
coInitialPointG

--------------------------------------------------------------------------------

-- coInitials -


-- | co-initials over @__x__@, i.e. terminals over @__o x__@. 

coInitialsG ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualsiableGEmpty Injective o c d
  )
  => InitialsG c d x -> TerminalsG c d (o x)
coInitialsG :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualsiableGEmpty 'Injective o c d) =>
InitialsG c d x -> TerminalsG c d (o x)
coInitialsG InitialsG c d x
ints = Dual1 (LimitsG c Mlt 'Injective d 'Empty N0 N0) (o x)
LimitsG c Mlt 'Projective d 'Empty N0 N0 (o x)
trms where
  Contravariant2 IsoO Mlt o x (o x)
i = Struct Mlt x
-> Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt o)) x (o x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO (Struct Mlt x
forall {x}. Multiplicative x => Struct Mlt x
forall s x. Structure s x => Struct s x
Struct :: Multiplicative x => Struct Mlt x)
  SDualBi (Left1 Dual1 (LimitsG c Mlt 'Injective d 'Empty N0 N0) (o x)
trms) = IsoO Mlt o x (o x)
-> SDualBi (LimitsG c Mlt 'Injective d 'Empty N0 N0) x
-> SDualBi (LimitsG c Mlt 'Injective d 'Empty N0 N0) (o x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Mlt o x (o x)
i (Either1
  (Dual1 (LimitsG c Mlt 'Injective d 'Empty N0 N0))
  (LimitsG c Mlt 'Injective d 'Empty N0 N0)
  x
-> SDualBi (LimitsG c Mlt 'Injective d 'Empty N0 N0) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (InitialsG c d x
-> Either1
     (LimitsG c Mlt 'Projective d 'Empty N0 N0)
     (LimitsG c Mlt 'Injective d 'Empty N0 N0)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 InitialsG c d x
ints))

--------------------------------------------------------------------------------

-- coInitials -


-- | co-initials over @__x__@, i.e. terminals over @__o x__@. 

coInitials ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableMultiplicative Mlt o
  )
  => Initials x -> Terminals (o x)
coInitials :: forall x (o :: * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableMultiplicative Mlt o) =>
Initials x -> Terminals (o x)
coInitials = InitialsG Cone Diagram x -> TerminalsG Cone Diagram (o x)
forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualsiableGEmpty 'Injective o c d) =>
InitialsG c d x -> TerminalsG c d (o x)
coInitialsG

--------------------------------------------------------------------------------

-- prpTerminalAndInitialPoint -


-- | validity of terminals and initials over @'Orientation' 'Symbol'@.

prpTerminalAndInitialPoint :: Statement
prpTerminalAndInitialPoint :: Statement
prpTerminalAndInitialPoint = String -> Label
Prp String
"TerminalAndInitialPoint" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XEligibleConeG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
-> XEligibleConeFactorG
     Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
-> X (Diagram 'Empty N0 N0 (Orientation Symbol))
-> LimitsG
     Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
-> Statement
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> X (d t n m x)
-> LimitsG c s p d t n m x
-> Statement
prpLimitsG XEligibleConeG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
xecT XEligibleConeFactorG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
xecfT X (Diagram 'Empty N0 N0 (Orientation Symbol))
forall x. XStandard x => X x
xStandard LimitsG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
tps    -- terminals

      , XEligibleConeG
  Cone Mlt 'Injective Diagram 'Empty N0 N0 (Op (Orientation Symbol))
-> XEligibleConeFactorG
     Cone Mlt 'Injective Diagram 'Empty N0 N0 (Op (Orientation Symbol))
-> X (Diagram 'Empty N0 N0 (Op (Orientation Symbol)))
-> LimitsG
     Cone Mlt 'Injective Diagram 'Empty N0 N0 (Op (Orientation Symbol))
-> Statement
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> X (d t n m x)
-> LimitsG c s p d t n m x
-> Statement
prpLimitsG XEligibleConeG
  Cone
  Mlt
  (Dual 'Projective)
  Diagram
  (Dual 'Empty)
  N0
  N0
  (Op (Orientation Symbol))
XEligibleConeG
  Cone Mlt 'Injective Diagram 'Empty N0 N0 (Op (Orientation Symbol))
xecT' XEligibleConeFactorG
  Cone
  Mlt
  (Dual 'Projective)
  Diagram
  (Dual 'Empty)
  N0
  N0
  (Op (Orientation Symbol))
XEligibleConeFactorG
  Cone Mlt 'Injective Diagram 'Empty N0 N0 (Op (Orientation Symbol))
xecfT' X (Diagram 'Empty N0 N0 (Op (Orientation Symbol)))
forall x. XStandard x => X x
xStandard LimitsG
  Cone Mlt 'Injective Diagram 'Empty N0 N0 (Op (Orientation Symbol))
tps' -- initials

      ]
  where
    xecT :: XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
xecT   = X Symbol
-> XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeG c s p d t n m (Orientation x)
xEligibleConeGOrnt X Symbol
forall x. XStandard x => X x
xStandard
    xecfT :: XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
xecfT  = X Symbol
-> XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeFactorG c s p d t n m (Orientation x)
xEligibleConeFactorGOrnt X Symbol
forall x. XStandard x => X x
xStandard 
    tps :: LimitsG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
tps    = Symbol
-> LimitsG
     Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
forall p. Entity p => p -> Terminals (Orientation p)
trmsOrnt Symbol
T

    xecT' :: XEligibleConeG
  Cone
  Mlt
  (Dual 'Projective)
  Diagram
  (Dual 'Empty)
  N0
  N0
  (Op (Orientation Symbol))
xecT'  = XEligibleConeG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
-> XEligibleConeG
     Cone
     Mlt
     (Dual 'Projective)
     Diagram
     (Dual 'Empty)
     N0
     N0
     (Op (Orientation Symbol))
forall x s
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x,
 NaturalConicBi (Inv2 (HomDisjEmpty s Op)) c s p d t n m,
 s ~ Mlt) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeG c s (Dual p) d (Dual t) n m (Op x)
coXEligibleConeG XEligibleConeG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
xecT
    xecfT' :: XEligibleConeFactorG
  Cone
  Mlt
  (Dual 'Projective)
  Diagram
  (Dual 'Empty)
  N0
  N0
  (Op (Orientation Symbol))
xecfT' = XEligibleConeFactorG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
-> XEligibleConeFactorG
     Cone
     Mlt
     (Dual 'Projective)
     Diagram
     (Dual 'Empty)
     N0
     N0
     (Op (Orientation Symbol))
forall x s
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x,
 NaturalConicBi (Inv2 (HomDisjEmpty s Op)) c s p d t n m,
 s ~ Mlt) =>
XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m (Op x)
coXEligibleConeFactorG XEligibleConeFactorG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
xecfT
    tps' :: LimitsG
  Cone Mlt 'Injective Diagram 'Empty N0 N0 (Op (Orientation Symbol))
tps'   = LimitsG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
-> LimitsG
     Cone Mlt 'Injective Diagram 'Empty N0 N0 (Op (Orientation Symbol))
forall x (o :: * -> *).
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableMultiplicative Mlt o) =>
Terminals x -> Initials (o x)
coTerminals LimitsG
  Cone Mlt 'Projective Diagram 'Empty N0 N0 (Orientation Symbol)
tps