{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Limes.Limits
-- Description : limits of diagrams
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- 'Limits' of 'Diagram's, i.e. assigning to each diagram a 'Limes' over the given diagram.
module OAlg.Limes.Limits
  (
    -- * Limits
    Limits(..), limes, lmsMap

    -- * Duality
  , lmsToOp, lmsFromOp, LimitsDuality(..)
  , coLimits, coLimitsInv, lmsFromOpOp

    -- * Construction
  , lmsToPrjOrnt, lmsFromInjOrnt
  
    -- * Proposition
  , prpLimits, prpLimitsDiagram
  ) where

import Data.Typeable

import OAlg.Prelude

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

import OAlg.Hom.Oriented
import OAlg.Hom.Multiplicative
import OAlg.Hom.Distributive

import OAlg.Entity.Diagram

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


--------------------------------------------------------------------------------
-- Limits -

-- | limes of a diagram, i.e. assigning to each diagram a limes over the given diagram.
--
-- __Property__ Let @lms@ be in @'Limits' __s__ __p__ __t__ __n__ __m__ __a__@
-- and @d@ in @'Diagram' __t__ __n__ __m__ __a__@ then holds:
-- @'diagram' ('limes' lms d) '==' d@.
newtype Limits s p t n m a
  = Limits (Diagram t n m a -> Limes s p t n m a)

--------------------------------------------------------------------------------
-- limes -

-- | the limes over the given diagram.
limes :: Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes (Limits Diagram t n m a -> Limes s p t n m a
lm) = Diagram t n m a -> Limes s p t n m a
lm

--------------------------------------------------------------------------------
-- lmsMap -

-- | mapping of limits.
lmsMap :: IsoOrt s h
  => h a b -> Limits s p t n m a -> Limits s p t n m b
lmsMap :: forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
IsoOrt s h =>
h a b -> Limits s p t n m a -> Limits s p t n m b
lmsMap h a b
h (Limits Diagram t n m a -> Limes s p t n m a
ls) = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall {s} {h :: * -> * -> *} {h :: * -> * -> *} {b} {a}
       {t :: DiagramType} {n :: N'} {m :: N'} {p :: Perspective}
       {t :: DiagramType} {n :: N'} {m :: N'}.
(Hom s h, Cayleyan2 h, FunctorialHomOriented h, Applicative h) =>
h b a
-> h (Diagram t n m b) (Limes s p t n m b)
-> Diagram t n m a
-> Limes s p t n m a
ls' h a b
h Diagram t n m a -> Limes s p t n m a
ls) where
  ls' :: h b a
-> h (Diagram t n m b) (Limes s p t n m b)
-> Diagram t n m a
-> Limes s p t n m a
ls' h b a
h h (Diagram t n m b) (Limes s p t n m b)
ls Diagram t n m a
d' = forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
IsoOrt s h =>
h a b -> Limes s p t n m a -> Limes s p t n m b
lmMap h b a
h forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ h (Diagram t n m b) (Limes s p t n m b)
ls forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap h a b
h' Diagram t n m a
d' where
    h' :: h a b
h' = forall (c :: * -> * -> *) x y. Cayleyan2 c => c x y -> c y x
invert2 h b a
h 

--------------------------------------------------------------------------------
-- Limits - Applicative1 -

instance IsoMultiplicative h => Applicative1 h (Limits Mlt p t n m) where
  amap1 :: forall a b. h a b -> Limits Mlt p t n m a -> Limits Mlt p t n m b
amap1 = forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
IsoOrt s h =>
h a b -> Limits s p t n m a -> Limits s p t n m b
lmsMap

instance IsoDistributive h => Applicative1 h (Limits Dst p t n m) where
  amap1 :: forall a b. h a b -> Limits Dst p t n m a -> Limits Dst p t n m b
amap1 = forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
IsoOrt s h =>
h a b -> Limits s p t n m a -> Limits s p t n m b
lmsMap

--------------------------------------------------------------------------------
-- Limits - Daul -

type instance Dual (Limits s p t n m a) = Limits s (Dual p) (Dual t) n m (Op a)

--------------------------------------------------------------------------------
-- coLimits -

-- | the co limits wit its inverse 'coLimitsInv'.
coLimits :: ConeStruct s a -> Dual (Dual p) :~: p -> Dual (Dual t) :~: t
  -> Limits s p t n m a -> Dual (Limits s p t n m a)
coLimits :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Limits s p t n m a
-> Dual (Limits s p t n m a)
coLimits ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt (Limits Diagram t n m a -> Limes s p t n m a
lm) = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits Diagram (Dual t) n m (Op a) -> Limes s (Dual p) (Dual t) n m (Op a)
lm' where
  lm' :: Diagram (Dual t) n m (Op a) -> Limes s (Dual p) (Dual t) n m (Op a)
lm' Diagram (Dual t) n m (Op a)
d' = case forall s a. ConeStruct s a -> Struct Mlt a
cnStructMlt ConeStruct s a
cs of
    Struct Mlt a
Struct -> forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Limes s p t n m a
-> Dual (Limes s p t n m a)
coLimes ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Diagram t n m a -> Limes s p t n m a
lm forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> Dual (Diagram t n m a) -> Diagram t n m a
coDiagramInv Dual (Dual t) :~: t
rt Diagram (Dual t) n m (Op a)
d'

--------------------------------------------------------------------------------
-- lmsFromOpOp -

-- | from the bidual.
lmsFromOpOp :: ConeStruct s a -> Dual (Dual p) :~: p -> Dual (Dual t) :~: t
  -> Limits s p t n m (Op (Op a)) -> Limits s p t n m a
lmsFromOpOp :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Limits s p t n m (Op (Op a))
-> Limits s p t n m a
lmsFromOpOp ConeStruct s a
cs Dual (Dual p) :~: p
Refl Dual (Dual t) :~: t
Refl = case ConeStruct s a
cs of
  ConeStruct s a
ConeStructMlt -> forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
IsoOrt s h =>
h a b -> Limits s p t n m a -> Limits s p t n m b
lmsMap forall a. Multiplicative a => IsoOp Mlt (Op (Op a)) a
isoFromOpOpMlt
  ConeStruct s a
ConeStructDst -> forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
IsoOrt s h =>
h a b -> Limits s p t n m a -> Limits s p t n m b
lmsMap forall a. Distributive a => IsoOp Dst (Op (Op a)) a
isoFromOpOpDst

--------------------------------------------------------------------------------
-- coLimitsInv -

-- | from the co limits, with its inverse of 'coLimits'.
coLimitsInv :: ConeStruct s a
  -> Dual (Dual p) :~: p -> Dual (Dual t) :~: t
  -> Dual (Limits s p t n m a) -> Limits s p t n m a
coLimitsInv :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Limits s p t n m a)
-> Limits s p t n m a
coLimitsInv ConeStruct s a
cs rp :: Dual (Dual p) :~: p
rp@Dual (Dual p) :~: p
Refl rt :: Dual (Dual t) :~: t
rt@Dual (Dual t) :~: t
Refl Dual (Limits s p t n m a)
lms'
  = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Limits s p t n m (Op (Op a))
-> Limits s p t n m a
lmsFromOpOp ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Limits s p t n m a
-> Dual (Limits s p t n m a)
coLimits (forall s a. ConeStruct s a -> ConeStruct s (Op a)
cnStructOp ConeStruct s a
cs) forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl Dual (Limits s p t n m a)
lms'

--------------------------------------------------------------------------------
-- LimitsDuality -

-- | 'Op'-duality between limits types.
data LimitsDuality s f g a where
  LimitsDuality :: 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

--------------------------------------------------------------------------------
-- lmsToOp -

-- | to @__g__ ('Op' __a__)@.
lmsToOp :: LimitsDuality s f g a -> f a -> g (Op a)
lmsToOp :: forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> f a -> g (Op a)
lmsToOp (LimitsDuality ConeStruct s a
cs f a :~: Limits s p t n m a
Refl g (Op a) :~: Dual (Limits s p t n m a)
Refl Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt) = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Limits s p t n m a
-> Dual (Limits s p t n m a)
coLimits ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt

--------------------------------------------------------------------------------
-- lmsFromOp -

-- | from @__g__ ('Op' __a__)@.
lmsFromOp :: LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp :: forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp (LimitsDuality ConeStruct s a
cs f a :~: Limits s p t n m a
Refl g (Op a) :~: Dual (Limits s p t n m a)
Refl Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt) = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Limits s p t n m a)
-> Limits s p t n m a
coLimitsInv ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt

--------------------------------------------------------------------------------
-- prpLimitsDiagram -

-- | validity according to 'Limits'.
prpLimitsDiagram :: ConeStruct s a -> XOrtPerspective p a
  -> Limits s p t n m a -> Diagram t n m a 
  -> Statement
prpLimitsDiagram :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> XOrtPerspective p a
-> Limits s p t n m a
-> Diagram t n m a
-> Statement
prpLimitsDiagram ConeStruct s a
cs XOrtPerspective p a
xop Limits s p t n m a
lms Diagram t n m a
d = String -> Label
Prp String
"LimesDiagram"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ case forall s a. ConeStruct s a -> Struct Mlt a
cnStructMlt ConeStruct s a
cs of
                Struct Mlt a
Struct -> (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Limes s p t n m a
lm forall a. Eq a => a -> a -> Bool
== Diagram t n m a
d) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"d"String -> String -> Parameter
:=forall a. Show a => a -> String
show Diagram t n m a
d,String
"lm"String -> String -> Parameter
:=forall a. Show a => a -> String
show Limes s p t n m a
lm]
            , forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> XOrtPerspective p a -> Limes s p t n m a -> Statement
relLimes ConeStruct s a
cs XOrtPerspective p a
xop Limes s p t n m a
lm
            ]
  where lm :: Limes s p t n m a
lm = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Limits s p t n m a
lms Diagram t n m a
d

--------------------------------------------------------------------------------
-- prpLimits -

-- | validity according to 'Limits', relative to the given random variable for 'Diagram's. 
prpLimits :: ConeStruct s a -> Limits s p t n m a
  -> X (Diagram t n m a) -> XOrtPerspective p a -> Statement
prpLimits :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> Limits s p t n m a
-> X (Diagram t n m a)
-> XOrtPerspective p a
-> Statement
prpLimits ConeStruct s a
cs Limits s p t n m a
lms X (Diagram t n m a)
xd XOrtPerspective p a
xop = String -> Label
Prp String
"Limits"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (Diagram t n m a)
xd (forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> XOrtPerspective p a
-> Limits s p t n m a
-> Diagram t n m a
-> Statement
prpLimitsDiagram ConeStruct s a
cs XOrtPerspective p a
xop Limits s p t n m a
lms)


instance ( Multiplicative a, XStandard (Diagram t n m a)
         , XStandardOrtPerspective p a
         )
  => Validable (Limits Mlt p t n m a) where
  valid :: Limits Mlt p t n m a -> Statement
valid Limits Mlt p t n m a
lm = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> Limits s p t n m a
-> X (Diagram t n m a)
-> XOrtPerspective p a
-> Statement
prpLimits forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt Limits Mlt p t n m a
lm forall x. XStandard x => X x
xStandard forall (p :: Perspective) a.
XStandardOrtPerspective p a =>
XOrtPerspective p a
xStandardOrtPerspective

instance ( Distributive a, XStandard (Diagram t n m a)
         , XStandardOrtPerspective p a
         )
  => Validable (Limits Dst p t n m a) where
  valid :: Limits Dst p t n m a -> Statement
valid Limits Dst p t n m a
lm = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> Limits s p t n m a
-> X (Diagram t n m a)
-> XOrtPerspective p a
-> Statement
prpLimits forall a. Distributive a => ConeStruct Dst a
ConeStructDst Limits Dst p t n m a
lm forall x. XStandard x => X x
xStandard forall (p :: Perspective) a.
XStandardOrtPerspective p a =>
XOrtPerspective p a
xStandardOrtPerspective

--------------------------------------------------------------------------------
-- lmsToPrjOrnt -

-- | projective limits for @'Orientation' __p__@.
lmsToPrjOrnt :: Entity p => p -> Limits Mlt Projective t n m (Orientation p)
lmsToPrjOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsToPrjOrnt = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. 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
  
--------------------------------------------------------------------------------
-- lmsFromInjOrnt -

-- | injective limits for @'Orientation' __p__@.
lmsFromInjOrnt :: Entity p => p -> Limits Mlt Injective t n m (Orientation p)
lmsFromInjOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsFromInjOrnt = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. 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