{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Limits.Core

-- Description : basic definition for limits of diagrammatic objects.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- basic definition for a 'LimesG' of diagrammatic object.

module OAlg.Limes.Limits.Core
  (
    -- * Limits

    limes, LimitsG(..), Limits
  , limesCone, limitsCone

    -- * Constructions

  , lmsMltPrjOrnt, lmsMltInjOrnt
  ) where

import OAlg.Prelude

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

import OAlg.Entity.Diagram

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

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

-- LimitsG -


-- | limes of a diagrammatic object, i.e. assigning to each diagrammatic object @d@ a limes over the

-- @d@.

--

-- __Property__ Let @l@ be in @'LimitsG' __c s p d t n m x__@ for a @'Conic' __c__@ and a

-- @'Diagrammatic' __d__@, then holds:

--

-- (1) @'diagram' '.' 'cone' '.' 'universalCone' '.' 'limes' l '.=.' 'diagram'@.

newtype LimitsG c s p d t n m x = LimitsG (d t n m x -> LimesG c s p d t n m x)

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

-- Limits -


-- | limits for 'Cone's over 'Diagram's.

type Limits s p = LimitsG Cone s p Diagram

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

-- limes -


-- | the limes over the given diagram.

limes :: LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes (LimitsG d t n m x -> LimesG c s p d t n m x
l) = d t n m x -> LimesG c s p d t n m x
l

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

-- limesCone -


-- | the underlying limes according to 'Cone' , given by a diagrammatic object of @__d t n m x__@.

limesCone :: Conic c => LimitsG c s p d t n m x -> d t n m x -> LimesG Cone s p d t n m x
limesCone :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
LimitsG c s p d t n m x -> d t n m x -> LimesG Cone s p d t n m x
limesCone LimitsG c s p d t n m x
lG d t n m x
d = case LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG c s p d t n m x
lG d t n m x
d of
  LimesProjective c s 'Projective d t n m x
cCn Cone s 'Projective d t n m x -> x
cUniv -> Cone s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG Cone s 'Projective d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective (c s 'Projective d t n m x -> Cone s 'Projective d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone c s 'Projective d t n m x
cCn) Cone s 'Projective d t n m x -> x
cUniv
  LimesInjective c s 'Injective d t n m x
cCn Cone s 'Injective d t n m x -> x
cUniv  -> Cone s 'Injective d t n m x
-> (Cone s 'Injective d t n m x -> x)
-> LimesG Cone s 'Injective d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Injective d t n m x
-> (Cone s 'Injective d t n m x -> x)
-> LimesG c s 'Injective d t n m x
LimesInjective (c s 'Injective d t n m x -> Cone s 'Injective d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone c s 'Injective d t n m x
cCn) Cone s 'Injective d t n m x -> x
cUniv

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

-- limitsCone -


-- | the underlying limits according to 'Cone'.

limitsCone :: Conic c => LimitsG c s p d t n m x -> LimitsG Cone s p d t n m x
limitsCone :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
LimitsG c s p d t n m x -> LimitsG Cone s p d t n m x
limitsCone = (d t n m x -> LimesG Cone s p d t n m x)
-> LimitsG Cone s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG ((d t n m x -> LimesG Cone s p d t n m x)
 -> LimitsG Cone s p d t n m x)
-> (LimitsG c s p d t n m x
    -> d t n m x -> LimesG Cone s p d t n m x)
-> LimitsG c s p d t n m x
-> LimitsG Cone s p d t n m x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. LimitsG c s p d t n m x -> d t n m x -> LimesG Cone s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
LimitsG c s p d t n m x -> d t n m x -> LimesG Cone s p d t n m x
limesCone

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

-- lmsMltPrjOrnt -


-- | projective limits for 'Multiplicative' structures over @'Orientation' __p__@ .

lmsMltPrjOrnt :: Entity p => p -> Limits Mlt Projective t n m (Orientation p)
lmsMltPrjOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsMltPrjOrnt = (Diagram t n m (Orientation p)
 -> LimesG Cone Mlt 'Projective Diagram t n m (Orientation p))
-> Limits Mlt 'Projective t n m (Orientation p)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG ((Diagram t n m (Orientation p)
  -> LimesG Cone Mlt 'Projective Diagram t n m (Orientation p))
 -> Limits Mlt 'Projective t n m (Orientation p))
-> (p
    -> Diagram t n m (Orientation p)
    -> LimesG Cone Mlt 'Projective Diagram t n m (Orientation p))
-> p
-> Limits Mlt 'Projective t n m (Orientation p)
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. p
-> Diagram t n m (Orientation p)
-> LimesG Cone Mlt 'Projective Diagram t n m (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

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

-- lmsMltInjOrnt -


-- | injective limits for 'Multiplicative' structures over @'Orientation' __p__@.

lmsMltInjOrnt :: Entity p => p -> Limits Mlt Injective t n m (Orientation p)
lmsMltInjOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsMltInjOrnt = (Diagram t n m (Orientation p)
 -> LimesG Cone Mlt 'Injective Diagram t n m (Orientation p))
-> Limits Mlt 'Injective t n m (Orientation p)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG ((Diagram t n m (Orientation p)
  -> LimesG Cone Mlt 'Injective Diagram t n m (Orientation p))
 -> Limits Mlt 'Injective t n m (Orientation p))
-> (p
    -> Diagram t n m (Orientation p)
    -> LimesG Cone Mlt 'Injective Diagram t n m (Orientation p))
-> p
-> Limits Mlt 'Injective t n m (Orientation p)
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. p
-> Diagram t n m (Orientation p)
-> LimesG Cone Mlt 'Injective Diagram t n m (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  

{-
--------------------------------------------------------------------------------
-- LimitsG - Dual -

type instance Dual1 (LimitsG c s p d t n m) = LimitsG c s (Dual p) d (Dual t) n m

--------------------------------------------------------------------------------
-- lmsMapCov -

lmsMapCov :: NaturalConic h c s p d t n m
  => Variant2 Covariant (Inv2 h) x y
  -> LimitsG c s p d t n m x -> LimitsG c s p d t n m y
lmsMapCov i@(Covariant2 (Inv2 _ f)) (LimitsG u) = LimitsG u' where
  u' d' = lmMapCov i (u d) where
    SDualBi (Right1 (DiagramG d)) = amapF f (SDualBi (Right1 (DiagramG d'))) 

--------------------------------------------------------------------------------
-- lmsMapCnt -

lmsMapCnt :: NaturalConic h c s p d t n m
  => Variant2 Contravariant (Inv2 h) x y
  -> LimitsG c s p d t n m x -> Dual1 (LimitsG c s p d t n m) y
lmsMapCnt i@(Contravariant2 (Inv2 _ f)) (LimitsG u) = LimitsG u' where
  u' d' = lmMapCnt i (u d) where
    SDualBi (Right1 (DiagramG d)) = amapF f (SDualBi (Left1 (DiagramG d'))) 

--------------------------------------------------------------------------------
-- lmsMapS -

lmsMapS ::
  ( NaturalConic h c s p d t n m
  , NaturalConic h c s (Dual p) d (Dual t) n m
  )
  => Inv2 h x y -> SDualBi (LimitsG c s p d t n m) x -> SDualBi (LimitsG c s p d t n m) y
lmsMapS = vmapBi lmsMapCov lmsMapCov lmsMapCnt lmsMapCnt

--------------------------------------------------------------------------------
-- FunctorialG -

instance NaturalConicBi h c s p d t n m
  => ApplicativeG (SDualBi (LimitsG c s p d t n m)) (Inv2 h) (->) where
  amapG = lmsMapS

instance NaturalConicBi h c s p d t n m
  => FunctorialG (SDualBi (LimitsG c s p d t n m)) (Inv2 h) (->)

--------------------------------------------------------------------------------
-- prpLimitsG -

-- | validity according to 'LimitsG'.
prpLimitsG ::
  ( Conic c
  , Diagrammatic d
  , Entity (d t n m x)
  , Entity x
  )
  => XEligibleCone c s p d t n m x
  -> XEligibleConeFactor 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 xec xef xd l = Prp "LimitsG" :<=>: Forall xd (prpLimes xec xef . limes l)

--------------------------------------------------------------------------------
-- LimitsG - Validable -

instance
  ( Conic c
  , Diagrammatic d
  , XStandardEligibleCone c s p d t n m x
  , XStandardEligibleConeFactor c s p d t n m x
  , XStandard (d t n m x)
  , Entity (d t n m x)
  , Entity x
  )
  => Validable (LimitsG c s p d t n m x) where
  valid = prpLimitsG xStandardEligibleCone xStandardEligibleConeFactor xStandard
-}