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

{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Definition.Proposition

-- Description : proposition for a limes over a digrammatic object.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- proposition of a 'Limes' over a 'Diagrammatic' object yielding a 'Conic' object.

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

    prpLimes, prpLimesFactorExist, prpLimesFactorUnique

    -- * X

  , XEligibleConeG(..), xec
  , xecMapS, xecMapCov, xecMapCnt
  , xEligibleConeGOrnt, coXEligibleConeG
  , xecDiscrete
  , XStandardEligibleConeG(..), XStandardEligibleCone
  
  , XEligibleConeFactorG(..), xecf
  , xecfMapS, xecfMapCov, xecfMapCnt
  , xEligibleConeFactorGOrnt, coXEligibleConeFactorG
  , xecfOrtSite
  , xecfEligibleCone
  , XStandardEligibleConeFactorG(..), XStandardEligibleConeFactor
  
  ) where

import Control.Monad

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Either
import OAlg.Data.Variant

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

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

import OAlg.Hom.Definition
import OAlg.Hom.Multiplicative

import OAlg.Limes.Cone

import OAlg.Limes.Definition.Core
import OAlg.Limes.Definition.Duality()

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

-- XEligibleConeG -


-- | random variable for eligible cones for a given limes.

data XEligibleConeG c s p d t n m x
  = XEligibleConeG (LimesG c s p d t n m x -> X (Cone s p d t n m x))

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

-- xec -


-- | random variable of eligible cones.

xec :: XEligibleConeG c s p d t n m x -> LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
XEligibleConeG c s p d t n m x
-> LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec (XEligibleConeG LimesG c s p d t n m x -> X (Cone s p d t n m x)
x) = LimesG c s p d t n m x -> X (Cone s p d t n m x)
x

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

-- Duality - XEligibleConeG -


type instance Dual1 (XEligibleConeG c s p d t n m) = XEligibleConeG c s (Dual p) d (Dual t) n m

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

-- xecMapCov -


-- | mapping according to a covariant isomorphism.

xecMapCov :: NaturalConicBi (Inv2 h) c s p d t n m
  => Variant2 Covariant (Inv2 h) x y
  -> XEligibleConeG c s p d t n m x -> XEligibleConeG c s p d t n m y
xecMapCov :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeG c s p d t n m x -> XEligibleConeG c s p d t n m y
xecMapCov (Covariant2 Inv2 h x y
i) (XEligibleConeG LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec) = (LimesG c s p d t n m y -> X (Cone s p d t n m y))
-> XEligibleConeG c s p d t n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(LimesG c s p d t n m x -> X (Cone s p d t n m x))
-> XEligibleConeG c s p d t n m x
XEligibleConeG LimesG c s p d t n m y -> X (Cone s p d t n m y)
xec' where
  xec' :: LimesG c s p d t n m y -> X (Cone s p d t n m y)
xec' LimesG c s p d t n m y
l' = X (Cone s p d t n m y)
xc' where
    SDualBi (Right1 LimesG c s p d t n m x
l) = Inv2 h y x
-> SDualBi (LimesG c s p d t n m) y
-> SDualBi (LimesG c s p d t n m) x
forall x y.
Inv2 h x y
-> SDualBi (LimesG c s p d t n m) x
-> SDualBi (LimesG c s p d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i) (Either1 (Dual1 (LimesG c s p d t n m)) (LimesG c s p d t n m) y
-> SDualBi (LimesG c s p d t n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s p d t n m y
-> Either1
     (LimesG c s (Dual p) d (Dual t) n m) (LimesG c s p d t n m) y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LimesG c s p d t n m y
l'))

    xc' :: X (Cone s p d t n m y)
xc' = do
      Cone s p d t n m x
c <- LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec LimesG c s p d t n m x
l
      let SDualBi (Right1 (ConeG Cone s p d t n m y
c')) = Inv2 h x y
-> SDualBi (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 h x y
i (Either1 (Dual1 (ConeG Cone s p d t n m)) (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s p d t n m x
-> Either1
     (ConeG Cone s (Dual p) d (Dual t) n m) (ConeG Cone s p d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Cone s p d t n m x -> ConeG Cone 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG Cone s p d t n m x
c))) in Cone s p d t n m y -> X (Cone s p d t n m y)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return Cone s p d t n m y
c'

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

-- xecMapCnt -


-- | mapping according to a contravariant isomorphism.

xecMapCnt :: NaturalConicBi (Inv2 h) c s p d t n m
  => Variant2 Contravariant (Inv2 h) x y
  -> XEligibleConeG c s p d t n m x -> Dual1 (XEligibleConeG c s p d t n m) y
xecMapCnt :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeG c s p d t n m x
-> Dual1 (XEligibleConeG c s p d t n m) y
xecMapCnt (Contravariant2 Inv2 h x y
i) (XEligibleConeG LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec) = (LimesG c s (Dual p) d (Dual t) n m y
 -> X (Cone s (Dual p) d (Dual t) n m y))
-> XEligibleConeG c s (Dual p) d (Dual t) n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(LimesG c s p d t n m x -> X (Cone s p d t n m x))
-> XEligibleConeG c s p d t n m x
XEligibleConeG LimesG c s (Dual p) d (Dual t) n m y
-> X (Cone s (Dual p) d (Dual t) n m y)
xec' where
  xec' :: LimesG c s (Dual p) d (Dual t) n m y
-> X (Cone s (Dual p) d (Dual t) n m y)
xec' LimesG c s (Dual p) d (Dual t) n m y
l' = X (Cone s (Dual p) d (Dual t) n m y)
xc' where
    SDualBi (Left1 Dual1 (LimesG c s (Dual p) d (Dual t) n m) x
l) = Inv2 h y x
-> SDualBi (LimesG c s (Dual p) d (Dual t) n m) y
-> SDualBi (LimesG c s (Dual p) d (Dual t) n m) x
forall x y.
Inv2 h x y
-> SDualBi (LimesG c s (Dual p) d (Dual t) n m) x
-> SDualBi (LimesG c s (Dual p) d (Dual t) n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i) (Either1
  (Dual1 (LimesG c s (Dual p) d (Dual t) n m))
  (LimesG c s (Dual p) d (Dual t) n m)
  y
-> SDualBi (LimesG c s (Dual p) d (Dual t) n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s (Dual p) d (Dual t) n m y
-> Either1
     (LimesG c s (Dual (Dual p)) d (Dual (Dual t)) n m)
     (LimesG c s (Dual p) d (Dual t) n m)
     y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LimesG c s (Dual p) d (Dual t) n m y
l'))

    xc' :: X (Cone s (Dual p) d (Dual t) n m y)
xc' = do
      Cone s p d t n m x
c <- LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec Dual1 (LimesG c s (Dual p) d (Dual t) n m) x
LimesG c s p d t n m x
l
      let SDualBi (Left1 (ConeG Cone s (Dual p) d (Dual t) n m y
c')) = Inv2 h x y
-> SDualBi (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 h x y
i (Either1 (Dual1 (ConeG Cone s p d t n m)) (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s p d t n m x
-> Either1
     (ConeG Cone s (Dual p) d (Dual t) n m) (ConeG Cone s p d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Cone s p d t n m x -> ConeG Cone 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG Cone s p d t n m x
c))) in Cone s (Dual p) d (Dual t) n m y
-> X (Cone s (Dual p) d (Dual t) n m y)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return Cone s (Dual p) d (Dual t) n m y
c'

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

-- xecMapS -


-- | mapping of a 'XEligibleConeG'.

xecMapS :: NaturalConicBi (Inv2 h) c s p d t n m
  => Inv2 h x y
  -> SDualBi (XEligibleConeG c s p d t n m) x -> SDualBi (XEligibleConeG c s p d t n m) y
xecMapS :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Inv2 h x y
-> SDualBi (XEligibleConeG c s p d t n m) x
-> SDualBi (XEligibleConeG c s p d t n m) y
xecMapS = (Variant2 'Covariant (Inv2 h) x y
 -> XEligibleConeG c s p d t n m x
 -> XEligibleConeG c s p d t n m y)
-> (Variant2 'Covariant (Inv2 h) x y
    -> Dual1 (XEligibleConeG c s p d t n m) x
    -> Dual1 (XEligibleConeG c s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> XEligibleConeG c s p d t n m x
    -> Dual1 (XEligibleConeG c s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> Dual1 (XEligibleConeG c s p d t n m) x
    -> XEligibleConeG c s p d t n m y)
-> Inv2 h x y
-> SDualBi (XEligibleConeG c s p d t n m) x
-> SDualBi (XEligibleConeG c s p d t n m) y
forall (h :: * -> * -> *) x y (d :: * -> *).
Disjunctive2 h =>
(Variant2 'Covariant h x y -> d x -> d y)
-> (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> Dual1 d x -> d y)
-> h x y
-> SDualBi d x
-> SDualBi d y
vmapBi Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeG c s p d t n m x -> XEligibleConeG c s p d t n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeG c s p d t n m x -> XEligibleConeG c s p d t n m y
xecMapCov Variant2 'Covariant (Inv2 h) x y
-> Dual1 (XEligibleConeG c s p d t n m) x
-> Dual1 (XEligibleConeG c s p d t n m) y
Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeG c s (Dual p) d (Dual t) n m x
-> XEligibleConeG c s (Dual p) d (Dual t) n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeG c s p d t n m x -> XEligibleConeG c s p d t n m y
xecMapCov Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeG c s p d t n m x
-> Dual1 (XEligibleConeG c s p d t n m) y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeG c s p d t n m x
-> Dual1 (XEligibleConeG c s p d t n m) y
xecMapCnt Variant2 'Contravariant (Inv2 h) x y
-> Dual1 (XEligibleConeG c s p d t n m) x
-> XEligibleConeG c s p d t n m y
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeG c s (Dual p) d (Dual t) n m x
-> Dual1 (XEligibleConeG c s (Dual p) d (Dual t) n m) y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeG c s p d t n m x
-> Dual1 (XEligibleConeG c s p d t n m) y
xecMapCnt 

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

-- coXEligibleConeG -


-- | random variable for eligible cones over 'Op'.

coXEligibleConeG ::
  ( Multiplicative x
  , NaturalConicBi (Inv2 (HomDisjEmpty s Op)) c s p d t n m
  , s ~ Mlt
  )
  => XEligibleConeG c s p d t n m x
  -> XEligibleConeG c s (Dual p) d (Dual t) n m (Op x)
coXEligibleConeG :: forall x s
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x,
 NaturalConicBi (Inv2 (HomDisjEmpty s Op)) c s p d t n m,
 s ~ Mlt) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeG c s (Dual p) d (Dual t) n m (Op x)
coXEligibleConeG = Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
-> XEligibleConeG c s p d t n m x
-> Dual1 (XEligibleConeG c s p d t n m) (Op x)
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeG c s p d t n m x
-> Dual1 (XEligibleConeG c s p d t n m) y
xecMapCnt Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
forall x.
Multiplicative x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
toDualOpMlt

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

-- xEligibleConeGOrnt -


-- | random variable of eligible 'Cone's over 'Orientation'.

xecOrnt ::
  ( Conic c
  , Diagrammatic d
  )
  => X x -> LimesG c s p d t n m (Orientation x) -> X (Cone s p d t n m (Orientation x))
xecOrnt :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x
-> LimesG c s p d t n m (Orientation x)
-> X (Cone s p d t n m (Orientation x))
xecOrnt X x
xx (LimesProjective c s 'Projective d t n m (Orientation x)
u Cone s 'Projective d t n m (Orientation x) -> Orientation x
_)
  = case c s 'Projective d t n m (Orientation x)
-> Cone s 'Projective d t n m (Orientation x)
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone 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.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone c s 'Projective d t n m (Orientation x)
u of
  ConeProjective d t n m (Orientation x)
d Point (Orientation x)
_ FinList n (Orientation x)
_ -> X x
-> X (d t n m (Orientation x))
-> X (Cone Mlt 'Projective d t n m (Orientation x))
forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Mlt 'Projective d t n m (Orientation p))
xCnPrjOrnt X x
xx (d t n m (Orientation x) -> X (d t n m (Orientation x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return d t n m (Orientation x)
d)
  ConeKernel d ('Parallel 'LeftToRight) ('S N1) m (Orientation x)
d Orientation x
_       -> X x
-> X (d t n m (Orientation x))
-> X (Cone Dst 'Projective d t n m (Orientation x))
forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p, t ~ 'Parallel 'LeftToRight,
 n ~ 'S N1) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Dst 'Projective d t n m (Orientation p))
xCnPrjDstOrnt X x
xx (d t n m (Orientation x) -> X (d t n m (Orientation x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return d t n m (Orientation x)
d ('Parallel 'LeftToRight) ('S N1) m (Orientation x)
d)
xecOrnt X x
xx (LimesInjective c s 'Injective d t n m (Orientation x)
u Cone s 'Injective d t n m (Orientation x) -> Orientation x
_)
  = case c s 'Injective d t n m (Orientation x)
-> Cone s 'Injective d t n m (Orientation x)
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone 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.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone c s 'Injective d t n m (Orientation x)
u of
  ConeInjective d t n m (Orientation x)
d Point (Orientation x)
_ FinList n (Orientation x)
_ -> X x
-> X (d t n m (Orientation x))
-> X (Cone Mlt 'Injective d t n m (Orientation x))
forall p (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
(Entity p, Diagrammatic d) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Mlt 'Injective d t n m (Orientation p))
xCnInjOrnt X x
xx (d t n m (Orientation x) -> X (d t n m (Orientation x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return d t n m (Orientation x)
d)
  ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m (Orientation x)
d Orientation x
_    -> X x
-> X (d t n m (Orientation x))
-> X (Cone Dst 'Injective d t n m (Orientation x))
forall p (t :: DiagramType) (n :: N')
       (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
(Entity p, t ~ 'Parallel 'RightToLeft, n ~ 'S N1,
 Diagrammatic d) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Dst 'Injective d t n m (Orientation p))
xCnInjDstOrnt X x
xx (d t n m (Orientation x) -> X (d t n m (Orientation x))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return d t n m (Orientation x)
d ('Parallel 'RightToLeft) ('S N1) m (Orientation x)
d)
  
-- | random variable of eligible 'Cone's over 'Orientation'.

xEligibleConeGOrnt ::
  ( Conic c
  , Diagrammatic d
  )
  => X x -> XEligibleConeG c s p d t n m (Orientation x)
xEligibleConeGOrnt :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeG c s p d t n m (Orientation x)
xEligibleConeGOrnt = (LimesG c s p d t n m (Orientation x)
 -> X (Cone s p d t n m (Orientation x)))
-> XEligibleConeG c s p d t n m (Orientation x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(LimesG c s p d t n m x -> X (Cone s p d t n m x))
-> XEligibleConeG c s p d t n m x
XEligibleConeG ((LimesG c s p d t n m (Orientation x)
  -> X (Cone s p d t n m (Orientation x)))
 -> XEligibleConeG c s p d t n m (Orientation x))
-> (X x
    -> LimesG c s p d t n m (Orientation x)
    -> X (Cone s p d t n m (Orientation x)))
-> X x
-> XEligibleConeG c s p d t n m (Orientation x)
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
. X x
-> LimesG c s p d t n m (Orientation x)
-> X (Cone s p d t n m (Orientation x))
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x
-> LimesG c s p d t n m (Orientation x)
-> X (Cone s p d t n m (Orientation x))
xecOrnt

instance
  ( Conic c
  , Diagrammatic d
  , XStandard x
  )
  => XStandardEligibleConeG c s p d t n m (Orientation x) where
  xStandardEligibleConeG :: XEligibleConeG c s p d t n m (Orientation x)
xStandardEligibleConeG = X x -> XEligibleConeG c s p d t n m (Orientation x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeG c s p d t n m (Orientation x)
xEligibleConeGOrnt X x
forall x. XStandard x => X x
xStandard

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

-- xecDiscrete -


-- | random variable for eligible cones over 'Discrete' diagrammtic objects

xecDiscrete ::
  ( Multiplicative x
  , Conic c
  , Diagrammatic d
  )
  => XOrtOrientation x -> XEligibleConeG c s p d Discrete n m x
xecDiscrete :: forall x
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (n :: N') (m :: N').
(Multiplicative x, Conic c, Diagrammatic d) =>
XOrtOrientation x -> XEligibleConeG c s p d 'Discrete n m x
xecDiscrete XOrtOrientation x
xo = (LimesG c s p d 'Discrete n m x -> X (Cone s p d 'Discrete n m x))
-> XEligibleConeG c s p d 'Discrete 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.
(LimesG c s p d t n m x -> X (Cone s p d t n m x))
-> XEligibleConeG c s p d t n m x
XEligibleConeG ((LimesG c s p d 'Discrete n m x -> X (Cone s p d 'Discrete n m x))
 -> XEligibleConeG c s p d 'Discrete n m x)
-> (LimesG c s p d 'Discrete n m x
    -> X (Cone s p d 'Discrete n m x))
-> XEligibleConeG c s p d 'Discrete n m x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtOrientation x
-> LimesG c s p d 'Discrete n m x -> X (Cone s p d 'Discrete n m x)
forall x
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType) s
       (p :: Perspective) (n :: N') (m :: N').
(Multiplicative x, Conic c, Diagrammatic d, t ~ 'Discrete) =>
XOrtOrientation x
-> LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec XOrtOrientation x
xo where

  xArwsPrj :: XOrtOrientation x -> Point x -> FinList n (Point x) -> X (FinList n x)
  xArwsPrj :: forall x (n :: N').
XOrtOrientation x
-> Point x -> FinList n (Point x) -> X (FinList n x)
xArwsPrj XOrtOrientation x
xo Point x
s = FinList n (X x) -> X (FinList n x)
forall (n :: N') x. FinList n (X x) -> X (FinList n x)
xListF (FinList n (X x) -> X (FinList n x))
-> (FinList n (Point x) -> FinList n (X x))
-> FinList n (Point x)
-> X (FinList n x)
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
. (Point x -> X x) -> FinList n (Point x) -> FinList n (X x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\Point x
p -> XOrtOrientation x -> Orientation (Point x) -> X x
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation x
xo (Point x
sPoint x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:>Point x
p))

  xArwsInj :: XOrtOrientation x -> Point x -> FinList n (Point x) -> X (FinList n x)
  xArwsInj :: forall x (n :: N').
XOrtOrientation x
-> Point x -> FinList n (Point x) -> X (FinList n x)
xArwsInj XOrtOrientation x
xo Point x
e = FinList n (X x) -> X (FinList n x)
forall (n :: N') x. FinList n (X x) -> X (FinList n x)
xListF (FinList n (X x) -> X (FinList n x))
-> (FinList n (Point x) -> FinList n (X x))
-> FinList n (Point x)
-> X (FinList n x)
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
. (Point x -> X x) -> FinList n (Point x) -> FinList n (X x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\Point x
p -> XOrtOrientation x -> Orientation (Point x) -> X x
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation x
xo (Point x
pPoint x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:>Point x
e))
  
  xec ::
    ( Multiplicative x
    , Conic c
    , Diagrammatic d
    , t ~ Discrete
    )
    => XOrtOrientation x -> LimesG c s p d t n m x -> X (Cone s p d t n m x)
  xec :: forall x
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType) s
       (p :: Perspective) (n :: N') (m :: N').
(Multiplicative x, Conic c, Diagrammatic d, t ~ 'Discrete) =>
XOrtOrientation x
-> LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec XOrtOrientation x
xo (LimesProjective c s 'Projective d t n m x
u Cone s 'Projective d t n m x -> x
_) = do
    Point x
t  <- XOrtOrientation x -> X (Point x)
forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint XOrtOrientation x
xo
    case c s 'Projective d t n m x -> Cone s 'Projective d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone 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.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone c s 'Projective d t n m x
u of
      ConeProjective d t n m x
d Point x
_ FinList n x
_ -> XOrtOrientation x
-> Point x -> FinList n (Point x) -> X (FinList n x)
forall x (n :: N').
XOrtOrientation x
-> Point x -> FinList n (Point x) -> X (FinList n x)
xArwsPrj XOrtOrientation x
xo Point x
t (Diagram t n m x -> FinList n (Point x)
Diagram 'Discrete n m x -> FinList n (Point x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints (Diagram t n m x -> FinList n (Point x))
-> Diagram t n m x -> FinList n (Point x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d t n m x -> Diagram t n m x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d t n m x
d) X (FinList n x)
-> (FinList n x -> X (Cone s p d t n m x))
-> X (Cone s p d t n m x)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Cone Mlt 'Projective d 'Discrete n m x
-> X (Cone Mlt 'Projective d 'Discrete n m x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cone Mlt 'Projective d 'Discrete n m x
 -> X (Cone Mlt 'Projective d 'Discrete n m x))
-> (FinList n x -> Cone Mlt 'Projective d 'Discrete n m x)
-> FinList n x
-> X (Cone Mlt 'Projective d 'Discrete n m x)
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
. d t n m x
-> Point x -> FinList n x -> Cone Mlt 'Projective d t n m x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective d t n m x
d Point x
t

  xec XOrtOrientation x
xo (LimesInjective c s 'Injective d t n m x
u Cone s 'Injective d t n m x -> x
_) = do
    Point x
t <- XOrtOrientation x -> X (Point x)
forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint XOrtOrientation x
xo
    case c s 'Injective d t n m x -> Cone s 'Injective d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone 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.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone c s 'Injective d t n m x
u of
      ConeInjective d t n m x
d Point x
_ FinList n x
_ -> XOrtOrientation x
-> Point x -> FinList n (Point x) -> X (FinList n x)
forall x (n :: N').
XOrtOrientation x
-> Point x -> FinList n (Point x) -> X (FinList n x)
xArwsInj XOrtOrientation x
xo Point x
t (Diagram t n m x -> FinList n (Point x)
Diagram 'Discrete n m x -> FinList n (Point x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints (Diagram t n m x -> FinList n (Point x))
-> Diagram t n m x -> FinList n (Point x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d t n m x -> Diagram t n m x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d t n m x
d) X (FinList n x)
-> (FinList n x -> X (Cone s p d t n m x))
-> X (Cone s p d t n m x)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Cone Mlt 'Injective d 'Discrete n m x
-> X (Cone Mlt 'Injective d 'Discrete n m x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cone Mlt 'Injective d 'Discrete n m x
 -> X (Cone Mlt 'Injective d 'Discrete n m x))
-> (FinList n x -> Cone Mlt 'Injective d 'Discrete n m x)
-> FinList n x
-> X (Cone Mlt 'Injective d 'Discrete n m x)
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
. d t n m x
-> Point x -> FinList n x -> Cone Mlt 'Injective d t n m x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective d t n m a
ConeInjective d t n m x
d Point x
t

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

-- XEligibleConeFactorG -


-- | random variable for eligible cones together with a eligible factor for a given limes.

data XEligibleConeFactorG c s p d t n m x
  = XEligibleConeFactorG (LimesG c s p d t n m x -> X (Cone s p d t n m x, x))

type instance Dual1 (XEligibleConeFactorG c s p d t n m)
  = XEligibleConeFactorG c s (Dual p) d (Dual t) n m

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

-- xecf -


-- | random variable of eligible cone factors.

xecf :: XEligibleConeFactorG c s p d t n m x -> LimesG c s p d t n m x -> X (Cone s p d t n m x,x)
xecf :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
XEligibleConeFactorG c s p d t n m x
-> LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xecf (XEligibleConeFactorG LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xcx) = LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xcx


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

-- xecfMapCov -


-- | covariant mapping of 'XEligibleConeFactorG'

xecfMapCov :: NaturalConicBi (Inv2 h) c s p d t n m
  => Variant2 Covariant (Inv2 h) x y
  -> XEligibleConeFactorG c s p d t n m x
  -> XEligibleConeFactorG c s p d t n m y
xecfMapCov :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m y
xecfMapCov (Covariant2 Inv2 h x y
i) (XEligibleConeFactorG LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xecf) = (LimesG c s p d t n m y -> X (Cone s p d t n m y, y))
-> XEligibleConeFactorG c s p d t n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(LimesG c s p d t n m x -> X (Cone s p d t n m x, x))
-> XEligibleConeFactorG c s p d t n m x
XEligibleConeFactorG LimesG c s p d t n m y -> X (Cone s p d t n m y, y)
xecf' where
  xecf' :: LimesG c s p d t n m y -> X (Cone s p d t n m y, y)
xecf' LimesG c s p d t n m y
l' = X (Cone s p d t n m y, y)
xcf' where
    SDualBi (Right1 LimesG c s p d t n m x
l) = Inv2 h y x
-> SDualBi (LimesG c s p d t n m) y
-> SDualBi (LimesG c s p d t n m) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i) (Either1 (Dual1 (LimesG c s p d t n m)) (LimesG c s p d t n m) y
-> SDualBi (LimesG c s p d t n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s p d t n m y
-> Either1
     (LimesG c s (Dual p) d (Dual t) n m) (LimesG c s p d t n m) y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LimesG c s p d t n m y
l'))

    xcf' :: X (Cone s p d t n m y, y)
xcf' = do
      (Cone s p d t n m x
c,x
f) <- LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xecf LimesG c s p d t n m x
l
      let SDualBi (Right1 (ConeG Cone s p d t n m y
c')) = Inv2 h x y
-> SDualBi (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 h x y
i (Either1 (Dual1 (ConeG Cone s p d t n m)) (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s p d t n m x
-> Either1
     (ConeG Cone s (Dual p) d (Dual t) n m) (ConeG Cone s p d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Cone s p d t n m x -> ConeG Cone 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG Cone s p d t n m x
c))) in (Cone s p d t n m y, y) -> X (Cone s p d t n m y, y)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cone s p d t n m y
c',Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf Inv2 h x y
i x
f)

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

-- xecfMapCnt -


-- | contravariant mapping of 'XEligibleConeFactorG'

xecfMapCnt :: NaturalConicBi (Inv2 h) c s p d t n m
  => Variant2 Contravariant (Inv2 h) x y
  -> XEligibleConeFactorG c s p d t n m x
  -> XEligibleConeFactorG c s (Dual p) d (Dual t) n m y
xecfMapCnt :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m y
xecfMapCnt (Contravariant2 Inv2 h x y
i) (XEligibleConeFactorG LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xecf) = (LimesG c s (Dual p) d (Dual t) n m y
 -> X (Cone s (Dual p) d (Dual t) n m y, y))
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(LimesG c s p d t n m x -> X (Cone s p d t n m x, x))
-> XEligibleConeFactorG c s p d t n m x
XEligibleConeFactorG LimesG c s (Dual p) d (Dual t) n m y
-> X (Cone s (Dual p) d (Dual t) n m y, y)
xecf' where
  xecf' :: LimesG c s (Dual p) d (Dual t) n m y
-> X (Cone s (Dual p) d (Dual t) n m y, y)
xecf' LimesG c s (Dual p) d (Dual t) n m y
l' = X (Cone s (Dual p) d (Dual t) n m y, y)
xcf' where
    SDualBi (Left1 Dual1 (LimesG c s (Dual p) d (Dual t) n m) x
l) = Inv2 h y x
-> SDualBi (LimesG c s (Dual p) d (Dual t) n m) y
-> SDualBi (LimesG c s (Dual p) d (Dual t) n m) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i) (Either1
  (Dual1 (LimesG c s (Dual p) d (Dual t) n m))
  (LimesG c s (Dual p) d (Dual t) n m)
  y
-> SDualBi (LimesG c s (Dual p) d (Dual t) n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s (Dual p) d (Dual t) n m y
-> Either1
     (LimesG c s (Dual (Dual p)) d (Dual (Dual t)) n m)
     (LimesG c s (Dual p) d (Dual t) n m)
     y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 LimesG c s (Dual p) d (Dual t) n m y
l'))

    xcf' :: X (Cone s (Dual p) d (Dual t) n m y, y)
xcf' = do
      (Cone s p d t n m x
c,x
f) <- LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xecf Dual1 (LimesG c s (Dual p) d (Dual t) n m) x
LimesG c s p d t n m x
l
      let SDualBi (Left1 (ConeG Cone s (Dual p) d (Dual t) n m y
cOp)) = Inv2 h x y
-> SDualBi (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) y
forall x y.
Inv2 h x y
-> SDualBi (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG Inv2 h x y
i (Either1 (Dual1 (ConeG Cone s p d t n m)) (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s p d t n m x
-> Either1
     (ConeG Cone s (Dual p) d (Dual t) n m) (ConeG Cone s p d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Cone s p d t n m x -> ConeG Cone 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG Cone s p d t n m x
c))) in (Cone s (Dual p) d (Dual t) n m y, y)
-> X (Cone s (Dual p) d (Dual t) n m y, y)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cone s (Dual p) d (Dual t) n m y
cOp,Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf Inv2 h x y
i x
f)

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

-- xecfMapS -


-- | mapping of 'XEligibleConeFactorG'

xecfMapS :: NaturalConicBi (Inv2 h) c s p d t n m
  => Inv2 h x y
  -> SDualBi (XEligibleConeFactorG c s p d t n m) x
  -> SDualBi (XEligibleConeFactorG c s p d t n m) y
xecfMapS :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Inv2 h x y
-> SDualBi (XEligibleConeFactorG c s p d t n m) x
-> SDualBi (XEligibleConeFactorG c s p d t n m) y
xecfMapS = (Variant2 'Covariant (Inv2 h) x y
 -> XEligibleConeFactorG c s p d t n m x
 -> XEligibleConeFactorG c s p d t n m y)
-> (Variant2 'Covariant (Inv2 h) x y
    -> Dual1 (XEligibleConeFactorG c s p d t n m) x
    -> Dual1 (XEligibleConeFactorG c s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> XEligibleConeFactorG c s p d t n m x
    -> Dual1 (XEligibleConeFactorG c s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> Dual1 (XEligibleConeFactorG c s p d t n m) x
    -> XEligibleConeFactorG c s p d t n m y)
-> Inv2 h x y
-> SDualBi (XEligibleConeFactorG c s p d t n m) x
-> SDualBi (XEligibleConeFactorG c s p d t n m) y
forall (h :: * -> * -> *) x y (d :: * -> *).
Disjunctive2 h =>
(Variant2 'Covariant h x y -> d x -> d y)
-> (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> Dual1 d x -> d y)
-> h x y
-> SDualBi d x
-> SDualBi d y
vmapBi Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m y
xecfMapCov Variant2 'Covariant (Inv2 h) x y
-> Dual1 (XEligibleConeFactorG c s p d t n m) x
-> Dual1 (XEligibleConeFactorG c s p d t n m) y
Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m y
xecfMapCov Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> Dual1 (XEligibleConeFactorG c s p d t n m) y
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m y
xecfMapCnt Variant2 'Contravariant (Inv2 h) x y
-> Dual1 (XEligibleConeFactorG c s p d t n m) x
-> XEligibleConeFactorG c s p d t n m y
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m x
-> XEligibleConeFactorG c s (Dual (Dual p)) d (Dual (Dual t)) n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m y
xecfMapCnt 

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

-- coXEligibleConeFactorG -


-- | the co-object of 'XEligibleConeFactorG' accordint to 'Op'.

coXEligibleConeFactorG ::
  ( Multiplicative x
  , NaturalConicBi (Inv2 (HomDisjEmpty s Op)) c s p d t n m
  , s ~ Mlt
  )
  => XEligibleConeFactorG c s p d t n m x
  -> XEligibleConeFactorG c s (Dual p) d (Dual t) n m (Op x)
coXEligibleConeFactorG :: forall x s
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x,
 NaturalConicBi (Inv2 (HomDisjEmpty s Op)) c s p d t n m,
 s ~ Mlt) =>
XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m (Op x)
coXEligibleConeFactorG = Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m (Op x)
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m y
xecfMapCnt Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
forall x.
Multiplicative x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
toDualOpMlt

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

-- xEligibleConeFactorGOrnt -


-- | gets a eligible factor for the given 'LimesG' and 'Cone'.

elgFactorOrnt :: Conic c
  => LimesG c s p d t n m (Orientation x)
  -> Cone s p d t n m (Orientation x) -> Orientation x
elgFactorOrnt :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
LimesG c s p d t n m (Orientation x)
-> Cone s p d t n m (Orientation x) -> Orientation x
elgFactorOrnt LimesG c s p d t n m (Orientation x)
l Cone s p d t n m (Orientation x)
c = case c s p d t n m (Orientation x) -> Cone s p d t n m (Orientation x)
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone 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.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone (c s p d t n m (Orientation x) -> Cone s p d t n m (Orientation x))
-> c s p d t n m (Orientation x)
-> Cone s p d t n m (Orientation x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG c s p d t n m (Orientation x)
-> c s p d t n m (Orientation x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG c s p d t n m (Orientation x)
l of
  ConeProjective d t n m (Orientation x)
_ Point (Orientation x)
t FinList n (Orientation x)
_ -> Cone s p d t n m (Orientation x) -> Point (Orientation x)
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone s p d t n m (Orientation x)
c x -> x -> Orientation x
forall p. p -> p -> Orientation p
:> x
Point (Orientation x)
t  
  ConeInjective d t n m (Orientation x)
_ Point (Orientation x)
t FinList n (Orientation x)
_  -> x
Point (Orientation x)
t x -> x -> Orientation x
forall p. p -> p -> Orientation p
:> Cone s p d t n m (Orientation x) -> Point (Orientation x)
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone s p d t n m (Orientation x)
c
  ConeKernel d ('Parallel 'LeftToRight) ('S N1) m (Orientation x)
_ Orientation x
k       -> Cone s p d t n m (Orientation x) -> Point (Orientation x)
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone s p d t n m (Orientation x)
c x -> x -> Orientation x
forall p. p -> p -> Orientation p
:> Orientation x -> Point (Orientation x)
forall q. Oriented q => q -> Point q
start Orientation x
k
  ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m (Orientation x)
_ Orientation x
k     -> Orientation x -> Point (Orientation x)
forall q. Oriented q => q -> Point q
end Orientation x
k x -> x -> Orientation x
forall p. p -> p -> Orientation p
:> Cone s p d t n m (Orientation x) -> Point (Orientation x)
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone s p d t n m (Orientation x)
c

-- | random variable of eligible factors over 'Orientation'.

xEligibleConeFactorGOrnt ::
  ( Conic c
  , Diagrammatic d
  )
  => X x -> XEligibleConeFactorG c s p d t n m (Orientation x)
xEligibleConeFactorGOrnt :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeFactorG c s p d t n m (Orientation x)
xEligibleConeFactorGOrnt X x
xx = (LimesG c s p d t n m (Orientation x)
 -> X (Cone s p d t n m (Orientation x), Orientation x))
-> XEligibleConeFactorG c s p d t n m (Orientation x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(LimesG c s p d t n m x -> X (Cone s p d t n m x, x))
-> XEligibleConeFactorG c s p d t n m x
XEligibleConeFactorG LimesG c s p d t n m (Orientation x)
-> X (Cone s p d t n m (Orientation x), Orientation x)
xef where
  XEligibleConeG LimesG c s p d t n m (Orientation x)
-> X (Cone s p d t n m (Orientation x))
xec = X x -> XEligibleConeG c s p d t n m (Orientation x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeG c s p d t n m (Orientation x)
xEligibleConeGOrnt X x
xx
  xef :: LimesG c s p d t n m (Orientation x)
-> X (Cone s p d t n m (Orientation x), Orientation x)
xef LimesG c s p d t n m (Orientation x)
l = (Cone s p d t n m (Orientation x)
 -> (Cone s p d t n m (Orientation x), Orientation x))
-> X (Cone s p d t n m (Orientation x))
-> X (Cone s p d t n m (Orientation x), Orientation x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\Cone s p d t n m (Orientation x)
c -> (Cone s p d t n m (Orientation x)
c,LimesG c s p d t n m (Orientation x)
-> Cone s p d t n m (Orientation x) -> Orientation x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
LimesG c s p d t n m (Orientation x)
-> Cone s p d t n m (Orientation x) -> Orientation x
elgFactorOrnt LimesG c s p d t n m (Orientation x)
l Cone s p d t n m (Orientation x)
c)) (X (Cone s p d t n m (Orientation x))
 -> X (Cone s p d t n m (Orientation x), Orientation x))
-> X (Cone s p d t n m (Orientation x))
-> X (Cone s p d t n m (Orientation x), Orientation x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG c s p d t n m (Orientation x)
-> X (Cone s p d t n m (Orientation x))
xec LimesG c s p d t n m (Orientation x)
l

instance
  ( Conic c
  , Diagrammatic d
  , XStandard x
  )
  => XStandardEligibleConeFactorG c s p d t n m (Orientation x) where
  xStandardEligibleConeFactorG :: XEligibleConeFactorG c s p d t n m (Orientation x)
xStandardEligibleConeFactorG = X x -> XEligibleConeFactorG c s p d t n m (Orientation x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeFactorG c s p d t n m (Orientation x)
xEligibleConeFactorGOrnt X x
forall x. XStandard x => X x
xStandard

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

-- xecfOrtSite -


xecfPrjOrtSiteTo :: Conic c
  => XOrtSite To x -> LimesG c s Projective d t n m x -> X (Cone s Projective d t n m x, x)
xecfPrjOrtSiteTo :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Conic c =>
XOrtSite 'To x
-> LimesG c s 'Projective d t n m x
-> X (Cone s 'Projective d t n m x, x)
xecfPrjOrtSiteTo (XEnd X (Point x)
_ Point x -> X x
xe) LimesG c s 'Projective d t n m x
l = (x -> (Cone s 'Projective d t n m x, x))
-> X x -> X (Cone s 'Projective d t n m x, x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Cone s 'Projective d t n m x
-> x -> (Cone s 'Projective d t n m x, x)
forall s (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Cone s 'Projective d t n m x
-> x -> (Cone s 'Projective d t n m x, x)
cn Cone s 'Projective d t n m x
u) (X x -> X (Cone s 'Projective d t n m x, x))
-> X x -> X (Cone s 'Projective d t n m x, x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Point x -> X x
xe (Point x -> X x) -> Point x -> X x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Cone s 'Projective d t n m x -> Point x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone s 'Projective d t n m x
u where
  u :: Cone s 'Projective d t n m x
u = c s 'Projective d t n m x -> Cone s 'Projective d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone 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.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone (c s 'Projective d t n m x -> Cone s 'Projective d t n m x)
-> c s 'Projective d t n m x -> Cone s 'Projective d t n m x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG c s 'Projective d t n m x -> c s 'Projective 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.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG c s 'Projective d t n m x
l
    
  cn :: Cone s Projective d t n m x -> x -> (Cone s Projective d t n m x, x)
  cn :: forall s (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Cone s 'Projective d t n m x
-> x -> (Cone s 'Projective d t n m x, x)
cn (ConeProjective d t n m x
d Point x
_ FinList n x
as) x
f = (d t n m x
-> Point x -> FinList n x -> Cone Mlt 'Projective d t n m x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective d t n m x
d (x -> Point x
forall q. Oriented q => q -> Point q
start x
f) ((x -> x) -> FinList n x -> FinList n x
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (x -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
f) FinList n x
as), x
f)
  cn (ConeKernel d ('Parallel 'LeftToRight) ('S N1) m x
d x
a) x
f        = (d ('Parallel 'LeftToRight) ('S N1) m x
-> x -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel d ('Parallel 'LeftToRight) ('S N1) m x
d (x
ax -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
f),x
f)     

xecfInjOrtSiteFrom :: Conic c
  => XOrtSite From x -> LimesG c s Injective d t n m x -> X (Cone s Injective d t n m x, x)
xecfInjOrtSiteFrom :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Conic c =>
XOrtSite 'From x
-> LimesG c s 'Injective d t n m x
-> X (Cone s 'Injective d t n m x, x)
xecfInjOrtSiteFrom (XStart X (Point x)
_ Point x -> X x
xs) LimesG c s 'Injective d t n m x
l = (x -> (Cone s 'Injective d t n m x, x))
-> X x -> X (Cone s 'Injective d t n m x, x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Cone s 'Injective d t n m x
-> x -> (Cone s 'Injective d t n m x, x)
forall s (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Cone s 'Injective d t n m x
-> x -> (Cone s 'Injective d t n m x, x)
cn Cone s 'Injective d t n m x
u) (X x -> X (Cone s 'Injective d t n m x, x))
-> X x -> X (Cone s 'Injective d t n m x, x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Point x -> X x
xs (Point x -> X x) -> Point x -> X x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Cone s 'Injective d t n m x -> Point x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone s 'Injective d t n m x
u where
  u :: Cone s 'Injective d t n m x
u = c s 'Injective d t n m x -> Cone s 'Injective d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone 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.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone (c s 'Injective d t n m x -> Cone s 'Injective d t n m x)
-> c s 'Injective d t n m x -> Cone s 'Injective d t n m x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG c s 'Injective d t n m x -> c s 'Injective 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.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG c s 'Injective d t n m x
l
    
  cn :: Cone s Injective d t n m x -> x -> (Cone s Injective d t n m x, x)
  cn :: forall s (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Cone s 'Injective d t n m x
-> x -> (Cone s 'Injective d t n m x, x)
cn (ConeInjective d t n m x
d Point x
_ FinList n x
as) x
f = (d t n m x
-> Point x -> FinList n x -> Cone Mlt 'Injective d t n m x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective d t n m a
ConeInjective d t n m x
d (x -> Point x
forall q. Oriented q => q -> Point q
end x
f) ((x -> x) -> FinList n x -> FinList n x
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (x
fx -> x -> x
forall c. Multiplicative c => c -> c -> c
*) FinList n x
as),x
f)
  cn (ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m x
d x
a) x
f     = (d ('Parallel 'RightToLeft) ('S N1) m x
-> x -> Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) m x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'RightToLeft) ('S N1) m a
-> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) m a
ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m x
d (x
fx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
a),x
f)

-- | the random variable 'XEligibleConeFactorG' given be 'XOrtSite'.

xecfOrtSite :: Conic c
  => XOrtSite r x -> XEligibleConeFactorG c s (ToPerspective r) d t n m x
xecfOrtSite :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (r :: Site) x s (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Conic c =>
XOrtSite r x
-> XEligibleConeFactorG c s (ToPerspective r) d t n m x
xecfOrtSite xe :: XOrtSite r x
xe@(XEnd X (Point x)
_ Point x -> X x
_)   = (LimesG c s 'Projective d t n m x
 -> X (Cone s 'Projective d t n m x, x))
-> XEligibleConeFactorG c s 'Projective 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.
(LimesG c s p d t n m x -> X (Cone s p d t n m x, x))
-> XEligibleConeFactorG c s p d t n m x
XEligibleConeFactorG (XOrtSite 'To x
-> LimesG c s 'Projective d t n m x
-> X (Cone s 'Projective d t n m x, x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Conic c =>
XOrtSite 'To x
-> LimesG c s 'Projective d t n m x
-> X (Cone s 'Projective d t n m x, x)
xecfPrjOrtSiteTo XOrtSite r x
XOrtSite 'To x
xe)
xecfOrtSite xs :: XOrtSite r x
xs@(XStart X (Point x)
_ Point x -> X x
_) = (LimesG c s 'Injective d t n m x
 -> X (Cone s 'Injective d t n m x, x))
-> XEligibleConeFactorG c s 'Injective 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.
(LimesG c s p d t n m x -> X (Cone s p d t n m x, x))
-> XEligibleConeFactorG c s p d t n m x
XEligibleConeFactorG (XOrtSite 'From x
-> LimesG c s 'Injective d t n m x
-> X (Cone s 'Injective d t n m x, x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N').
Conic c =>
XOrtSite 'From x
-> LimesG c s 'Injective d t n m x
-> X (Cone s 'Injective d t n m x, x)
xecfInjOrtSiteFrom XOrtSite r x
XOrtSite 'From x
xs)

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

-- xecfEligibleCone -


-- | the induced random variable for eligible cones.

xecfEligibleCone :: XEligibleConeFactorG c s p d t n m x -> XEligibleConeG c s p d t n m x
xecfEligibleCone :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
XEligibleConeFactorG c s p d t n m x
-> XEligibleConeG c s p d t n m x
xecfEligibleCone (XEligibleConeFactorG LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xecf) = (LimesG c s p d t n m x -> X (Cone s p d t n m x))
-> 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.
(LimesG c s p d t n m x -> X (Cone s p d t n m x))
-> XEligibleConeG c s p d t n m x
XEligibleConeG (((Cone s p d t n m x, x) -> Cone s p d t n m x)
-> X (Cone s p d t n m x, x) -> X (Cone s p d t n m x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Cone s p d t n m x, x) -> Cone s p d t n m x
forall a b. (a, b) -> a
fst (X (Cone s p d t n m x, x) -> X (Cone s p d t n m x))
-> (LimesG c s p d t n m x -> X (Cone s p d t n m x, x))
-> LimesG c s p d t n m x
-> X (Cone s p d t n m x)
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
. LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xecf)

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

-- XStandardEligibleConeFactorG -


-- | standard random variable for eligible cone factors.

class XStandardEligibleConeFactorG c s p d t n m x where
  xStandardEligibleConeFactorG :: XEligibleConeFactorG c s p d t n m x
  
--------------------------------------------------------------------------------

-- XStandardEligibleCone -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeFactorG Cone s p Diagram t n m x => XStandardEligibleConeFactor s p t n m x

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

-- XStandardEligibleConeG -


-- | standard random variable for eligible cones.

class XStandardEligibleConeG c s p d t n m x where
  xStandardEligibleConeG :: XEligibleConeG c s p d t n m x

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

-- XStandardEligibleCone -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeG Cone s p Diagram t n m x
  => XStandardEligibleCone s p t n m x

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

-- prpLimesFactorExist -


-- | validity according the existence of a eligible factor for a given 'LimesG'

-- and 'Cone'.

prpLimesFactorExist ::
  ( Conic c
  , Diagrammatic d
  , Show (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
  -> LimesG c s p d t n m x -> Statement
prpLimesFactorExist :: 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),
 Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> LimesG c s p d t n m x -> Statement
prpLimesFactorExist (XEligibleConeG LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec) LimesG c s p d t n m x
l = String -> Label
Prp String
"LimesFactorExists" Label -> Statement -> Statement
:<=>:
  X (Cone s p d t n m x)
-> (Cone s p d t n m x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (LimesG c s p d t n m x -> X (Cone s p d t n m x)
xec LimesG c s p d t n m x
l)
    (\Cone s p d t n m x
c -> LimesG c s p d t n m x -> Cone s p d t n m x -> Bool
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x s (p :: Perspective).
(Conic c, Eq (d t n m x)) =>
LimesG c s p d t n m x -> Cone s p d t n m x -> Bool
eligibleCone LimesG c s p d t n m x
l Cone s p d t n m x
c Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"c"String -> String -> Parameter
:=Cone s p d t n m x -> String
forall a. Show a => a -> String
show Cone s p d t n m x
c]
           -- actually the random variable should produce eligible cones!!

           -- but the preconditions tests also the validity of xec

       Statement -> Statement -> Statement
:=> let f :: x
f = LimesG c s p d t n m x -> Cone s p d t n m x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalFactor LimesG c s p d t n m x
l Cone s p d t n m x
c
            in [Statement] -> Statement
And [ x -> Statement
forall a. Validable a => a -> Statement
valid x
f
                   , LimesG c s p d t n m x -> Cone s p d t n m x -> x -> Bool
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) =>
LimesG c s p d t n m x -> Cone s p d t n m x -> x -> Bool
eligibleFactor LimesG c s p d t n m x
l Cone s p d t n m x
c x
f Bool -> Message -> Statement
:?> [Parameter] -> Message
Params
                       [ String
"u"String -> String -> Parameter
:= c s p d t n m x -> String
forall a. Show a => a -> String
show (LimesG c s p d t n m x -> 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.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG c s p d t n m x
l)
                       , String
"c"String -> String -> Parameter
:=Cone s p d t n m x -> String
forall a. Show a => a -> String
show Cone s p d t n m x
c
                       , String
"f"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
f
                       ]
                   ]
    ) 

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

-- prpLimesFactorUnique -


-- | validity according to the uniqueness of a eligible factor for a given 'LimesG'

-- and 'Cone'.

prpLimesFactorUnique ::
  ( Conic c, Diagrammatic d
  , Entity (d t n m x)
  , Entity x
  )
  => XEligibleConeFactorG c s p d t n m x
  -> LimesG c s p d t n m x -> Statement
prpLimesFactorUnique :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x s (p :: Perspective).
(Conic c, Diagrammatic d, Entity (d t n m x), Entity x) =>
XEligibleConeFactorG c s p d t n m x
-> LimesG c s p d t n m x -> Statement
prpLimesFactorUnique (XEligibleConeFactorG LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xef) LimesG c s p d t n m x
l = String -> Label
Prp String
"LimesFactorUnique" Label -> Statement -> Statement
:<=>:
  X (Cone s p d t n m x, x)
-> ((Cone s p d t n m x, x) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (LimesG c s p d t n m x -> X (Cone s p d t n m x, x)
xef LimesG c s p d t n m x
l)
    (\(Cone s p d t n m x
c,x
x) -> [Statement] -> Statement
And [ LimesG c s p d t n m x -> Cone s p d t n m x -> Bool
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x s (p :: Perspective).
(Conic c, Eq (d t n m x)) =>
LimesG c s p d t n m x -> Cone s p d t n m x -> Bool
eligibleCone LimesG c s p d t n m x
l Cone s p d t n m x
c Bool -> Message -> Statement
:?> [Parameter] -> Message
Params []
                   , LimesG c s p d t n m x -> Cone s p d t n m x -> x -> Bool
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) =>
LimesG c s p d t n m x -> Cone s p d t n m x -> x -> Bool
eligibleFactor LimesG c s p d t n m x
l Cone s p d t n m x
c x
x Bool -> Message -> Statement
:?> [Parameter] -> Message
Params []
                   ]
           Statement -> Statement -> Statement
:=> let f :: x
f = LimesG c s p d t n m x -> Cone s p d t n m x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalFactor LimesG c s p d t n m x
l Cone s p d t n m x
c
                in (x
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
f) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"c"String -> String -> Parameter
:=Cone s p d t n m x -> String
forall a. Show a => a -> String
show Cone s p d t n m x
c, String
"x'"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x, String
"f"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
f]
    )

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

-- prpLimes -


-- | validity according to 'LimesG'.

prpLimes ::
  ( 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 :: 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
l = String -> Label
Prp String
"Limes" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ c s p d t n m x -> Statement
forall a. Validable a => a -> Statement
valid (LimesG c s p d t n m x -> 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.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG c s p d t n m x
l)
      , XEligibleConeG 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),
 Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> LimesG c s p d t n m x -> Statement
prpLimesFactorExist XEligibleConeG c s p d t n m x
xec LimesG c s p d t n m x
l
      , 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' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x s (p :: Perspective).
(Conic c, Diagrammatic d, Entity (d t n m x), Entity x) =>
XEligibleConeFactorG c s p d t n m x
-> LimesG c s p d t n m x -> Statement
prpLimesFactorUnique XEligibleConeFactorG c s p d t n m x
xef LimesG c s p d t n m x
l
      ]

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

-- Validable -


instance
  ( Conic c, Diagrammatic d
  , XStandardEligibleConeG c s p d t n m x
  , XStandardEligibleConeFactorG c s p 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 (LimesG c s p d t n m x) where
  valid :: LimesG 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
-> 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
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