{-# 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

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

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

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

      , String -> Label
Label String
"PullbacksAndPushouts" Label -> Statement -> Statement
:<=>:
          forall x. X x -> (x -> Statement) -> Statement
Exist X SomeNatural
xN (\(SomeNatural W n
n) -> String -> Label
Label (forall a. Show a => a -> String
show W n
n) Label -> Statement -> Statement
:<=>:
                      forall a. Validable a => a -> Statement
valid (forall a (p :: N' -> *) (n :: N').
Multiplicative a =>
p n -> Pushouts ('S N1) a -> Pushouts n a
pushouts' W n
n (forall p (n :: N'). Entity p => p -> Pushouts n (Orientation p)
pushoutsOrnt Symbol
I))
                   )
      , String -> Label
Label String
"plbPrdEql2" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid (forall a.
Multiplicative a =>
Products ('S N1) a -> Equalizers ('S N1) a -> Pullbacks ('S N1) a
plbPrdEql2 (forall p (n :: N'). Entity p => p -> Products n (Orientation p)
productsOrnt Symbol
P) (forall p (n :: N'). Entity p => p -> Equalizers n (Orientation p)
equalizersOrnt Symbol
E))    

      , String -> Label
Label String
"KernelsAndCokernels" Label -> Statement -> Statement
:<=>:
          forall x. X x -> (x -> Statement) -> Statement
Exist X SomeNatural
xN (\(SomeNatural W n
n) -> String -> Label
Label (forall a. Show a => a -> String
show W n
n) Label -> Statement -> Statement
:<=>:
                      forall a. Validable a => a -> Statement
valid (forall a (p :: N' -> *) (n :: N').
Distributive a =>
p n -> Cokernels N1 a -> Cokernels n a
cokernels' W n
n (forall p (n :: N'). Entity p => p -> Cokernels n (Orientation p)
cokernelsOrnt Symbol
I))
                   )
      ]
  where xN :: X SomeNatural
xN = forall a. [a] -> X a
xOneOf forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. N -> [a] -> [a]
takeN N
20 [SomeNatural]
naturals