{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Limes.Proposition
-- Description : propositions on limits
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- propositions on 'OAlg.Limes.Limits.Limits'.
module OAlg.Limes.Proposition
  (
    prpLimitsOrntSymbol
  )
  where

import Data.Typeable

import OAlg.Prelude

import OAlg.Data.Symbol

import OAlg.Structure.Oriented

import OAlg.Entity.Natural

import OAlg.Limes.TerminalAndInitialPoint
import OAlg.Limes.MinimaAndMaxima
import OAlg.Limes.ProductsAndSums
import OAlg.Limes.EqualizersAndCoequalizers
import OAlg.Limes.PullbacksAndPushouts
import OAlg.Limes.KernelsAndCokernels
import OAlg.Limes.Exact.Deviation

--------------------------------------------------------------------------------
-- prpLimitsOrntSymbol -

-- | validity of 'OAlg.Limes.Limits.Limits' for @'Orientation' 'Symbol'@.
prpLimitsOrntSymbol :: N -> Statement
prpLimitsOrntSymbol :: N -> Statement
prpLimitsOrntSymbol N
n' = String -> Label
Prp String
"LimesOrntSymbol" Label -> Statement -> Statement
:<=>: String -> Label
Label (N -> String
forall a. Show a => a -> String
show N
n') Label -> Statement -> Statement
:<=>:
  case N -> SomeNatural
someNatural N
n' of
    SomeNatural W n
n
      -> [Statement] -> Statement
And [ String -> Label
Label String
"TerminalAndInitialPoint" Label -> Statement -> Statement
:<=>:
               (Symbol -> InitialPoint OS) -> Statement
forall a. Validable a => a -> Statement
valid (Symbol -> InitialPoint OS
forall p. Entity p => p -> InitialPoint (Orientation p)
initialPointOrnt :: Symbol -> InitialPoint OS)
                  
             , String -> Label
Label String
"MinimaAndMaxima" Label -> Statement -> Statement
:<=>:
                 [Statement] -> Statement
And [ LimitsG Cone Mlt 'Injective Diagram ('Chain 'To) ('S n) n OS
-> Statement
forall a. Validable a => a -> Statement
valid (W n -> Proxy OS -> Maxima 'To n OS
forall x (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative x =>
p n -> f x -> Maxima 'To n x
maximaTo' W n
n (Proxy OS
forall {k} (t :: k). Proxy t
Proxy :: Proxy OS))
                     , LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n OS
-> Statement
forall a. Validable a => a -> Statement
valid (W n -> Proxy OS -> Maxima 'From n OS
forall x (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative x =>
p n -> f x -> Maxima 'From n x
maximaFrom' W n
n (Proxy OS
forall {k} (t :: k). Proxy t
Proxy :: Proxy OS))
                     ]

             , String -> Label
Label String
"ProductsAndSums" Label -> Statement -> Statement
:<=>:
                 Sums n OS -> Statement
forall a. Validable a => a -> Statement
valid (W n -> Sums 'N0 OS -> Sums ('S N1) OS -> Sums n OS
forall a (p :: N' -> *) (n :: N').
Multiplicative a =>
p n -> Sums 'N0 a -> Sums ('S N1) a -> Sums n a
sums' W n
n (Symbol -> Sums 'N0 OS
forall p (n :: N'). Entity p => p -> Sums n (Orientation p)
sumsOrnt Symbol
I) (Symbol -> Sums ('S N1) OS
forall p (n :: N'). Entity p => p -> Sums n (Orientation p)
sumsOrnt Symbol
I))
                      
             , String -> Label
Label String
"EqualizersAndCoEqualizers" Label -> Statement -> Statement
:<=>:
                 Coequalizers n OS -> Statement
forall a. Validable a => a -> Statement
valid (W n
-> Sums ('S N1) OS -> Coequalizers ('S N1) OS -> Coequalizers n OS
forall x (p :: N' -> *) (n :: N').
Multiplicative x =>
p n -> Sums ('S N1) x -> Coequalizers ('S N1) x -> Coequalizers n x
coequalizers' W n
n (Symbol -> Sums ('S N1) OS
forall p (n :: N'). Entity p => p -> Sums n (Orientation p)
sumsOrnt Symbol
I) (Symbol -> Coequalizers ('S N1) OS
forall p (n :: N'). Entity p => p -> Coequalizers n (Orientation p)
coequalizersOrnt Symbol
I))


             , String -> Label
Label String
"PullbacksAndPushouts" Label -> Statement -> Statement
:<=>:
                 LimitsG Cone Mlt 'Injective Diagram ('Star 'From) ('S n) n OS
-> Statement
forall a. Validable a => a -> Statement
valid (W n -> Pushouts ('S N1) OS -> Pushouts n OS
forall x (p :: N' -> *) (n :: N').
Multiplicative x =>
p n -> Pushouts ('S N1) x -> Pushouts n x
pushouts' W n
n (Symbol -> Pushouts ('S N1) OS
forall p (n :: N'). Entity p => p -> Pushouts n (Orientation p)
pushoutsOrnt Symbol
I))

             , String -> Label
Label String
"plbPrdEql2" Label -> Statement -> Statement
:<=>:
                 LimitsG
  Cone Mlt 'Projective Diagram ('Star 'To) ('S ('S N1)) ('S N1) OS
-> Statement
forall a. Validable a => a -> Statement
valid (Products ('S N1) OS
-> Equalizers ('S N1) OS -> Pullbacks ('S N1) OS
forall x.
Multiplicative x =>
Products ('S N1) x -> Equalizers ('S N1) x -> Pullbacks ('S N1) x
plbPrdEql2 (Symbol -> Products ('S N1) OS
forall p (n :: N'). Entity p => p -> Products n (Orientation p)
productsOrnt Symbol
P) (Symbol -> Equalizers ('S N1) OS
forall p (n :: N'). Entity p => p -> Equalizers n (Orientation p)
equalizersOrnt Symbol
E))    


             , String -> Label
Label String
"KernelsAndCokernels" Label -> Statement -> Statement
:<=>:
                 Cokernels n OS -> Statement
forall a. Validable a => a -> Statement
valid (W n -> Cokernels N1 OS -> Cokernels n OS
forall x (q :: N' -> *) (n :: N').
Distributive x =>
q n -> Cokernels N1 x -> Cokernels n x
cokernels' W n
n (Symbol -> Cokernels N1 OS
forall p (n :: N'). Entity p => p -> Cokernels n (Orientation p)
cokernelsOrnt Symbol
I))

             , String -> Label
Label String
"Deviation" Label -> Statement -> Statement
:<=>: Statement
prpDeviationOrntSymbol
             ]