{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Limits.Proposition

-- Description : propositions for limits.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- duality for 'LimitsG'.

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

    prpLimitsG
  ) where

import OAlg.Prelude

import OAlg.Entity.Diagram

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

import OAlg.Limes.Limits.Core

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

-- prpLimitsG -


-- | validity according to 'LimitsG'.

prpLimitsG ::
  ( Conic c
  , Diagrammatic d
  , Show (c s p d t n m x)
  , Validable (c s p d t n m x)
  , Entity (d t n m x)
  , Entity x
  )
  => XEligibleConeG c s p d t n m x
  -> XEligibleConeFactorG 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 :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG 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 XEligibleConeG c s p d t n m x
xec XEligibleConeFactorG c s p d t n m x
xef X (d t n m x)
xd LimitsG c s p d t n m x
l = String -> Label
Prp String
"LimitsG" Label -> Statement -> Statement
:<=>: X (d t n m x) -> (d t n m x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (d t n m x)
xd (XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> LimesG c s p d t n m x
-> Statement
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> LimesG c s p d t n m x
-> Statement
prpLimes XEligibleConeG c s p d t n m x
xec XEligibleConeFactorG c s p d t n m x
xef (LimesG c s p d t n m x -> Statement)
-> (d t n m x -> LimesG c s p d t n m x) -> d t n m x -> Statement
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 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
l)

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

-- LimitsG - Validable -


instance
  ( Conic c
  , Diagrammatic d
  , XStandardEligibleConeG c s p d t n m x
  , XStandardEligibleConeFactorG c s p d t n m x
  , XStandard (d t n m x)
  , Show (c s p d t n m x)
  , Validable (c s p 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 :: LimitsG c s p d t n m x -> Statement
valid = XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> X (d t n m x)
-> LimitsG c s p d t n m x
-> Statement
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG 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 XEligibleConeG 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.
XStandardEligibleConeG c s p d t n m x =>
XEligibleConeG c s p d t n m x
xStandardEligibleConeG XEligibleConeFactorG 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.
XStandardEligibleConeFactorG c s p d t n m x =>
XEligibleConeFactorG c s p d t n m x
xStandardEligibleConeFactorG X (d t n m x)
forall x. XStandard x => X x
xStandard