{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Limes.Definition
-- Description : definition of a limes of a diagram.
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- definition of a 'Limes' of a 'Diagram'.
module OAlg.Limes.Definition
  (
    -- * Limes
    Limes(..)
  , universalPoint
  , universalCone
  , universalShell
  , universalFactor
  , diagram, lmDiagramTypeRefl
  , eligibleCone
  , eligibleFactor
  , lmMap

    -- * Duality
  , lmToOp, lmFromOp, LimesDuality(..)
  , coLimes, coLimesInv, lmFromOpOp

    -- * Construction
  , lmToPrjOrnt, lmFromInjOrnt
  
    -- * Proposition
  , relLimes

    -- * Exception
  , LimesException(..)

  ) where

import Control.Monad (fmap)
import Data.Typeable
import Data.List as L ((++))

import OAlg.Prelude

import OAlg.Entity.Diagram
import OAlg.Entity.FinList

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.Limes.Cone

--------------------------------------------------------------------------------
-- LimesException -

-- | limes exceptions which are sub exceptions from 'SomeOAlgException'.
data LimesException
  = ConeNotEligible String
  deriving (LimesException -> LimesException -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LimesException -> LimesException -> Bool
$c/= :: LimesException -> LimesException -> Bool
== :: LimesException -> LimesException -> Bool
$c== :: LimesException -> LimesException -> Bool
Eq,Int -> LimesException -> ShowS
[LimesException] -> ShowS
LimesException -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LimesException] -> ShowS
$cshowList :: [LimesException] -> ShowS
show :: LimesException -> String
$cshow :: LimesException -> String
showsPrec :: Int -> LimesException -> ShowS
$cshowsPrec :: Int -> LimesException -> ShowS
Show)

instance Exception LimesException where
  toException :: LimesException -> SomeException
toException   = forall e. Exception e => e -> SomeException
oalgExceptionToException
  fromException :: SomeException -> Maybe LimesException
fromException = forall e. Exception e => SomeException -> Maybe e
oalgExceptionFromException

--------------------------------------------------------------------------------
-- Limes -

-- | limes of a diagram, i.e. a distinguished cone over a given diagram
-- having the following /universal/ property
--
-- __Property__ Let __@a@__ be a 'Multiplicative' structure and
-- @u@ in @'Limes' __s__ __p__ __t__ __n__ __m__ __a__@ then holds:
-- Let @l = 'universalCone' u@ in
--
-- (1) @l@ is 'valid'.
--
-- (2) @'eligibleCone' u l@.
--
-- (3) @'eligibleFactor' u l ('one' ('tip' l))@.
--
-- (4) For all @c@ in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ with
-- @'eligibleCone' u c@ holds: Let @f = 'universalFactor' u c@ in
--
--     (1) @f@ is 'valid'.
--
--     (2) @'eligibleFactor' u c f@.
--
--     (3) For all @x@ in __@a@__ with @'eligibleFactor' u c x@
--     holds: @x '==' f@.
--
-- __Note__
--
-- (1) #Nt1#As the function @'universalFactor' l@ for a given limes @l@ is uniquely
-- determined by the underlying cone of @l@, it is permissible to test equality of two
-- limits just by there underling cones. In every computation equal limits
-- can be safely replaced by each other.
--
-- (2) It is not required that the evaluation of universal factor on a non eligible cone
--  yield an exception! The implementation of the general algorithms for limits do not
--  check for eligibility.
data Limes s p t n m a where
  LimesProjective :: Cone s Projective t n m a -> (Cone s Projective t n m a -> a)
            -> Limes s Projective t n m a
  LimesInjective :: Cone s Injective t n m a -> (Cone s Injective t n m a -> a)
            -> Limes s Injective t n m a


instance Oriented a => Show (Limes s p t n m a) where
  show :: Limes s p t n m a -> String
show (LimesProjective Cone s 'Projective t n m a
l Cone s 'Projective t n m a -> a
_) = String
"LimesProjective[" forall a. [a] -> [a] -> [a]
L.++ forall a. Show a => a -> String
show Cone s 'Projective t n m a
l forall a. [a] -> [a] -> [a]
L.++ String
"]"
  show (LimesInjective Cone s 'Injective t n m a
l Cone s 'Injective t n m a -> a
_)  = String
"LimesInjective[" forall a. [a] -> [a] -> [a]
L.++ forall a. Show a => a -> String
show Cone s 'Injective t n m a
l forall a. [a] -> [a] -> [a]
L.++ String
"]"

-- | see "OAlg.Limes.Definition#Nt1"
instance Oriented a => Eq (Limes s p t n m a) where
  LimesProjective Cone s 'Projective t n m a
l Cone s 'Projective t n m a -> a
_ == :: Limes s p t n m a -> Limes s p t n m a -> Bool
== LimesProjective Cone s 'Projective t n m a
l' Cone s 'Projective t n m a -> a
_  = Cone s 'Projective t n m a
l forall a. Eq a => a -> a -> Bool
== Cone s 'Projective t n m a
l'
  LimesInjective Cone s 'Injective t n m a
l Cone s 'Injective t n m a -> a
_ == LimesInjective Cone s 'Injective t n m a
l' Cone s 'Injective t n m a -> a
_    = Cone s 'Injective t n m a
l forall a. Eq a => a -> a -> Bool
== Cone s 'Injective t n m a
l'

--------------------------------------------------------------------------------
-- universalCone -

-- | the underlying universal cone of a limes.
universalCone :: Limes s p t n m a -> Cone s p t n m a
universalCone :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone (LimesProjective Cone s 'Projective t n m a
l Cone s 'Projective t n m a -> a
_) = Cone s 'Projective t n m a
l
universalCone (LimesInjective Cone s 'Injective t n m a
l Cone s 'Injective t n m a -> a
_)  = Cone s 'Injective t n m a
l

--------------------------------------------------------------------------------
-- universalPoint -

-- | the universal point of a limes, i.e. the tip of the universal cone.
universalPoint :: Limes s p t n m a -> Point a
universalPoint :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Point a
universalPoint = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone

--------------------------------------------------------------------------------
-- universalShell -

-- | the shell of the universal cone.
universalShell :: Limes s p t n m a -> FinList n a
universalShell :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> FinList n a
universalShell = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone

--------------------------------------------------------------------------------
-- diagram -

-- | the underlying diagram of a limes.
diagram :: Limes s p t n m a -> Diagram t n m a
diagram :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone

--------------------------------------------------------------------------------
-- lmDiagramTypeRefl -

-- | reflexivity of the underlying diagram type.
lmDiagramTypeRefl :: Limes s p t n m a -> Dual (Dual t) :~: t
lmDiagramTypeRefl :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Dual (Dual t) :~: t
lmDiagramTypeRefl (LimesProjective Cone s 'Projective t n m a
l Cone s 'Projective t n m a -> a
_) = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Dual t) :~: t
cnDiagramTypeRefl Cone s 'Projective t n m a
l
lmDiagramTypeRefl (LimesInjective Cone s 'Injective t n m a
l Cone s 'Injective t n m a -> a
_)  = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Dual t) :~: t
cnDiagramTypeRefl Cone s 'Injective t n m a
l

--------------------------------------------------------------------------------
-- universalFactor -

-- | the universal factor of a 'Limes' @l@ to a given eligible cone.
--
-- __Property__ Let @l@ be in @'Limes' __s__ __p__ __t__ __n__ __m__ __a__@ then holds:
-- For all @c@ in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ with @'eligibleCone' l c@
-- holds: @'eligibleFactor' l c ('universalFactor' l c)@.
universalFactor :: Limes s p t n m a -> Cone s p t n m a -> a
universalFactor :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor (LimesProjective Cone s 'Projective t n m a
_ Cone s 'Projective t n m a -> a
u) = Cone s 'Projective t n m a -> a
u
universalFactor (LimesInjective Cone s 'Injective t n m a
_ Cone s 'Injective t n m a -> a
u)  = Cone s 'Injective t n m a -> a
u

--------------------------------------------------------------------------------
-- eligibleCone -

-- | eligibility of a cone with respect to a limes.
--
-- __Property__ Let @u@ be in @'Limes' __s__ __p__ __t__ __n__ __m__ __a__@
-- and @c@ in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ then holds:
-- @'eligibleCone' u c@ is true if and only if @'diagram' u '==' 'cnDiagram' c@ is true.
eligibleCone :: Oriented a => Limes s p t n m a -> Cone s p t n m a -> Bool
eligibleCone :: forall a s (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
Oriented a =>
Limes s p t n m a -> Cone s p t n m a -> Bool
eligibleCone Limes s p t n m a
u Cone s p t n m a
c = 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
u forall a. Eq a => a -> a -> Bool
== forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone s p t n m a
c 

--------------------------------------------------------------------------------
-- eligibleFactor -

-- | eligibility of a factor with respect to a limes and a cone.
--
-- __Property__ Let @u@ be in @'Limes' __s__ __p__ __t__ __n__ __m__ __a__@,
-- @c@ in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ with @'eligibleCone' u c@
-- and @x@ in __@a@__ then holds:
--
-- (1) If @u@ matches @'LimesProjective' l _@ then holds: @'eligibleFactor' u c x@ is true
-- if and only if @'cnEligibleFactor' x c l@ is true.
--
-- (2) If @u@ matches @'LimesInjective' l _@ then holds: @'eligibleFactor' u c x@ is true
-- if and only if @'cnEligibleFactor' x l c@ is true.
eligibleFactor :: Limes s p t n m a -> Cone s p t n m a -> a -> Bool
eligibleFactor :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a -> Bool
eligibleFactor (LimesProjective Cone s 'Projective t n m a
l Cone s 'Projective t n m a -> a
_) Cone s p t n m a
c a
x = forall a s (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
a -> Cone s p t n m a -> Cone s p t n m a -> Bool
cnEligibleFactor a
x Cone s p t n m a
c Cone s 'Projective t n m a
l
eligibleFactor (LimesInjective Cone s 'Injective t n m a
l Cone s 'Injective t n m a -> a
_) Cone s p t n m a
c a
x  = forall a s (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
a -> Cone s p t n m a -> Cone s p t n m a -> Bool
cnEligibleFactor a
x Cone s 'Injective t n m a
l Cone s p t n m a
c

--------------------------------------------------------------------------------
-- lmMap -

-- | mapping between limits.
lmMap :: IsoOrt s h
  => h a b -> Limes s p t n m a -> Limes s p t n m b
lmMap :: 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 a b
h Limes s p t n m a
l = case Limes s p t n m a
l of
  LimesProjective Cone s 'Projective t n m a
t Cone s 'Projective t n m a -> a
u   -> forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective (forall {s} {h :: * -> * -> *} {a} {b} {p :: Perspective}
       {t :: DiagramType} {n :: N'} {m :: N'}.
Hom s h =>
h a b -> Cone s p t n m a -> Cone s p t n m b
t' h a b
h Cone s 'Projective t n m a
t) (forall {s} {h :: * -> * -> *} {h :: * -> * -> *} {b} {a}
       {p :: Perspective} {t :: DiagramType} {n :: N'} {m :: N'}.
(Hom s h, Applicative h, Applicative h, Cayleyan2 h) =>
h b a -> h (Cone s p t n m b) b -> Cone s p t n m a -> a
u' h a b
h Cone s 'Projective t n m a -> a
u)
  LimesInjective Cone s 'Injective t n m a
t Cone s 'Injective t n m a -> a
u -> forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> (Cone s 'Injective t n m a -> a) -> Limes s 'Injective t n m a
LimesInjective  (forall {s} {h :: * -> * -> *} {a} {b} {p :: Perspective}
       {t :: DiagramType} {n :: N'} {m :: N'}.
Hom s h =>
h a b -> Cone s p t n m a -> Cone s p t n m b
t' h a b
h Cone s 'Injective t n m a
t) (forall {s} {h :: * -> * -> *} {h :: * -> * -> *} {b} {a}
       {p :: Perspective} {t :: DiagramType} {n :: N'} {m :: N'}.
(Hom s h, Applicative h, Applicative h, Cayleyan2 h) =>
h b a -> h (Cone s p t n m b) b -> Cone s p t n m a -> a
u' h a b
h Cone s 'Injective t n m a -> a
u)
  where t' :: h a b -> Cone s p t n m a -> Cone s p t n m b
t' h a b
h Cone s p t n m a
t = forall {s} {h :: * -> * -> *} {a} {b} {p :: Perspective}
       {t :: DiagramType} {n :: N'} {m :: N'}.
Hom s h =>
h a b -> Cone s p t n m a -> Cone s p t n m b
cnMap h a b
h Cone s p t n m a
t
        u' :: h b a -> h (Cone s p t n m b) b -> Cone s p t n m a -> a
u' h b a
h h (Cone s p t n m b) b
u Cone s p t n m a
c = h b a
h forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ h (Cone s p t n m b) b
u forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall {s} {h :: * -> * -> *} {a} {b} {p :: Perspective}
       {t :: DiagramType} {n :: N'} {m :: N'}.
Hom s h =>
h a b -> Cone s p t n m a -> Cone s p t n m b
cnMap (forall (c :: * -> * -> *) x y. Cayleyan2 c => c x y -> c y x
invert2 h b a
h) Cone s p t n m a
c

--------------------------------------------------------------------------------
-- Limes - Applicative1 -

instance IsoMultiplicative h => Applicative1 h (Limes Mlt p t n m) where
  amap1 :: forall a b. h a b -> Limes Mlt p t n m a -> Limes 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 -> Limes s p t n m a -> Limes s p t n m b
lmMap
  
--------------------------------------------------------------------------------
-- Limes - Dual -

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

--------------------------------------------------------------------------------
-- coLimes -

-- | the co limes with its inverse 'coLimesInv'.
coLimes :: 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 :: 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 (LimesProjective Cone s 'Projective t n m a
l Cone s 'Projective t n m a -> a
u) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> (Cone s 'Injective t n m a -> a) -> Limes s 'Injective t n m a
LimesInjective Dual (Cone s 'Projective t n m a)
l' Cone s 'Injective (Dual t) n m (Op a) -> Op a
u' where
  l' :: Dual (Cone s 'Projective t n m a)
l' = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s 'Projective t n m a
l
  u' :: Cone s 'Injective (Dual t) n m (Op a) -> Op a
u' Cone s 'Injective (Dual t) n m (Op a)
c' = forall x. x -> Op x
Op forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cone s 'Projective t n m a -> a
u 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)
-> Dual (Cone s p t n m a)
-> Cone s p t n m a
coConeInv ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt Cone s 'Injective (Dual t) n m (Op a)
c'
coLimes ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt (LimesInjective Cone s 'Injective t n m a
l Cone s 'Injective t n m a -> a
u) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Dual (Cone s 'Injective t n m a)
l' Cone s 'Projective (Dual t) n m (Op a) -> Op a
u' where
  l' :: Dual (Cone s 'Injective t n m a)
l' = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s 'Injective t n m a
l
  u' :: Cone s 'Projective (Dual t) n m (Op a) -> Op a
u' Cone s 'Projective (Dual t) n m (Op a)
c' = forall x. x -> Op x
Op forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Cone s 'Injective t n m a -> a
u 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)
-> Dual (Cone s p t n m a)
-> Cone s p t n m a
coConeInv ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt Cone s 'Projective (Dual t) n m (Op a)
c'

--------------------------------------------------------------------------------
-- lmFromOpOp -

-- | from @'Op' '.' 'Op'@.
lmFromOpOp :: ConeStruct s a -> Dual (Dual p) :~: p -> Dual (Dual t) :~: t
  -> Limes s p t n m (Op (Op a)) -> Limes s p t n m a
lmFromOpOp :: 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 (Op (Op a))
-> Limes s p t n m a
lmFromOpOp 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 -> Limes s p t n m a -> Limes s p t n m b
lmMap 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 -> Limes s p t n m a -> Limes s p t n m b
lmMap forall a. Distributive a => IsoOp Dst (Op (Op a)) a
isoFromOpOpDst

--------------------------------------------------------------------------------
-- coLimesInv -

-- | the inverse of 'coLimes'.
coLimesInv :: ConeStruct s a
  -> Dual (Dual p) :~: p -> Dual (Dual t) :~: t
  -> Dual (Limes s p t n m a) -> Limes s p t n m a
coLimesInv :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Limes s p t n m a)
-> Limes s p t n m a
coLimesInv 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
  = 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 (Op (Op a))
-> Limes s p t n m a
lmFromOpOp ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. 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 (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

--------------------------------------------------------------------------------
-- LimesDuality -

-- | 'Op'-duality between limes types.
data LimesDuality s f g a where
  LimesDuality
    :: ConeStruct s a
    -> f a :~: Limes s p t n m a
    -> g (Op a) :~: Dual (Limes s p t n m a)
    -> Dual (Dual p) :~: p
    -> Dual (Dual t) :~: t
    -> LimesDuality s f g a

--------------------------------------------------------------------------------
-- lmToOp -

-- | to @__g__ ('Op' __a__)@.
lmToOp :: LimesDuality s f g a -> f a -> g (Op a)
lmToOp :: forall s (f :: * -> *) (g :: * -> *) a.
LimesDuality s f g a -> f a -> g (Op a)
lmToOp (LimesDuality ConeStruct s a
cs f a :~: Limes s p t n m a
Refl g (Op a) :~: Dual (Limes 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)
-> 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

--------------------------------------------------------------------------------
-- lmFromOp -

-- | from @__g__ ('Op' __a__)@.
lmFromOp :: LimesDuality s f g a -> g (Op a) -> f a
lmFromOp :: forall s (f :: * -> *) (g :: * -> *) a.
LimesDuality s f g a -> g (Op a) -> f a
lmFromOp (LimesDuality ConeStruct s a
cs f a :~: Limes s p t n m a
Refl g (Op a) :~: Dual (Limes 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 (Limes s p t n m a)
-> Limes s p t n m a
coLimesInv ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt

--------------------------------------------------------------------------------
-- relLimes -

-- | validity of a 'Limes'.
relLimes :: ConeStruct s a
  -> XOrtPerspective p a -> Limes s p t n m a -> Statement
relLimes :: 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
u = String -> Label
Label String
"Limes" Label -> Statement -> Statement
:<=>: case forall s a. ConeStruct s a -> Struct Mlt a
cnStructMlt ConeStruct s a
cs of
  Struct Mlt a
Struct -> let l :: Cone s p t n m a
l = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Limes s p t n m a
u in
    [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid Cone s p t n m a
l
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (forall a s (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
Oriented a =>
Limes s p t n m a -> Cone s p t n m a -> Bool
eligibleCone Limes s p t n m a
u Cone s p t n m a
l)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"u"String -> String -> Parameter
:=forall a. Show a => a -> String
show Limes s p t n m a
u,String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show Cone s p t n m a
l]
        , String -> Label
Label String
"3" Label -> Statement -> Statement
:<=>: (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a -> Bool
eligibleFactor Limes s p t n m a
u Cone s p t n m a
l (forall c. Multiplicative c => Point c -> c
one forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone s p t n m a
l))
            Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"u"String -> String -> Parameter
:=forall a. Show a => a -> String
show Limes s p t n m a
u,String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show Cone s p t n m a
l]
        , forall x. X x -> (x -> Statement) -> Statement
Forall (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
EligibleFactor s p t n m a -> (a, Cone s p t n m a)
elfFactorCone 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
-> XOrtPerspective p a
-> Cone s p t n m a
-> X (EligibleFactor s p t n m a)
xopEligibleFactor ConeStruct s a
cs XOrtPerspective p a
xop Cone s p t n m a
l)
            (\(a
x,Cone s p t n m a
c) -> let f :: a
f = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Limes s p t n m a
u Cone s p t n m a
c in
                [Statement] -> Statement
And [ String -> Label
Label String
"4.1" Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid a
f
                    , String -> Label
Label String
"4.2" Label -> Statement -> Statement
:<=>: (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a -> Bool
eligibleFactor Limes s p t n m a
u Cone s p t n m a
c a
f)
                        Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"u"String -> String -> Parameter
:=forall a. Show a => a -> String
show Limes s p t n m a
u,String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
x,String
"c"String -> String -> Parameter
:=forall a. Show a => a -> String
show Cone s p t n m a
c,String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
f]
                    , String -> Label
Label String
"4.3" Label -> Statement -> Statement
:<=>: (a
x forall a. Eq a => a -> a -> Bool
== a
f)
                        Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"u"String -> String -> Parameter
:=forall a. Show a => a -> String
show Limes s p t n m a
u
                                 ,String
"c"String -> String -> Parameter
:=forall a. Show a => a -> String
show Cone s p t n m a
c,String
"f"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
f,String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
x
                                 ]
                    ]
            )
        ]

--------------------------------------------------------------------------------
-- Limes - Validable -

instance (Multiplicative a, XStandardOrtPerspective p a)
  => Validable (Limes Mlt p t n m a) where
  valid :: Limes Mlt p t n m a -> Statement
valid Limes Mlt p t n m a
l = String -> Label
Label String
"Mlt" Label -> Statement -> Statement
:<=>: 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 forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall (p :: Perspective) a.
XStandardOrtPerspective p a =>
XOrtPerspective p a
xStandardOrtPerspective Limes Mlt p t n m a
l


instance ( Distributive a, XStandardOrtPerspective p a
         , Typeable p, Typeable t, Typeable n, Typeable m
         )
  => Validable (Limes Dst p t n m a) where
  valid :: Limes Dst p t n m a -> Statement
valid Limes Dst p t n m a
l = String -> Label
Label (forall a. Show a => a -> String
show forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Typeable a => a -> TypeRep
typeOf Limes Dst p t n m a
l) Label -> Statement -> Statement
:<=>: 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 forall a. Distributive a => ConeStruct Dst a
ConeStructDst forall (p :: Perspective) a.
XStandardOrtPerspective p a =>
XOrtPerspective p a
xStandardOrtPerspective Limes Dst p t n m a
l

--------------------------------------------------------------------------------
-- Limes - Entity -

instance ( Multiplicative a, XStandardOrtPerspective p a
         , Typeable p, Typeable t, Typeable n, Typeable m
         )
  => Entity (Limes Mlt p t n m a)

instance ( Distributive a, XStandardOrtPerspective p a
         , Typeable p, Typeable t, Typeable n, Typeable m
         )
  => Entity (Limes Dst p t n m a) 

--------------------------------------------------------------------------------
-- lmToPrjOrnt -

-- | projective limes on oriented structures.
lmToPrjOrnt :: (Entity p, a ~ Orientation p)
  => p -> Diagram t n m a -> Limes Mlt Projective t n m a
lmToPrjOrnt :: 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 p
t Diagram t n m a
d = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective t n m (Orientation p)
l Cone Mlt 'Projective t n m a -> a
u where
    l :: Cone Mlt 'Projective t n m (Orientation p)
l = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p
-> Diagram t n m (Orientation p)
-> Cone Mlt 'Projective t n m (Orientation p)
cnPrjOrnt p
t Diagram t n m a
d
    u :: Cone Mlt 'Projective t n m a -> a
u (ConeProjective Diagram t n m a
_ Point a
x FinList n a
_) = Point a
xforall p. p -> p -> Orientation p
:>p
t

--------------------------------------------------------------------------------
-- lmFromInjOrnt -

-- | injective limes on oriented structures.
lmFromInjOrnt :: (Entity p, a ~ Orientation p)
  => p -> Diagram t n m a -> Limes Mlt Injective t n m a
lmFromInjOrnt :: 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 p
t Diagram t n m a
d = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> (Cone s 'Injective t n m a -> a) -> Limes s 'Injective t n m a
LimesInjective Cone Mlt 'Injective t n m (Orientation p)
l Cone Mlt 'Injective t n m a -> a
u where
    l :: Cone Mlt 'Injective t n m (Orientation p)
l = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p
-> Diagram t n m (Orientation p)
-> Cone Mlt 'Injective t n m (Orientation p)
cnInjOrnt p
t Diagram t n m a
d
    u :: Cone Mlt 'Injective t n m a -> a
u (ConeInjective Diagram t n m a
_ Point a
x FinList n a
_) = p
tforall p. p -> p -> Orientation p
:>Point a
x