{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

-- |
-- 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' 'OAlg.Entity.Diagram.Definition.Empty'@.
module OAlg.Limes.TerminalAndInitialPoint
  (
    -- * Terminal
    Terminals, TerminalPoint, TerminalCone, TerminalDiagram
  , trmDiagram, trmCone

    -- ** Orientation
  , terminalPointOrnt, trmsOrnt
    

    -- * Initial
  , Initials, InitialPoint, InitialCone, InitialDiagram
  , intDiagram, intCone

    -- ** Orientation
  , initialPointOrnt, intsOrnt

    -- * Duality
    -- ** Terminal
  , trmDiagramDuality
  , trmConeDuality
  , trmLimesDuality
  , trmLimitsDuality

    -- ** Initial
  , intDiagramDuality
  , intConeDuality
  , intLimesDuality
  , intLimitsDuality

  ) where

import Data.Typeable

import OAlg.Prelude

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.Limes.Cone.Definition
import OAlg.Limes.Definition
import OAlg.Limes.Limits

--------------------------------------------------------------------------------
-- Terminal -

-- | 'Diagram' for a terminal point.
type TerminalDiagram = Diagram 'Empty N0 N0

-- | 'Cone' for a terminal point.
type TerminalCone = Cone Mlt Projective 'Empty N0 N0

-- | terminal point as 'Limes'.
type TerminalPoint = Limes Mlt Projective 'Empty N0 N0

-- | terminal point within a 'Multiplicative' structure.
type Terminals = Limits Mlt Projective 'Empty N0 N0

--------------------------------------------------------------------------------
-- trmDiagram -

-- | the terminal diagram.
trmDiagram :: TerminalDiagram a
trmDiagram :: forall a. TerminalDiagram a
trmDiagram = forall a. TerminalDiagram a
DiagramEmpty

--------------------------------------------------------------------------------
-- trmCone -

-- | the terminal cone of a given point.
trmCone :: Multiplicative a => Point a -> TerminalCone a
trmCone :: forall a. Multiplicative a => Point a -> TerminalCone a
trmCone Point a
t = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective forall a. TerminalDiagram a
DiagramEmpty Point a
t forall a. FinList N0 a
Nil

--------------------------------------------------------------------------------
-- 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 = forall p a (t :: DiagramType) (n :: N') (m :: N').
(Entity p, a ~ Orientation p) =>
p -> Diagram t n m a -> Limes Mlt 'Projective t n m a
lmToPrjOrnt p
p forall a. TerminalDiagram a
trmDiagram

-- | terminals for 'Orientation'.
trmsOrnt :: Entity p => p -> Terminals (Orientation p)
trmsOrnt :: forall p. Entity p => p -> Terminals (Orientation p)
trmsOrnt = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsToPrjOrnt 

--------------------------------------------------------------------------------
-- Initial -

-- | 'Diagram' for a initial point.
type InitialDiagram = Diagram 'Empty N0 N0

-- | 'Cone' for a initial point.
type InitialCone = Cone Mlt Injective 'Empty N0 N0

-- | initial point as 'Limes'.
type InitialPoint = Limes Mlt Injective 'Empty N0 N0

-- | initial point within a 'Multiplicative' structure.
type Initials = Limits Mlt Injective 'Empty N0 N0

--------------------------------------------------------------------------------
-- Duality - Terminal -

-- | terminal 'Diagram' duality.
trmDiagramDuality :: Oriented a => DiagramDuality TerminalDiagram InitialDiagram a
trmDiagramDuality :: forall a.
Oriented a =>
DiagramDuality TerminalDiagram TerminalDiagram a
trmDiagramDuality = forall a (f :: * -> *) (p :: DiagramType) (t :: N') (n :: N')
       (g :: * -> *).
Oriented a =>
(f a :~: Diagram p t n a)
-> (g (Op a) :~: Dual (Diagram p t n a))
-> (Dual (Dual p) :~: p)
-> DiagramDuality f g a
DiagramDuality forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

-- | terminal 'Cone' duality.
trmConeDuality :: Multiplicative a
  => ConeDuality Mlt TerminalCone InitialCone a
trmConeDuality :: forall a.
Multiplicative a =>
ConeDuality Mlt TerminalCone InitialCone a
trmConeDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Cone s p t n m a)
-> (g (Op a) :~: Dual (Cone s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> ConeDuality s f g a
ConeDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

-- |  terminal 'Limes' duality.
trmLimesDuality :: Multiplicative a
  => LimesDuality Mlt TerminalPoint InitialPoint a
trmLimesDuality :: forall a.
Multiplicative a =>
LimesDuality Mlt TerminalPoint InitialPoint a
trmLimesDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limes s p t n m a)
-> (g (Op a) :~: Dual (Limes s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimesDuality s f g a
LimesDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

-- |  terminal 'Limits' duality.
trmLimitsDuality :: Multiplicative a
  => LimitsDuality Mlt Terminals Initials a
trmLimitsDuality :: forall a.
Multiplicative a =>
LimitsDuality Mlt Terminals Initials a
trmLimitsDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limits s p t n m a)
-> (g (Op a) :~: Dual (Limits s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimitsDuality s f g a
LimitsDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- Duality - Initial -

-- | initial 'Diagram' duality.
intDiagramDuality :: Oriented a => DiagramDuality InitialDiagram TerminalDiagram a
intDiagramDuality :: forall a.
Oriented a =>
DiagramDuality TerminalDiagram TerminalDiagram a
intDiagramDuality = forall a (f :: * -> *) (p :: DiagramType) (t :: N') (n :: N')
       (g :: * -> *).
Oriented a =>
(f a :~: Diagram p t n a)
-> (g (Op a) :~: Dual (Diagram p t n a))
-> (Dual (Dual p) :~: p)
-> DiagramDuality f g a
DiagramDuality forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

-- | initial 'Cone' duality.
intConeDuality :: Multiplicative a
  => ConeDuality Mlt InitialCone TerminalCone a
intConeDuality :: forall a.
Multiplicative a =>
ConeDuality Mlt InitialCone TerminalCone a
intConeDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Cone s p t n m a)
-> (g (Op a) :~: Dual (Cone s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> ConeDuality s f g a
ConeDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

-- | initial 'Limes' duality.
intLimesDuality :: Multiplicative a
  => LimesDuality Mlt InitialPoint TerminalPoint a
intLimesDuality :: forall a.
Multiplicative a =>
LimesDuality Mlt InitialPoint TerminalPoint a
intLimesDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limes s p t n m a)
-> (g (Op a) :~: Dual (Limes s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimesDuality s f g a
LimesDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

-- | initial 'Limits' duality.
intLimitsDuality :: Multiplicative a
  => LimitsDuality Mlt Initials Terminals a
intLimitsDuality :: forall a.
Multiplicative a =>
LimitsDuality Mlt Initials Terminals a
intLimitsDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limits s p t n m a)
-> (g (Op a) :~: Dual (Limits s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimitsDuality s f g a
LimitsDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- intDiagram -

-- | the initial diagram.
intDiagram :: InitialDiagram a
intDiagram :: forall a. TerminalDiagram a
intDiagram = forall a. TerminalDiagram a
DiagramEmpty

--------------------------------------------------------------------------------
-- intCone -

-- | the initial cone of a given point.
intCone :: Multiplicative a => Point a -> InitialCone a
intCone :: forall a. Multiplicative a => Point a -> InitialCone a
intCone Point a
i = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective t n m a
ConeInjective forall a. TerminalDiagram a
DiagramEmpty Point a
i 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 = forall p a (t :: DiagramType) (n :: N') (m :: N').
(Entity p, a ~ Orientation p) =>
p -> Diagram t n m a -> Limes Mlt 'Injective t n m a
lmFromInjOrnt p
i forall a. TerminalDiagram a
intDiagram

-- | initials.
intsOrnt :: Entity p => p -> Initials (Orientation p)
intsOrnt :: forall p. Entity p => p -> Initials (Orientation p)
intsOrnt = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsFromInjOrnt