{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Exact.Deviation

-- Description : measuring the deviation of exactness.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- measuring the deviation exactness.

module OAlg.Limes.Exact.Deviation
  (
    -- * Deviation

    deviation, deviations, Deviation
  , dvZeroPoint, dvZeroPoint'

    -- * Deviation Hom

  , deviationHom, DeviationHom
  
    -- * Variance

  , variance, VarianceG(..), Variance
  , isExact, isExactVariance

  , vrcConsZeroHom

  , vrcSite
  , vrcHead, vrcTail

  , NaturalKernelCokernel
  , EntityDiagrammatic
  , ObjectKernelCokernel

    -- ** Duality

  , vrcMapS, vrcMapCov, vrcMapCnt


    -- * Variance Hom

  , varianceHom, VarianceGHom(..), VarianceHom

  , vrcHomSite
  , vrcHomConsZeroHom

    -- ** Duality

  , vrcHomMapS, vrcHomMapCov, vrcHomMapCnt

    -- * Proposition


  , prpVarianceG
  , prpVarianceGHom
  , prpDeviationOrntSymbol

  ) where

import Data.Typeable
import Data.List as L ((++))

import OAlg.Prelude

import OAlg.Category.SDuality

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

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Distributive

import OAlg.Entity.Diagram
import OAlg.Entity.Natural
import OAlg.Entity.FinList as F

import OAlg.Hom.Definition
import OAlg.Hom.Distributive

import OAlg.Limes.Definition
import OAlg.Limes.Cone
import OAlg.Limes.Limits
import OAlg.Limes.KernelsAndCokernels

import OAlg.Limes.Exact.ConsecutiveZero
import OAlg.Limes.Exact.ZeroPoint

import OAlg.Data.Symbol

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

-- VarianceG -


-- | measuring the 'deviation' of a consecutive zero chain of being exact accordind to the given

-- generalized kernels and cokernels. The exactness is given by  'deviations'.

--

-- __Properties__ Let @'VarianceG' c vs@ be in @t'VarianceG' __t k c d n x__@ for a 'Distributive'

-- structure @__x__@, then

-- for all @(ker 0, coker 0), (ker 1, coker 1) .. (ker i,coker i) .. (ker n,coker n)@ in @vs@,

-- and @d 0, d 1 .. d i, d (i+1) .. d (n+1)@ in @'cnzArrows' t@ holds:

--

-- (1) If @t@ matches @'ConsecutiveZero' ('DiagramChainTo' _ _)@ then holds (see diagram below):

--

--     (1) @ker i@ is a kernel of @d i@.

--

--     (2) @coker i@ is a cokernel of @d' (i+1)@, where @d' (i+1)@ is the universal factor given

--     by @ker i@ and @d (i+1)@.

--

-- @

--                d i          d (i+1)               

-- c :  ... a <------------ b <------------ c ...

--                          ^              || 

--                          |              || 

--                          | ker i        || one

--                          |              || 

--                          ^              || 

--          a'<<----------- b'<------------ c 

--               coker i        d' (i+1)

-- @

--

-- (2) If @t@ matches @'ConsecutiveZero' ('DiagramChainFrom' _ _)@ then holds (see diagram below):

--

--     (1) @coker i@ is a cokernel of @d i@.

--

--     (2) @ker i@ is a kernel of @d' (i+1)@, where @d' (i+1)@ is the universal factor given

--     by @coker i@ and @d (i+1)@.

--

-- @

--                d i          d (i+1)               

-- c :  ... a ------------> b ------------> c ...

--                          v              || 

--                          |              || 

--                          | coker i      || one

--                          v              || 

--                          v              || 

--          a'>>----------> b'------------> c 

--               ker i          d' (i+1)

-- @

data VarianceG t k c d n x where
  VarianceG
    :: ConsecutiveZero t n x
    -> FinList (n+1) (KernelG k d N1 x, CokernelG c d N1 x)
    -> VarianceG t k c d n x

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

-- Variance -


-- | the variance according to 'Kernels' and 'Cokernels'

type Variance t = VarianceG t Cone Cone Diagram
--------------------------------------------------------------------------------

-- vrcSite -


-- | proof that the site is either 'From' or 'To'.

vrcSite :: VarianceG t k c d n x -> Either (t :~: From) (t :~: To)
vrcSite :: forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceG t k c d n x -> Either (t :~: 'From) (t :~: 'To)
vrcSite (VarianceG ConsecutiveZero t n x
c FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
_) = ConsecutiveZero t n x -> Either (t :~: 'From) (t :~: 'To)
forall (t :: Site) (n :: N') x.
ConsecutiveZero t n x -> Either (t :~: 'From) (t :~: 'To)
cnzSite ConsecutiveZero t n x
c

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

-- vrcMapCov -


-- | covariant mapping of 'VarianceG'.

vrcMapCov ::
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h
  , NaturalConic (Inv2 h) k Dst Projective d (Parallel LeftToRight) N2 N1
  , NaturalConic (Inv2 h) c Dst Injective d (Parallel RightToLeft) N2 N1
  )
  => Variant2 Covariant (Inv2 h) x y -> VarianceG t k c d n x -> VarianceG t k c d n y
vrcMapCov :: forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Covariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG t k c d n y
vrcMapCov Variant2 'Covariant (Inv2 h) x y
i (VarianceG ConsecutiveZero t n x
c FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
vs) = ConsecutiveZero t n y
-> FinList (n + 1) (KernelG k d N1 y, CokernelG c d N1 y)
-> VarianceG t k c d n y
forall (t :: Site) (n :: N') x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
ConsecutiveZero t n x
-> FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
-> VarianceG t k c d n x
VarianceG ConsecutiveZero t n y
c' FinList (n + 1) (KernelG k d N1 y, CokernelG c d N1 y)
FinList ('S n) (KernelG k d N1 y, CokernelG c d N1 y)
vs' where
  c' :: ConsecutiveZero t n y
c'  = Variant2 'Covariant (Inv2 h) x y
-> ConsecutiveZero t n x -> ConsecutiveZero t n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
HomDistributiveDisjunctive h =>
Variant2 'Covariant h x y
-> ConsecutiveZero t n x -> ConsecutiveZero t n y
cnzMapCov Variant2 'Covariant (Inv2 h) x y
i ConsecutiveZero t n x
c
  vs' :: FinList ('S n) (KernelG k d N1 y, CokernelG c d N1 y)
vs' = ((KernelG k d N1 x, CokernelG c d N1 x)
 -> (KernelG k d N1 y, CokernelG c d N1 y))
-> FinList ('S n) (KernelG k d N1 x, CokernelG c d N1 x)
-> FinList ('S n) (KernelG k d N1 y, CokernelG c d N1 y)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(KernelG k d N1 x
ker,CokernelG c d N1 x
coker) -> (Variant2 'Covariant (Inv2 h) x y
-> KernelG k d N1 x -> KernelG k d N1 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.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s p d t n m y
lmMapCov Variant2 'Covariant (Inv2 h) x y
i KernelG k d N1 x
ker, Variant2 'Covariant (Inv2 h) x y
-> CokernelG c d N1 x -> CokernelG c d N1 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.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s p d t n m y
lmMapCov Variant2 'Covariant (Inv2 h) x y
i CokernelG c d N1 x
coker)) FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
FinList ('S n) (KernelG k d N1 x, CokernelG c d N1 x)
vs

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

-- vrcMapCnt -


-- | contravariant mapping of 'VarianceG'.

vrcMapCnt ::
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h
  , NaturalConic (Inv2 h) k Dst Projective d (Parallel LeftToRight) N2 N1
  , NaturalConic (Inv2 h) c Dst Injective d (Parallel RightToLeft) N2 N1
  )
  => Variant2 Contravariant (Inv2 h) x y -> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
vrcMapCnt :: forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Contravariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
vrcMapCnt Variant2 'Contravariant (Inv2 h) x y
i (VarianceG ConsecutiveZero t n x
c FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
vs) = ConsecutiveZero (Dual t) n y
-> FinList (n + 1) (KernelG c d N1 y, CokernelG k d N1 y)
-> VarianceG (Dual t) c k d n y
forall (t :: Site) (n :: N') x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
ConsecutiveZero t n x
-> FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
-> VarianceG t k c d n x
VarianceG ConsecutiveZero (Dual t) n y
c' FinList (n + 1) (KernelG c d N1 y, CokernelG k d N1 y)
FinList ('S n) (KernelG c d N1 y, CokernelG k d N1 y)
vs' where
  c' :: ConsecutiveZero (Dual t) n y
c'  = Variant2 'Contravariant (Inv2 h) x y
-> ConsecutiveZero t n x -> ConsecutiveZero (Dual t) n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
HomDistributiveDisjunctive h =>
Variant2 'Contravariant h x y
-> ConsecutiveZero t n x -> ConsecutiveZero (Dual t) n y
cnzMapCnt Variant2 'Contravariant (Inv2 h) x y
i ConsecutiveZero t n x
c
  vs' :: FinList ('S n) (KernelG c d N1 y, CokernelG k d N1 y)
vs' = ((KernelG k d N1 x, CokernelG c d N1 x)
 -> (KernelG c d N1 y, CokernelG k d N1 y))
-> FinList ('S n) (KernelG k d N1 x, CokernelG c d N1 x)
-> FinList ('S n) (KernelG c d N1 y, CokernelG k d N1 y)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(KernelG k d N1 x
ker,CokernelG c d N1 x
coker) -> (Variant2 'Contravariant (Inv2 h) x y
-> CokernelG c d N1 x
-> LimesG
     c Dst (Dual 'Injective) d (Dual ('Parallel 'RightToLeft)) N2 N1 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.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s (Dual p) d (Dual t) n m y
lmMapCnt Variant2 'Contravariant (Inv2 h) x y
i CokernelG c d N1 x
coker, Variant2 'Contravariant (Inv2 h) x y
-> KernelG k d N1 x
-> LimesG
     k Dst (Dual 'Projective) d (Dual ('Parallel 'LeftToRight)) N2 N1 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.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s (Dual p) d (Dual t) n m y
lmMapCnt Variant2 'Contravariant (Inv2 h) x y
i KernelG k d N1 x
ker)) FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
FinList ('S n) (KernelG k d N1 x, CokernelG c d N1 x)
vs

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

-- Duality -


type instance Dual1 (VarianceG t k c d n) = VarianceG (Dual t) c k d n

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

-- vrcMapS -


-- | mapping of 'VarianceG'.

vrcMapS :: 
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h
  , NaturalConicBi (Inv2 h) k Dst Projective d (Parallel LeftToRight) N2 N1
  , NaturalConicBi (Inv2 h) c Dst Injective d (Parallel RightToLeft) N2 N1
  , t ~ Dual (Dual t)
  )
  => Inv2 h x y -> SDualBi (VarianceG t k c d n) x  -> SDualBi (VarianceG t k c d n) y
vrcMapS :: forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) x y (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConicBi
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConicBi
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1,
 t ~ Dual (Dual t)) =>
Inv2 h x y
-> SDualBi (VarianceG t k c d n) x
-> SDualBi (VarianceG t k c d n) y
vrcMapS = (Variant2 'Covariant (Inv2 h) x y
 -> VarianceG t k c d n x -> VarianceG t k c d n y)
-> (Variant2 'Covariant (Inv2 h) x y
    -> Dual1 (VarianceG t k c d n) x -> Dual1 (VarianceG t k c d n) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> VarianceG t k c d n x -> Dual1 (VarianceG t k c d n) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> Dual1 (VarianceG t k c d n) x -> VarianceG t k c d n y)
-> Inv2 h x y
-> SDualBi (VarianceG t k c d n) x
-> SDualBi (VarianceG t k c d n) 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
-> VarianceG t k c d n x -> VarianceG t k c d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Covariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG t k c d n y
vrcMapCov Variant2 'Covariant (Inv2 h) x y
-> Dual1 (VarianceG t k c d n) x -> Dual1 (VarianceG t k c d n) y
Variant2 'Covariant (Inv2 h) x y
-> VarianceG (Dual t) c k d n x -> VarianceG (Dual t) c k d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Covariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG t k c d n y
vrcMapCov Variant2 'Contravariant (Inv2 h) x y
-> VarianceG t k c d n x -> Dual1 (VarianceG t k c d n) y
Variant2 'Contravariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Contravariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
vrcMapCnt Variant2 'Contravariant (Inv2 h) x y
-> Dual1 (VarianceG t k c d n) x -> VarianceG t k c d n y
Variant2 'Contravariant (Inv2 h) x y
-> VarianceG (Dual t) c k d n x
-> VarianceG (Dual (Dual t)) k c d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Contravariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
vrcMapCnt

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

-- NaturalKernelCokernel -


-- | natural conics for kernels and cokenrels.

type NaturalKernelCokernel h k c d =
  ( NaturalConic h k Dst Projective d (Parallel LeftToRight) N2 N1
  , NaturalConic h k Dst Injective d (Parallel RightToLeft) N2 N1
  , NaturalConic h c Dst Projective d (Parallel LeftToRight) N2 N1
  , NaturalConic h c Dst Injective d (Parallel RightToLeft) N2 N1
  )
    
--------------------------------------------------------------------------------

-- FunctorialG -


instance
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h
  , NaturalKernelCokernel (Inv2 h) k c d
  , t ~ Dual (Dual t)

  )
  => ApplicativeG (SDualBi (VarianceG t k c d n)) (Inv2 h) (->) where
  amapG :: forall x y.
Inv2 h x y
-> SDualBi (VarianceG t k c d n) x
   -> SDualBi (VarianceG t k c d n) y
amapG = Inv2 h x y
-> SDualBi (VarianceG t k c d n) x
-> SDualBi (VarianceG t k c d n) y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) x y (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConicBi
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConicBi
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1,
 t ~ Dual (Dual t)) =>
Inv2 h x y
-> SDualBi (VarianceG t k c d n) x
-> SDualBi (VarianceG t k c d n) y
vrcMapS

instance
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h
  , NaturalKernelCokernel (Inv2 h) k c d
  , t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (VarianceG t k c d n)) (Inv2 h) (->)

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

-- vrcHead -


-- | the head.

vrcHead :: Distributive x => VarianceG t k c d n x -> VarianceG t k c d N0 x
vrcHead :: forall x (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
Distributive x =>
VarianceG t k c d n x -> VarianceG t k c d N0 x
vrcHead (VarianceG ConsecutiveZero t n x
c FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
vs) = ConsecutiveZero t N0 x
-> FinList (N0 + 1) (KernelG k d N1 x, CokernelG c d N1 x)
-> VarianceG t k c d N0 x
forall (t :: Site) (n :: N') x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
ConsecutiveZero t n x
-> FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
-> VarianceG t k c d n x
VarianceG (ConsecutiveZero t n x -> ConsecutiveZero t N0 x
forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZero t n x -> ConsecutiveZero t N0 x
cnzHead ConsecutiveZero t n x
c) (FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
-> (KernelG k d N1 x, CokernelG c d N1 x)
forall (n :: N') a. FinList (n + 1) a -> a
head FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
vs(KernelG k d N1 x, CokernelG c d N1 x)
-> FinList N0 (KernelG k d N1 x, CokernelG c d N1 x)
-> FinList (N0 + 1) (KernelG k d N1 x, CokernelG c d N1 x)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList N0 (KernelG k d N1 x, CokernelG c d N1 x)
forall a. FinList N0 a
Nil)

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

-- vrcTail -


-- | the tail.

vrcTail :: Distributive x => VarianceG t k c d (n+1) x -> VarianceG t k c d n x
vrcTail :: forall x (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
Distributive x =>
VarianceG t k c d (n + 1) x -> VarianceG t k c d n x
vrcTail (VarianceG ConsecutiveZero t (n + 1) x
c FinList ((n + 1) + 1) (KernelG k d N1 x, CokernelG c d N1 x)
vs) = ConsecutiveZero t n x
-> FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
-> VarianceG t k c d n x
forall (t :: Site) (n :: N') x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
ConsecutiveZero t n x
-> FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
-> VarianceG t k c d n x
VarianceG (ConsecutiveZero t (n + 1) x -> ConsecutiveZero t n x
forall d (t :: Site) (n :: N').
Distributive d =>
ConsecutiveZero t (n + 1) d -> ConsecutiveZero t n d
cnzTail ConsecutiveZero t (n + 1) x
c) (FinList ('S n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
-> FinList ('S n) (KernelG k d N1 x, CokernelG c d N1 x)
forall (n :: N') a. FinList (n + 1) a -> FinList n a
tail FinList ((n + 1) + 1) (KernelG k d N1 x, CokernelG c d N1 x)
FinList ('S n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
vs)

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

-- ObjectKernelCokernel -


-- | kernels and cokernels admitting 'Object'

type ObjectKernelCokernel k c d x =
  ( Diagrammatic d
  , Object (k Dst Projective d (Parallel LeftToRight) N2 N1 x)  
  , Object (k Dst Injective d (Parallel RightToLeft) N2 N1 (Op x))
  , Object (c Dst Injective d (Parallel RightToLeft) N2 N1 x)
  , Object (c Dst Projective d (Parallel LeftToRight) N2 N1 (Op x))  
  )

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

-- EntityDiagrammatic -


-- | diagrammatic object admitting 'Entity'.

type EntityDiagrammatic d x =
  ( Typeable d
  , Entity (d (Parallel LeftToRight) N2 N1 x)
  , Entity (d (Parallel RightToLeft) N2 N1 x)  
  , Entity (d (Parallel LeftToRight) N2 N1 (Op x))
  , Entity (d (Parallel RightToLeft) N2 N1 (Op x))
  )
  
--------------------------------------------------------------------------------

-- prpVarianceG -


relVarianceGTo ::
  ( Distributive x
  
    -- d

  , Diagrammatic d
  , Typeable d
  , Entity (d (Parallel LeftToRight) N2 N1 x)
  , Entity (d (Parallel RightToLeft) N2 N1 x)

    -- k

  , Conic k
  , Object (k Dst Projective d (Parallel LeftToRight) N2 N1 x)

    -- c

  , Conic c
  , Object (c Dst Injective d (Parallel RightToLeft) N2 N1 x)
  
  )
  => XEligibleConeG k Dst Projective d (Parallel LeftToRight) N2 N1 x
  -> XEligibleConeFactorG k Dst Projective d (Parallel LeftToRight) N2 N1 x
  -> XEligibleConeG c Dst Injective d (Parallel RightToLeft) N2 N1 x
  -> XEligibleConeFactorG c Dst Injective d (Parallel RightToLeft) N2 N1 x
  -> N -> VarianceG To k c d n x -> Statement
relVarianceGTo :: forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (n :: N').
(Distributive x, Diagrammatic d, Typeable d,
 Entity (d ('Parallel 'LeftToRight) N2 N1 x),
 Entity (d ('Parallel 'RightToLeft) N2 N1 x), Conic k,
 Object (k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x),
 Conic c,
 Object (c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x)) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> N
-> VarianceG 'To k c d n x
-> Statement
relVarianceGTo XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc N
i
  v :: VarianceG 'To k c d n x
v@(VarianceG c :: ConsecutiveZero 'To n x
c@(ConsecutiveZero (DiagramChainTo Point x
_ (x
f:|x
g:|FinList n1 x
ds))) ((KernelG k d N1 x
ker,CokernelG c d N1 x
coker):|FinList n1 (KernelG k d N1 x, CokernelG c d N1 x)
_))
  = [Statement] -> Statement
And [ ConsecutiveZero 'To n x -> Statement
forall a. Validable a => a -> Statement
valid ConsecutiveZero 'To n x
c
        , String -> Label
Label String
"ker"   Label -> Statement -> Statement
:<=>: XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> KernelG k d N1 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 k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk KernelG k d N1 x
ker
        , String -> Label
Label String
"coker" Label -> Statement -> Statement
:<=>: XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> CokernelG c d N1 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 Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc CokernelG c d N1 x
coker        
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (x -> KernelDiagram N1 x
forall x. Oriented x => x -> KernelDiagram N1 x
kernelDiagram x
f KernelDiagram N1 x -> KernelDiagram N1 x -> Bool
forall a. Eq a => a -> a -> Bool
== d ('Parallel 'LeftToRight) N2 N1 x -> KernelDiagram N1 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 (KernelG k d N1 x -> d ('Parallel 'LeftToRight) N2 N1 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 x -> d t n m x
universalDiagram KernelG k d N1 x
ker))
                            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [(String
"d " String -> String -> String
forall a. [a] -> [a] -> [a]
L.++ N -> String
forall a. Show a => a -> String
show N
i)String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
f, (String
"ker" String -> String -> String
forall a. [a] -> [a] -> [a]
L.++ N -> String
forall a. Show a => a -> String
show N
i)String -> String -> Parameter
:=KernelG k d N1 x -> String
forall a. Show a => a -> String
show KernelG k d N1 x
ker]
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (x -> CokernelDiagram N1 x
forall x. Oriented x => x -> CokernelDiagram N1 x
cokernelDiagram x
g' CokernelDiagram N1 x -> CokernelDiagram N1 x -> Bool
forall a. Eq a => a -> a -> Bool
== d ('Parallel 'RightToLeft) N2 N1 x -> CokernelDiagram N1 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 (CokernelG c d N1 x -> d ('Parallel 'RightToLeft) N2 N1 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 x -> d t n m x
universalDiagram CokernelG c d N1 x
coker))
                            Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [ (String
"d' " String -> String -> String
forall a. [a] -> [a] -> [a]
L.++ N -> String
forall a. Show a => a -> String
show N
i')String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
g'
                                       , (String
"coker" String -> String -> String
forall a. [a] -> [a] -> [a]
L.++ N -> String
forall a. Show a => a -> String
show N
i)String -> String -> Parameter
:=CokernelG c d N1 x -> String
forall a. Show a => a -> String
show CokernelG c d N1 x
coker
                                       ]
        , case FinList n1 x
ds of
            FinList n1 x
Nil    -> Statement
SValid
            x
_ :| FinList n1 x
_ -> XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> N
-> VarianceG 'To k c d n1 x
-> Statement
forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (n :: N').
(Distributive x, Diagrammatic d, Typeable d,
 Entity (d ('Parallel 'LeftToRight) N2 N1 x),
 Entity (d ('Parallel 'RightToLeft) N2 N1 x), Conic k,
 Object (k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x),
 Conic c,
 Object (c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x)) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> N
-> VarianceG 'To k c d n x
-> Statement
relVarianceGTo XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc N
i' (VarianceG 'To k c d (n1 + 1) x -> VarianceG 'To k c d n1 x
forall x (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
Distributive x =>
VarianceG t k c d (n + 1) x -> VarianceG t k c d n x
vrcTail VarianceG 'To k c d n x
VarianceG 'To k c d (n1 + 1) x
v)
                        

        ] where g' :: x
g' = KernelG k d N1 x
-> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 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 KernelG k d N1 x
ker (d ('Parallel 'LeftToRight) N2 N1 x
-> x -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel (KernelG k d N1 x -> d ('Parallel 'LeftToRight) N2 N1 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 x -> d t n m x
universalDiagram KernelG k d N1 x
ker) x
g)
                i' :: N
i' = N -> N
forall a. Enum a => a -> a
succ N
i

relVarianceG ::
  ( Distributive x
  , EntityDiagrammatic d x
  , NaturalKernelCokernel (IsoO Dst Op) k c d
  , ObjectKernelCokernel k c d x
  )
  => XEligibleConeG k Dst Projective d (Parallel LeftToRight) N2 N1 x
  -> XEligibleConeFactorG k Dst Projective d (Parallel LeftToRight) N2 N1 x
  -> XEligibleConeG c Dst Injective d (Parallel RightToLeft) N2 N1 x
  -> XEligibleConeFactorG c Dst Injective d (Parallel RightToLeft) N2 N1 x
  -> VarianceG t k c d n x -> Statement
relVarianceG :: forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x, EntityDiagrammatic d x,
 NaturalKernelCokernel (IsoO Dst Op) k c d,
 ObjectKernelCokernel k c d x) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t k c d n x
-> Statement
relVarianceG XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc v :: VarianceG t k c d n x
v@(VarianceG (ConsecutiveZero (DiagramChainTo Point x
_ FinList (n + 2) x
_)) FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
_)
  = XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> N
-> VarianceG 'To k c d n x
-> Statement
forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (n :: N').
(Distributive x, Diagrammatic d, Typeable d,
 Entity (d ('Parallel 'LeftToRight) N2 N1 x),
 Entity (d ('Parallel 'RightToLeft) N2 N1 x), Conic k,
 Object (k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x),
 Conic c,
 Object (c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x)) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> N
-> VarianceG 'To k c d n x
-> Statement
relVarianceGTo XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc N
0 VarianceG t k c d n x
VarianceG 'To k c d n x
v

relVarianceG XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc v :: VarianceG t k c d n x
v@(VarianceG (ConsecutiveZero (DiagramChainFrom Point x
_ FinList (n + 2) x
_)) FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
_)
  = XEligibleConeG
  c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 (Op x)
-> XEligibleConeFactorG
     c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 (Op x)
-> XEligibleConeG
     k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 (Op x)
-> XEligibleConeFactorG
     k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 (Op x)
-> N
-> VarianceG 'To c k d n (Op x)
-> Statement
forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (n :: N').
(Distributive x, Diagrammatic d, Typeable d,
 Entity (d ('Parallel 'LeftToRight) N2 N1 x),
 Entity (d ('Parallel 'RightToLeft) N2 N1 x), Conic k,
 Object (k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x),
 Conic c,
 Object (c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x)) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> N
-> VarianceG 'To k c d n x
-> Statement
relVarianceGTo Dual1
  (XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
  (Op x)
XEligibleConeG
  c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 (Op x)
xeck' Dual1
  (XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
  (Op x)
XEligibleConeFactorG
  c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 (Op x)
xecfk' Dual1
  (XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
  (Op x)
XEligibleConeG
  k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 (Op x)
xecc' Dual1
  (XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
  (Op x)
XEligibleConeFactorG
  k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 (Op x)
xecfc' N
0 Dual1 (VarianceG t k c d n) (Op x)
VarianceG 'To c k d n (Op x)
v' where
  Contravariant2 IsoO Dst Op x (Op x)
i       = Variant2 'Contravariant (IsoO Dst Op) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst
  
  SDualBi (Left1 Dual1 (VarianceG t k c d n) (Op x)
v')     = IsoO Dst Op x (Op x)
-> SDualBi (VarianceG t k c d n) x
-> SDualBi (VarianceG t k c d n) (Op x)
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) x y (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConicBi
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConicBi
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1,
 t ~ Dual (Dual t)) =>
Inv2 h x y
-> SDualBi (VarianceG t k c d n) x
-> SDualBi (VarianceG t k c d n) y
vrcMapS IsoO Dst Op x (Op x)
i (Either1 (Dual1 (VarianceG t k c d n)) (VarianceG t k c d n) x
-> SDualBi (VarianceG t k c d n) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (VarianceG t k c d n x
-> Either1 (VarianceG 'To c k d n) (VarianceG t k c d n) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 VarianceG t k c d n x
v))
  
  SDualBi (Left1 Dual1
  (XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
  (Op x)
xeck')  = IsoO Dst Op x (Op x)
-> SDualBi
     (XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     x
-> SDualBi
     (XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     (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 =>
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 IsoO Dst Op x (Op x)
i (Either1
  (Dual1
     (XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1))
  (XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
  x
-> SDualBi
     (XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> Either1
     (XEligibleConeG c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     (XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc))
  SDualBi (Left1 Dual1
  (XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
  (Op x)
xecc')  = IsoO Dst Op x (Op x)
-> SDualBi
     (XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     x
-> SDualBi
     (XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     (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 =>
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 IsoO Dst Op x (Op x)
i (Either1
  (Dual1
     (XEligibleConeG
        k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1))
  (XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
  x
-> SDualBi
     (XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> Either1
     (XEligibleConeG k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     (XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck))
  SDualBi (Left1 Dual1
  (XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
  (Op x)
xecfk') = IsoO Dst Op x (Op x)
-> SDualBi
     (XEligibleConeFactorG
        c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     x
-> SDualBi
     (XEligibleConeFactorG
        c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     (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 =>
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 IsoO Dst Op x (Op x)
i (Either1
  (Dual1
     (XEligibleConeFactorG
        c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1))
  (XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
  x
-> SDualBi
     (XEligibleConeFactorG
        c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> Either1
     (XEligibleConeFactorG
        c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     (XEligibleConeFactorG
        c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc))
  SDualBi (Left1 Dual1
  (XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
  (Op x)
xecfc') = IsoO Dst Op x (Op x)
-> SDualBi
     (XEligibleConeFactorG
        k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     x
-> SDualBi
     (XEligibleConeFactorG
        k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     (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 =>
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 IsoO Dst Op x (Op x)
i (Either1
  (Dual1
     (XEligibleConeFactorG
        k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1))
  (XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
  x
-> SDualBi
     (XEligibleConeFactorG
        k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> Either1
     (XEligibleConeFactorG
        k Dst 'Injective d ('Parallel 'RightToLeft) N2 N1)
     (XEligibleConeFactorG
        k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk))
  

-- | validity according to 'VarianceG'.

prpVarianceG ::
  ( Distributive x
  , EntityDiagrammatic d x
  , NaturalKernelCokernel (IsoO Dst Op) k c d
  , ObjectKernelCokernel k c d x
  )
  => XEligibleConeG k Dst Projective d (Parallel LeftToRight) N2 N1 x
  -> XEligibleConeFactorG k Dst Projective d (Parallel LeftToRight) N2 N1 x
  -> XEligibleConeG c Dst Injective d (Parallel RightToLeft) N2 N1 x
  -> XEligibleConeFactorG c Dst Injective d (Parallel RightToLeft) N2 N1 x
  -> VarianceG t k c d n x -> Statement
prpVarianceG :: forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x, EntityDiagrammatic d x,
 NaturalKernelCokernel (IsoO Dst Op) k c d,
 ObjectKernelCokernel k c d x) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t k c d n x
-> Statement
prpVarianceG XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc VarianceG t k c d n x
v = String -> Label
Prp String
"VarianceG"
  Label -> Statement -> Statement
:<=>: XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t k c d n x
-> Statement
forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x, EntityDiagrammatic d x,
 NaturalKernelCokernel (IsoO Dst Op) k c d,
 ObjectKernelCokernel k c d x) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t k c d n x
-> Statement
relVarianceG XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc VarianceG t k c d n x
v


instance
  ( Distributive x
  , XStandardEligibleConeKernel N1 x
  , XStandardEligibleConeFactorKernel N1 x
  , XStandardEligibleConeCokernel N1 x
  , XStandardEligibleConeFactorCokernel N1 x
  )
  => Validable (VarianceG t Cone Cone Diagram n x) where
  valid :: VarianceG t Cone Cone Diagram n x -> Statement
valid = XEligibleConeG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t Cone Cone Diagram n x
-> Statement
forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x, EntityDiagrammatic d x,
 NaturalKernelCokernel (IsoO Dst Op) k c d,
 ObjectKernelCokernel k c d x) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t k c d n x
-> Statement
prpVarianceG XEligibleConeG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 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
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 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
                      XEligibleConeG
  Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 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
  Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 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

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

-- variance -


-- | the variance for the site 'To' according to 'Kernels' and 'Cokernels'.

varianceTo :: Distributive x
  => Kernels N1 x -> Cokernels N1 x
  -> ConsecutiveZero To n x -> Variance To n x
varianceTo :: forall x (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZero 'To n x -> Variance 'To n x
varianceTo Kernels N1 x
ker Cokernels N1 x
coker ConsecutiveZero 'To n x
c = ConsecutiveZero 'To n x
-> FinList
     (n + 1) (KernelG Cone Diagram N1 x, CokernelG Cone Diagram N1 x)
-> VarianceG 'To Cone Cone Diagram n x
forall (t :: Site) (n :: N') x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
ConsecutiveZero t n x
-> FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
-> VarianceG t k c d n x
VarianceG ConsecutiveZero 'To n x
c (Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero 'To n x
-> FinList
     (n + 1) (KernelG Cone Diagram N1 x, CokernelG Cone Diagram N1 x)
forall x (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero 'To n x
-> FinList (n + 1) (Kernel N1 x, Cokernel N1 x)
kcs Kernels N1 x
ker Cokernels N1 x
coker ConsecutiveZero 'To n x
c) where

  kc :: Distributive x
    => Kernels N1 x -> Cokernels N1 x
    -> ConsecutiveZero To n x -> (Kernel N1 x,Cokernel N1 x)
  kc :: forall x (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero 'To n x
-> (Kernel N1 x, Cokernel N1 x)
kc Kernels N1 x
ks Cokernels N1 x
cs (ConsecutiveZero (DiagramChainTo Point x
_ (x
v:|x
w:|FinList n1 x
_))) = (LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
k,LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 x
c) where
    k :: LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
k  = Kernels N1 x
-> Diagram ('Parallel 'LeftToRight) N2 N1 x
-> LimesG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes Kernels N1 x
ks (x -> Diagram ('Parallel 'LeftToRight) N2 N1 x
forall x. Oriented x => x -> KernelDiagram N1 x
kernelDiagram x
v)
    w' :: x
w' = LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 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
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
k (Diagram ('Parallel 'LeftToRight) N2 N1 x
-> x
-> Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel (LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> Diagram ('Parallel 'LeftToRight) N2 N1 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 x -> d t n m x
universalDiagram LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
k) x
w)
    c :: LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 x
c  = Cokernels N1 x
-> Diagram ('Parallel 'RightToLeft) N2 N1 x
-> LimesG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes Cokernels N1 x
cs (x -> Diagram ('Parallel 'RightToLeft) N2 N1 x
forall x. Oriented x => x -> CokernelDiagram N1 x
cokernelDiagram x
w')

  kcs :: Distributive x
    => Kernels N1 x -> Cokernels N1 x
    -> ConsecutiveZero To n x -> FinList (n+1) (Kernel N1 x,Cokernel N1 x)
  kcs :: forall x (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero 'To n x
-> FinList (n + 1) (Kernel N1 x, Cokernel N1 x)
kcs Kernels N1 x
ks Cokernels N1 x
cs c :: ConsecutiveZero 'To n x
c@(ConsecutiveZero (DiagramChainTo Point x
_ (x
_:|x
_:|FinList n1 x
ds)))
    = Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero 'To n x
-> (Kernel N1 x, Cokernel N1 x)
forall x (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero 'To n x
-> (Kernel N1 x, Cokernel N1 x)
kc Kernels N1 x
ks Cokernels N1 x
cs ConsecutiveZero 'To n x
c (Kernel N1 x, Cokernel N1 x)
-> FinList n (Kernel N1 x, Cokernel N1 x)
-> FinList (n + 1) (Kernel N1 x, Cokernel N1 x)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| case FinList n1 x
ds of
        FinList n1 x
Nil     -> FinList n (Kernel N1 x, Cokernel N1 x)
FinList N0 (Kernel N1 x, Cokernel N1 x)
forall a. FinList N0 a
Nil
        x
_ :| FinList n1 x
_  -> Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero 'To n1 x
-> FinList (n1 + 1) (Kernel N1 x, Cokernel N1 x)
forall x (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero 'To n x
-> FinList (n + 1) (Kernel N1 x, Cokernel N1 x)
kcs Kernels N1 x
ks Cokernels N1 x
cs (ConsecutiveZero 'To (n1 + 1) x -> ConsecutiveZero 'To n1 x
forall d (t :: Site) (n :: N').
Distributive d =>
ConsecutiveZero t (n + 1) d -> ConsecutiveZero t n d
cnzTail ConsecutiveZero 'To n x
ConsecutiveZero 'To (n1 + 1) x
c)

-- | the variance according to 'Kernels' and 'Cokernels'.

variance :: Distributive x
  => Kernels N1 x -> Cokernels N1 x
  -> ConsecutiveZero t n x -> Variance t n x
variance :: forall x (t :: Site) (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZero t n x -> Variance t n x
variance Kernels N1 x
ks Cokernels N1 x
cs c :: ConsecutiveZero t n x
c@(ConsecutiveZero (DiagramChainTo Point x
_ FinList (n + 2) x
_))   = Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZero 'To n x -> Variance 'To n x
forall x (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZero 'To n x -> Variance 'To n x
varianceTo Kernels N1 x
ks Cokernels N1 x
cs ConsecutiveZero t n x
ConsecutiveZero 'To n x
c
variance Kernels N1 x
ks Cokernels N1 x
cs c :: ConsecutiveZero t n x
c@(ConsecutiveZero (DiagramChainFrom Point x
_ FinList (n + 2) x
_)) = VarianceG t Cone Cone Diagram n x
v where
  Contravariant2 IsoO Dst Op x (Op x)
i = Variant2 'Contravariant (IsoO Dst Op) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst
  SDualBi (Left1 Dual1 (ConsecutiveZero 'From n) (Op x)
c')  = IsoO Dst Op x (Op x)
-> SDualBi (ConsecutiveZero 'From n) x
-> SDualBi (ConsecutiveZero 'From n) (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Dst Op x (Op x)
i (Either1 (Dual1 (ConsecutiveZero t n)) (ConsecutiveZero t n) x
-> SDualBi (ConsecutiveZero t n) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConsecutiveZero t n x
-> Either1 (ConsecutiveZero 'To n) (ConsecutiveZero t n) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 ConsecutiveZero t n x
c))
  SDualBi (Left1 Dual1
  (LimitsG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
  (Op x)
ks') = IsoO Dst Op x (Op x)
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
     x
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
     (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Dst Op x (Op x)
i (Either1
  (Dual1
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1))
  (LimitsG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
  x
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Cokernels N1 x
-> Either1
     (LimitsG
        Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1)
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Cokernels N1 x
cs))
  SDualBi (Left1 Dual1
  (LimitsG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1)
  (Op x)
cs') = IsoO Dst Op x (Op x)
-> SDualBi
     (LimitsG
        Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1)
     x
-> SDualBi
     (LimitsG
        Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1)
     (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Dst Op x (Op x)
i (Either1
  (Dual1
     (LimitsG
        Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1))
  (LimitsG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1)
  x
-> SDualBi
     (LimitsG
        Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Kernels N1 x
-> Either1
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
     (LimitsG
        Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Kernels N1 x
ks))

  v' :: Variance 'To n (Op x)
v' = Kernels N1 (Op x)
-> Cokernels N1 (Op x)
-> ConsecutiveZero 'To n (Op x)
-> Variance 'To n (Op x)
forall x (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZero 'To n x -> Variance 'To n x
varianceTo Dual1
  (LimitsG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
  (Op x)
Kernels N1 (Op x)
ks' Dual1
  (LimitsG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1)
  (Op x)
Cokernels N1 (Op x)
cs' Dual1 (ConsecutiveZero 'From n) (Op x)
ConsecutiveZero 'To n (Op x)
c'
  SDualBi (Right1 VarianceG t Cone Cone Diagram n x
v) = Inv2 (HomDisjEmpty Dst Op) (Op x) x
-> SDualBi (VarianceG 'From Cone Cone Diagram n) (Op x)
-> SDualBi (VarianceG 'From Cone Cone Diagram n) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Dst Op x (Op x) -> Inv2 (HomDisjEmpty Dst Op) (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Dst Op x (Op x)
i) (Either1
  (Dual1 (VarianceG 'From Cone Cone Diagram n))
  (VarianceG 'From Cone Cone Diagram n)
  (Op x)
-> SDualBi (VarianceG 'From Cone Cone Diagram n) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Variance 'To n (Op x)
-> Either1
     (VarianceG 'To Cone Cone Diagram n)
     (VarianceG 'From Cone Cone Diagram n)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Variance 'To n (Op x)
v'))

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

-- vrcConsZeroHom -


-- | the induced @'ConsecutiveZeroHom' __'To'__@.

vrcConsZeroHomTo ::
  ( Distributive x
  , Conic c, Conic k
  )
  => VarianceG To k c d n x -> ConsecutiveZeroHom To n x
vrcConsZeroHomTo :: forall x
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, Conic c, Conic k) =>
VarianceG 'To k c d n x -> ConsecutiveZeroHom 'To n x
vrcConsZeroHomTo (VarianceG (ConsecutiveZero top :: Diagram ('Chain 'To) (n + 3) (n + 2) x
top@(DiagramChainTo Point x
a (x
_:|x
w:|FinList n1 x
ds))) ((KernelG k d N1 x
ker,CokernelG c d N1 x
coker):|FinList n1 (KernelG k d N1 x, CokernelG c d N1 x)
_))
  = DiagramTrafo ('Chain 'To) (n + 3) (n + 2) x
-> ConsecutiveZeroHom 'To n x
forall (t :: Site) (n :: N') x.
DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
ConsecutiveZeroHom (Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) x
-> Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) x
-> FinList ('S ('S ('S n))) x
-> DiagramTrafo ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> DiagramTrafo t n m a
DiagramTrafo Diagram ('Chain 'To) ('S ('S n) + 1) ('S ('S n)) x
Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) x
bot Diagram ('Chain 'To) (n + 3) (n + 2) x
Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) x
top FinList ('S ('S n) + 1) x
FinList ('S ('S ('S n))) x
ts) where
  bot :: Diagram ('Chain 'To) ('S ('S n) + 1) ('S ('S n)) x
bot = Point x
-> FinList ('S ('S n)) x
-> Diagram ('Chain 'To) ('S ('S n) + 1) ('S ('S n)) x
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo Point x
a' (x
v'x -> FinList ('S n) x -> FinList ('S n + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
w'x -> FinList n1 x -> FinList (n1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList n1 x
ds)
  a' :: Point x
a'  = x -> Point x
forall q. Oriented q => q -> Point q
end x
v'
  v' :: x
v'  = CokernelConic c d N1 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Conic c =>
CokernelConic c d n x -> x
cokernelFactor (CokernelConic c d N1 x -> x) -> CokernelConic c d N1 x -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ CokernelG c d N1 x -> CokernelConic c d N1 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 CokernelG c d N1 x
coker
  w' :: x
w'  = KernelG k d N1 x
-> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 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 KernelG k d N1 x
ker (d ('Parallel 'LeftToRight) N2 N1 x
-> x -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel (KernelG k d N1 x -> d ('Parallel 'LeftToRight) N2 N1 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 x -> d t n m x
universalDiagram KernelG k d N1 x
ker) x
w)
  
  ts :: FinList ('S ('S n) + 1) x
ts = Root x -> x
forall a. Additive a => Root a -> a
zero (Point x
a'Point x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:>Point x
a)x -> FinList ('S ('S n)) x -> FinList ('S ('S n) + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| KernelConic k d N1 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Conic c =>
KernelConic c d n x -> x
kernelFactor (KernelG k d N1 x -> KernelConic k d N1 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 KernelG k d N1 x
ker) x -> FinList ('S n) x -> FinList ('S n + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| (x -> x) -> FinList ('S n) x -> FinList ('S n) x
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Point x -> x
forall c. Multiplicative c => Point c -> c
one (Point x -> x) -> (x -> Point x) -> x -> 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 -> Point x
forall q. Oriented q => q -> Point q
start) (x
wx -> FinList n1 x -> FinList (n1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList n1 x
ds)
  

-- | the induce homomorphism of consecutive zero-able chains.

--

-- __Property__ Let @v = 'VarianceG' c vs@ be in @'VarianceG' __t k c d n x__@, then holds:

--

-- (1) If @c@ matches @'ConsecutiveZero' ('DiagramChainTo _ _)@ then holds:

--

--     (1) @'end' ('vrcConsZeroHom' v) '==' c@.

--

--     (2) @ti@ is given by the diagram below.

--

-- @

--                                 v              w               

-- top:      end t         a <------------ b <------------ c <------------ d ...

--             ^           ^               ^              ||              ||

--             |           |               |              ||              ||

--           t |           | t0 = 0        | t1 = ker0 v  || t2 = one c   || t3 = one d ...

--             |           |               |              ||              ||

--             |           |               ^              ||              || 

-- bottom:  start t        a'<<----------- b'<------------ c <------------ d ...

--                           v' = coker0 w'        w' 

-- @

--

-- (2) If @c@ matches @'ConsecutiveZero' ('DiagramChainFrom' _ _)@ then holds:

--

--     (1) @'start' ('vrcConsZeroHom' v) '==' c@.

--

--     (2) @t i@ is given by the diagram below.

--

-- @

--                                  v               w

-- top:      sart t        a ------------> b -------------> c ------------> d ...

--             |           |               |               ||              ||

--             |           |               |               ||              ||

--           t |           | t0 = 0        | t1 = coker0 v || t2 = one c   || t3 = one d ...

--             |           |               v               ||              ||

--             v           v               v               ||              ||

-- bottom:   end t         a'>-----------> b'-------------> c ------------> d ...

--                           v' = ker0 w'          w'

-- @

vrcConsZeroHom :: (Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d)
  => VarianceG t k c d n x -> ConsecutiveZeroHom t n x
vrcConsZeroHom :: forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d) =>
VarianceG t k c d n x -> ConsecutiveZeroHom t n x
vrcConsZeroHom v :: VarianceG t k c d n x
v@(VarianceG (ConsecutiveZero (DiagramChainTo Point x
_ FinList (n + 2) x
_)) FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
_)   = VarianceG 'To k c d n x -> ConsecutiveZeroHom 'To n x
forall x
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, Conic c, Conic k) =>
VarianceG 'To k c d n x -> ConsecutiveZeroHom 'To n x
vrcConsZeroHomTo VarianceG t k c d n x
VarianceG 'To k c d n x
v
vrcConsZeroHom v :: VarianceG t k c d n x
v@(VarianceG (ConsecutiveZero (DiagramChainFrom Point x
_ FinList (n + 2) x
_)) FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
_) = ConsecutiveZeroHom t n x
t where
  Contravariant2 IsoO Dst Op x (Op x)
i   = Variant2 'Contravariant (IsoO Dst Op) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst
  SDualBi (Left1 Dual1 (VarianceG 'From k c d n) (Op x)
v') = IsoO Dst Op x (Op x)
-> SDualBi (VarianceG 'From k c d n) x
-> SDualBi (VarianceG 'From k c d n) (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Dst Op x (Op x)
i (Either1 (Dual1 (VarianceG t k c d n)) (VarianceG t k c d n) x
-> SDualBi (VarianceG t k c d n) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (VarianceG t k c d n x
-> Either1 (VarianceG 'To c k d n) (VarianceG t k c d n) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 VarianceG t k c d n x
v))
  t' :: ConsecutiveZeroHom 'To n (Op x)
t'                 = VarianceG 'To c k d n (Op x) -> ConsecutiveZeroHom 'To n (Op x)
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d) =>
VarianceG t k c d n x -> ConsecutiveZeroHom t n x
vrcConsZeroHom Dual1 (VarianceG 'From k c d n) (Op x)
VarianceG 'To c k d n (Op x)
v'
  SDualBi (Right1 ConsecutiveZeroHom t n x
t) = Inv2 (HomDisjEmpty Dst Op) (Op x) x
-> SDualBi (ConsecutiveZeroHom 'From n) (Op x)
-> SDualBi (ConsecutiveZeroHom 'From n) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Dst Op x (Op x) -> Inv2 (HomDisjEmpty Dst Op) (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Dst Op x (Op x)
i) (Either1
  (Dual1 (ConsecutiveZeroHom 'From n))
  (ConsecutiveZeroHom 'From n)
  (Op x)
-> SDualBi (ConsecutiveZeroHom 'From n) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConsecutiveZeroHom 'To n (Op x)
-> Either1
     (ConsecutiveZeroHom 'To n) (ConsecutiveZeroHom 'From n) (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 ConsecutiveZeroHom 'To n (Op x)
t'))

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

-- VarianceGHom -


-- | homomorphism between variances.

--

-- __Property__ Let @t@ be in @'VarianceGHom' __t k c d n x__@, the holds:

--

-- (1) the induced homomorphism @'vrcHomConsZeroHom' t@ is 'valid'.

data VarianceGHom t k c d n x
  = VarianceGHom (VarianceG t k c d n x) (VarianceG t k c d n x) (FinList (n+3) x)

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

-- VarianceHom -


-- | homomorphism according to 'Kernel' and 'Cokernel'.

type VarianceHom t = VarianceGHom t Cone Cone Diagram

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

-- vrcHomSite -


-- | proof that the site is either 'From' or 'To'.

vrcHomSite :: VarianceGHom t k c d n x -> Either (t :~: From) (t :~: To)
vrcHomSite :: forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceGHom t k c d n x -> Either (t :~: 'From) (t :~: 'To)
vrcHomSite (VarianceGHom VarianceG t k c d n x
v VarianceG t k c d n x
_ FinList (n + 3) x
_) = VarianceG t k c d n x -> Either (t :~: 'From) (t :~: 'To)
forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceG t k c d n x -> Either (t :~: 'From) (t :~: 'To)
vrcSite VarianceG t k c d n x
v

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

-- vrcHomConsZeroHom -


-- | the induce homomorphism between consecutive zero chains.

vrcHomConsZeroHom :: VarianceGHom t k c d n x -> ConsecutiveZeroHom t n x
vrcHomConsZeroHom :: forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceGHom t k c d n x -> ConsecutiveZeroHom t n x
vrcHomConsZeroHom (VarianceGHom VarianceG t k c d n x
a VarianceG t k c d n x
b FinList (n + 3) x
fs) = DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
forall (t :: Site) (n :: N') x.
DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t where
  VarianceG (ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
a') FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
_ = VarianceG t k c d n x
a
  VarianceG (ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
b') FinList (n + 1) (KernelG k d N1 x, CokernelG c d N1 x)
_ = VarianceG t k c d n x
b
  t :: DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t = Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> FinList ('S ('S ('S n))) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> DiagramTrafo t n m a
DiagramTrafo Diagram ('Chain t) (n + 3) (n + 2) x
Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
a' Diagram ('Chain t) (n + 3) (n + 2) x
Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
b' FinList (n + 3) x
FinList ('S ('S ('S n))) x
fs

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

-- prpVarianceGHom -


-- | validity according to 'VarianceGHom'.

prpVarianceGHom ::
  ( Distributive x
  , EntityDiagrammatic d x
  , NaturalKernelCokernel (IsoO Dst Op) k c d
  , ObjectKernelCokernel k c d x
  , Typeable t, Typeable n
  )
  => XEligibleConeG k Dst Projective d (Parallel LeftToRight) N2 N1 x
  -> XEligibleConeFactorG k Dst Projective d (Parallel LeftToRight) N2 N1 x
  -> XEligibleConeG c Dst Injective d (Parallel RightToLeft) N2 N1 x
  -> XEligibleConeFactorG c Dst Injective d (Parallel RightToLeft) N2 N1 x
  -> VarianceGHom t k c d n x -> Statement
prpVarianceGHom :: forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x, EntityDiagrammatic d x,
 NaturalKernelCokernel (IsoO Dst Op) k c d,
 ObjectKernelCokernel k c d x, Typeable t, Typeable n) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceGHom t k c d n x
-> Statement
prpVarianceGHom XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc t :: VarianceGHom t k c d n x
t@(VarianceGHom VarianceG t k c d n x
a VarianceG t k c d n x
b FinList (n + 3) x
_) = String -> Label
Prp String
"VarianceGHom" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"start" Label -> Statement -> Statement
:<=>: XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t k c d n x
-> Statement
forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x, EntityDiagrammatic d x,
 NaturalKernelCokernel (IsoO Dst Op) k c d,
 ObjectKernelCokernel k c d x) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t k c d n x
-> Statement
prpVarianceG XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc VarianceG t k c d n x
a
      , String -> Label
Label String
"end" Label -> Statement -> Statement
:<=>: XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t k c d n x
-> Statement
forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x, EntityDiagrammatic d x,
 NaturalKernelCokernel (IsoO Dst Op) k c d,
 ObjectKernelCokernel k c d x) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceG t k c d n x
-> Statement
prpVarianceG XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xeck XEligibleConeFactorG
  k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
xecfk XEligibleConeG c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecc XEligibleConeFactorG
  c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
xecfc VarianceG t k c d n x
b
      , String -> Label
Label String
"trafo" Label -> Statement -> Statement
:<=>: ConsecutiveZeroHom t n x -> Statement
forall a. Validable a => a -> Statement
valid (VarianceGHom t k c d n x -> ConsecutiveZeroHom t n x
forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceGHom t k c d n x -> ConsecutiveZeroHom t n x
vrcHomConsZeroHom VarianceGHom t k c d n x
t)
      ]

instance
  ( Distributive x
  , XStandardEligibleConeKernel N1 x
  , XStandardEligibleConeFactorKernel N1 x
  , XStandardEligibleConeCokernel N1 x
  , XStandardEligibleConeFactorCokernel N1 x
  , Typeable t, Typeable n
  )
  => Validable (VarianceGHom t Cone Cone Diagram n x) where
  valid :: VarianceGHom t Cone Cone Diagram n x -> Statement
valid = XEligibleConeG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 x
-> VarianceGHom t Cone Cone Diagram n x
-> Statement
forall x (d :: DiagramType -> N' -> N' -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x, EntityDiagrammatic d x,
 NaturalKernelCokernel (IsoO Dst Op) k c d,
 ObjectKernelCokernel k c d x, Typeable t, Typeable n) =>
XEligibleConeG k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeFactorG
     k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
-> XEligibleConeG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> XEligibleConeFactorG
     c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
-> VarianceGHom t k c d n x
-> Statement
prpVarianceGHom XEligibleConeG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 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
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 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
                           XEligibleConeG
  Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 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
  Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1 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

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

-- vrcHomMapCov -


-- | covariant mapping of 'VarianceGHom'.

vrcHomMapCov ::
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h  
  , NaturalConic (Inv2 h) k Dst Projective d (Parallel LeftToRight) N2 N1
  , NaturalConic (Inv2 h) c Dst Injective d (Parallel RightToLeft) N2 N1
  )
  => Variant2 Covariant (Inv2 h) x y -> VarianceGHom t k c d n x -> VarianceGHom t k c d n y
vrcHomMapCov :: forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Covariant (Inv2 h) x y
-> VarianceGHom t k c d n x -> VarianceGHom t k c d n y
vrcHomMapCov Variant2 'Covariant (Inv2 h) x y
h (VarianceGHom VarianceG t k c d n x
a VarianceG t k c d n x
b FinList (n + 3) x
fs) = VarianceG t k c d n y
-> VarianceG t k c d n y
-> FinList (n + 3) y
-> VarianceGHom t k c d n y
forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceG t k c d n x
-> VarianceG t k c d n x
-> FinList (n + 3) x
-> VarianceGHom t k c d n x
VarianceGHom VarianceG t k c d n y
a' VarianceG t k c d n y
b' FinList (n + 3) y
FinList ('S ('S ('S n))) y
fs' where
  a' :: VarianceG t k c d n y
a'  = Variant2 'Covariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG t k c d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Covariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG t k c d n y
vrcMapCov Variant2 'Covariant (Inv2 h) x y
h VarianceG t k c d n x
a
  b' :: VarianceG t k c d n y
b'  = Variant2 'Covariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG t k c d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Covariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG t k c d n y
vrcMapCov Variant2 'Covariant (Inv2 h) x y
h VarianceG t k c d n x
b
  fs' :: FinList ('S ('S ('S n))) y
fs' = (x -> y)
-> FinList ('S ('S ('S n))) x -> FinList ('S ('S ('S n))) y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Variant2 'Covariant (Inv2 h) x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Variant2 'Covariant (Inv2 h) x y
h) FinList (n + 3) x
FinList ('S ('S ('S n))) x
fs

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

-- vrcHomMapCnt -


-- | contravariant mapping of 'VarianceGHom'.

vrcHomMapCnt ::
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h  
  , NaturalConic (Inv2 h) k Dst Projective d (Parallel LeftToRight) N2 N1
  , NaturalConic (Inv2 h) c Dst Injective d (Parallel RightToLeft) N2 N1
  )
  => Variant2 Contravariant (Inv2 h) x y
  -> VarianceGHom t k c d n x -> VarianceGHom (Dual t) c k d n y
vrcHomMapCnt :: forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Contravariant (Inv2 h) x y
-> VarianceGHom t k c d n x -> VarianceGHom (Dual t) c k d n y
vrcHomMapCnt Variant2 'Contravariant (Inv2 h) x y
h (VarianceGHom VarianceG t k c d n x
a VarianceG t k c d n x
b FinList (n + 3) x
fs) = VarianceG (Dual t) c k d n y
-> VarianceG (Dual t) c k d n y
-> FinList (n + 3) y
-> VarianceGHom (Dual t) c k d n y
forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceG t k c d n x
-> VarianceG t k c d n x
-> FinList (n + 3) x
-> VarianceGHom t k c d n x
VarianceGHom VarianceG (Dual t) c k d n y
b' VarianceG (Dual t) c k d n y
a' FinList (n + 3) y
FinList ('S ('S ('S n))) y
fs' where
  a' :: VarianceG (Dual t) c k d n y
a'  = Variant2 'Contravariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Contravariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
vrcMapCnt Variant2 'Contravariant (Inv2 h) x y
h VarianceG t k c d n x
a
  b' :: VarianceG (Dual t) c k d n y
b'  = Variant2 'Contravariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Contravariant (Inv2 h) x y
-> VarianceG t k c d n x -> VarianceG (Dual t) c k d n y
vrcMapCnt Variant2 'Contravariant (Inv2 h) x y
h VarianceG t k c d n x
b
  fs' :: FinList ('S ('S ('S n))) y
fs' = (x -> y)
-> FinList ('S ('S ('S n))) x -> FinList ('S ('S ('S n))) y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Variant2 'Contravariant (Inv2 h) x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Variant2 'Contravariant (Inv2 h) x y
h) FinList (n + 3) x
FinList ('S ('S ('S n))) x
fs

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

-- Duality -


type instance Dual1 (VarianceGHom t k c d n) = VarianceGHom (Dual t) c k d n

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

-- vrcHomMapS -


-- | mapping of 'VarianceGHom'.

vrcHomMapS :: 
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h  
  , NaturalConicBi (Inv2 h) k Dst Projective d (Parallel LeftToRight) N2 N1
  , NaturalConicBi (Inv2 h) c Dst Injective d (Parallel RightToLeft) N2 N1
  , t ~ Dual (Dual t)
  )
  => Inv2 h x y -> SDualBi (VarianceGHom t k c d n) x -> SDualBi (VarianceGHom t k c d n) y
vrcHomMapS :: forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) x y (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConicBi
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConicBi
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1,
 t ~ Dual (Dual t)) =>
Inv2 h x y
-> SDualBi (VarianceGHom t k c d n) x
-> SDualBi (VarianceGHom t k c d n) y
vrcHomMapS = (Variant2 'Covariant (Inv2 h) x y
 -> VarianceGHom t k c d n x -> VarianceGHom t k c d n y)
-> (Variant2 'Covariant (Inv2 h) x y
    -> Dual1 (VarianceGHom t k c d n) x
    -> Dual1 (VarianceGHom t k c d n) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> VarianceGHom t k c d n x -> Dual1 (VarianceGHom t k c d n) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> Dual1 (VarianceGHom t k c d n) x -> VarianceGHom t k c d n y)
-> Inv2 h x y
-> SDualBi (VarianceGHom t k c d n) x
-> SDualBi (VarianceGHom t k c d n) 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
-> VarianceGHom t k c d n x -> VarianceGHom t k c d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Covariant (Inv2 h) x y
-> VarianceGHom t k c d n x -> VarianceGHom t k c d n y
vrcHomMapCov Variant2 'Covariant (Inv2 h) x y
-> Dual1 (VarianceGHom t k c d n) x
-> Dual1 (VarianceGHom t k c d n) y
Variant2 'Covariant (Inv2 h) x y
-> VarianceGHom (Dual t) c k d n x
-> VarianceGHom (Dual t) c k d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Covariant (Inv2 h) x y
-> VarianceGHom t k c d n x -> VarianceGHom t k c d n y
vrcHomMapCov Variant2 'Contravariant (Inv2 h) x y
-> VarianceGHom t k c d n x -> Dual1 (VarianceGHom t k c d n) y
Variant2 'Contravariant (Inv2 h) x y
-> VarianceGHom t k c d n x -> VarianceGHom (Dual t) c k d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Contravariant (Inv2 h) x y
-> VarianceGHom t k c d n x -> VarianceGHom (Dual t) c k d n y
vrcHomMapCnt Variant2 'Contravariant (Inv2 h) x y
-> Dual1 (VarianceGHom t k c d n) x -> VarianceGHom t k c d n y
Variant2 'Contravariant (Inv2 h) x y
-> VarianceGHom (Dual t) c k d n x
-> VarianceGHom (Dual (Dual t)) k c d n y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConic
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConic
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1) =>
Variant2 'Contravariant (Inv2 h) x y
-> VarianceGHom t k c d n x -> VarianceGHom (Dual t) c k d n y
vrcHomMapCnt

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

-- FunctorialG -


instance
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h
  , NaturalKernelCokernel (Inv2 h) k c d
  , t ~ Dual (Dual t)

  )
  => ApplicativeG (SDualBi (VarianceGHom t k c d n)) (Inv2 h) (->) where
  amapG :: forall x y.
Inv2 h x y
-> SDualBi (VarianceGHom t k c d n) x
   -> SDualBi (VarianceGHom t k c d n) y
amapG = Inv2 h x y
-> SDualBi (VarianceGHom t k c d n) x
-> SDualBi (VarianceGHom t k c d n) y
forall (h :: * -> * -> *)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) x y (n :: N').
(HomDistributiveDisjunctive h, CategoryDisjunctive h,
 NaturalConicBi
   (Inv2 h) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConicBi
   (Inv2 h) c Dst 'Injective d ('Parallel 'RightToLeft) N2 N1,
 t ~ Dual (Dual t)) =>
Inv2 h x y
-> SDualBi (VarianceGHom t k c d n) x
-> SDualBi (VarianceGHom t k c d n) y
vrcHomMapS

instance
  ( HomDistributiveDisjunctive h
  , CategoryDisjunctive h
  , NaturalKernelCokernel (Inv2 h) k c d
  , t ~ Dual (Dual t)

  )
  => FunctorialG (SDualBi (VarianceGHom t k c d n)) (Inv2 h) (->)

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

-- varianceHom --


-- | constructing a 'VarianceGHom' by a 'ConsecutiveZeroHom' according to the given 'Kernels' and

-- 'Cokernels'.

varianceHom :: (Distributive x, Typeable t, Attestable n)
  => Kernels N1 x -> Cokernels N1 x
  -> ConsecutiveZeroHom t n x -> VarianceHom t n x
varianceHom :: forall x (t :: Site) (n :: N').
(Distributive x, Typeable t, Attestable n) =>
Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZeroHom t n x -> VarianceHom t n x
varianceHom Kernels N1 x
kers Cokernels N1 x
cokers ConsecutiveZeroHom t n x
h = VarianceG t Cone Cone Diagram n x
-> VarianceG t Cone Cone Diagram n x
-> FinList (n + 3) x
-> VarianceGHom t Cone Cone Diagram n x
forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceG t k c d n x
-> VarianceG t k c d n x
-> FinList (n + 3) x
-> VarianceGHom t k c d n x
VarianceGHom VarianceG t Cone Cone Diagram n x
a VarianceG t Cone Cone Diagram n x
b FinList (n + 3) x
fs where
  a :: VarianceG t Cone Cone Diagram n x
a  = Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero t n x
-> VarianceG t Cone Cone Diagram n x
forall x (t :: Site) (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZero t n x -> Variance t n x
variance Kernels N1 x
kers Cokernels N1 x
cokers (ConsecutiveZeroHom t n x -> Point (ConsecutiveZeroHom t n x)
forall q. Oriented q => q -> Point q
start ConsecutiveZeroHom t n x
h)
  b :: VarianceG t Cone Cone Diagram n x
b  = Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero t n x
-> VarianceG t Cone Cone Diagram n x
forall x (t :: Site) (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZero t n x -> Variance t n x
variance Kernels N1 x
kers Cokernels N1 x
cokers (ConsecutiveZeroHom t n x -> Point (ConsecutiveZeroHom t n x)
forall q. Oriented q => q -> Point q
end ConsecutiveZeroHom t n x
h)
  fs :: FinList (n + 3) x
fs = ConsecutiveZeroHom t n x -> FinList (n + 3) x
forall (t :: Site) (n :: N') x.
ConsecutiveZeroHom t n x -> FinList (n + 3) x
cnzHomArrows ConsecutiveZeroHom t n x
h

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

-- deviation -


-- | the 'deviation' of being exact, i.e. the 'Point' @a'@ in the diagram of 'VarianceG'.

deviation ::
  ( Distributive x
  , NaturalKernelCokernel (IsoO Dst Op) k c d
  , Typeable t, Typeable n
  )
  => VarianceG t k c d n x -> Point x
deviation :: forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Typeable t, Typeable n) =>
VarianceG t k c d n x -> Point x
deviation VarianceG t k c d n x
v = case ConsecutiveZeroHom t n x
-> Orientation (Point (ConsecutiveZeroHom t n x))
ConsecutiveZeroHom t n x -> Orientation (ConsecutiveZero t n x)
forall q. Oriented q => q -> Orientation (Point q)
orientation (ConsecutiveZeroHom t n x -> Orientation (ConsecutiveZero t n x))
-> ConsecutiveZeroHom t n x -> Orientation (ConsecutiveZero t n x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ VarianceG t k c d n x -> ConsecutiveZeroHom t n x
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d) =>
VarianceG t k c d n x -> ConsecutiveZeroHom t n x
vrcConsZeroHom VarianceG t k c d n x
v of
  ConsecutiveZero (DiagramChainTo Point x
a' FinList (n + 2) x
_) :> ConsecutiveZero t n x
_   -> Point x
a'
  ConsecutiveZero t n x
_ :> ConsecutiveZero (DiagramChainFrom Point x
a' FinList (n + 2) x
_) -> Point x
a'

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

-- Deviation -


-- | measuring the deviations.

type Deviation n = Diagram Discrete n N0

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

-- deviations -


-- | the induced 'Deviation's.

deviations :: 
  ( Distributive x
  , NaturalKernelCokernel (IsoO Dst Op) k c d
  , Typeable t, Attestable n
  )
  => VarianceG t k c d n x -> Deviation (n+1) x
deviations :: forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Typeable t, Attestable n) =>
VarianceG t k c d n x -> Deviation (n + 1) x
deviations VarianceG t k c d n x
v = FinList ('S n) (Point x) -> Diagram 'Discrete ('S n) N0 x
forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete (Any n -> VarianceG t k c d n x -> FinList (n + 1) (Point x)
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Typeable t, Attestable n) =>
Any n -> VarianceG t k c d n x -> FinList (n + 1) (Point x)
dvs Any n
forall (n :: N'). Attestable n => W n
attest VarianceG t k c d n x
v) where

  dvs ::
    ( Distributive x
    , NaturalKernelCokernel (IsoO Dst Op) k c d
    , Typeable t, Attestable n
    )
    => Any n -> VarianceG t k c d n x -> FinList (n+1) (Point x)
  dvs :: forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Typeable t, Attestable n) =>
Any n -> VarianceG t k c d n x -> FinList (n + 1) (Point x)
dvs Any n
n VarianceG t k c d n x
v = VarianceG t k c d n x -> Point x
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Typeable t, Typeable n) =>
VarianceG t k c d n x -> Point x
deviation VarianceG t k c d n x
v Point x -> FinList n (Point x) -> FinList (n + 1) (Point x)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| case Any n
n of
    Any n
W0   -> FinList n (Point x)
FinList N0 (Point x)
forall a. FinList N0 a
Nil
    SW W n1
n -> case W n1 -> Ats n1
forall (n :: N'). Any n -> Ats n
ats W n1
n of Ats n1
Ats -> W n1 -> VarianceG t k c d n1 x -> FinList (n1 + 1) (Point x)
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Typeable t, Attestable n) =>
Any n -> VarianceG t k c d n x -> FinList (n + 1) (Point x)
dvs W n1
n (VarianceG t k c d (n1 + 1) x -> VarianceG t k c d n1 x
forall x (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
Distributive x =>
VarianceG t k c d (n + 1) x -> VarianceG t k c d n x
vrcTail VarianceG t k c d n x
VarianceG t k c d (n1 + 1) x
v)

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

-- DeviationHom -


-- | transormation between 'Deviation's.

type DeviationHom n = DiagramTrafo Discrete n N0

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

-- isExactVariance -


-- | testing of being exact, i.e. the 'deviations' are all 'ZeroPoint's.

isExactVariance ::
  ( Distributive x
  , NaturalConicBi (IsoO Dst Op) k Dst Projective d (Parallel LeftToRight) N2 N1
  , NaturalConicBi (IsoO Dst Op) c Dst Projective d (Parallel LeftToRight) N2 N1
  , Typeable t, Attestable n
  )
  => VarianceG t k c d n x -> Bool
isExactVariance :: forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x,
 NaturalConicBi
   (IsoO Dst Op) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConicBi
   (IsoO Dst Op) c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 Typeable t, Attestable n) =>
VarianceG t k c d n x -> Bool
isExactVariance VarianceG t k c d n x
v = Proxy (DeviationHom ('S n) x)
-> Point (DeviationHom ('S n) x) -> Bool
forall x (q :: * -> *). Distributive x => q x -> Point x -> Bool
isZeroPoint (VarianceG t k c d n x -> Proxy (DeviationHom (n + 1) x)
forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceG t k c d n x -> Proxy (DeviationHom (n + 1) x)
q VarianceG t k c d n x
v) (Point (DeviationHom ('S n) x) -> Bool)
-> Point (DeviationHom ('S n) x) -> Bool
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ VarianceG t k c d n x -> Deviation (n + 1) x
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Typeable t, Attestable n) =>
VarianceG t k c d n x -> Deviation (n + 1) x
deviations VarianceG t k c d n x
v where
  q :: VarianceG t k c d n x -> Proxy (DeviationHom (n+1) x)
  q :: forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceG t k c d n x -> Proxy (DeviationHom (n + 1) x)
q VarianceG t k c d n x
_ = Proxy (DeviationHom (n + 1) x)
Proxy (DeviationHom ('S n) x)
forall {k} (t :: k). Proxy t
Proxy

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

-- isExact -


-- | testing of being exact, i.e. the 'deviations' of its 'variance' are all 'ZeroPoint's.

isExact :: (Distributive x, Typeable t, Attestable n)
  => Kernels N1 x -> Cokernels N1 x -> ConsecutiveZero t n x -> Bool
isExact :: forall x (t :: Site) (n :: N').
(Distributive x, Typeable t, Attestable n) =>
Kernels N1 x -> Cokernels N1 x -> ConsecutiveZero t n x -> Bool
isExact Kernels N1 x
kers Cokernels N1 x
cokers = VarianceG t Cone Cone Diagram n x -> Bool
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (t :: Site) (n :: N').
(Distributive x,
 NaturalConicBi
   (IsoO Dst Op) k Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 NaturalConicBi
   (IsoO Dst Op) c Dst 'Projective d ('Parallel 'LeftToRight) N2 N1,
 Typeable t, Attestable n) =>
VarianceG t k c d n x -> Bool
isExactVariance (VarianceG t Cone Cone Diagram n x -> Bool)
-> (ConsecutiveZero t n x -> VarianceG t Cone Cone Diagram n x)
-> ConsecutiveZero t n x
-> Bool
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
. Kernels N1 x
-> Cokernels N1 x
-> ConsecutiveZero t n x
-> VarianceG t Cone Cone Diagram n x
forall x (t :: Site) (n :: N').
Distributive x =>
Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZero t n x -> Variance t n x
variance Kernels N1 x
kers Cokernels N1 x
cokers

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

-- dvZeroPoint -


-- | zero point for @'DeviationHom' __n x__@.

dvZeroPoint :: ZeroPoint x -> Any n -> ZeroPoint (DeviationHom n x)
dvZeroPoint :: forall x (n :: N').
ZeroPoint x -> Any n -> ZeroPoint (DeviationHom n x)
dvZeroPoint (ZeroPoint Point x
z) Any n
n = Point (DeviationHom n x) -> ZeroPoint (DeviationHom n x)
Diagram 'Discrete n N0 x -> ZeroPoint (DeviationHom n x)
forall x. Point x -> ZeroPoint x
ZeroPoint (Diagram 'Discrete n N0 x -> ZeroPoint (DeviationHom n x))
-> Diagram 'Discrete n N0 x -> ZeroPoint (DeviationHom n x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FinList n (Point x) -> Diagram 'Discrete n N0 x
forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete (FinList n (Point x) -> Diagram 'Discrete n N0 x)
-> FinList n (Point x) -> Diagram 'Discrete n N0 x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Any n -> Point x -> FinList n (Point x)
forall (n :: N') a. Any n -> a -> FinList n a
repeat Any n
n Point x
z 

-- | zero point for @'DeviationHom' __n x__@ according to the given proxy type.

dvZeroPoint' :: Attestable n => q n -> ZeroPoint x -> ZeroPoint (DeviationHom n x)
dvZeroPoint' :: forall (n :: N') (q :: N' -> *) x.
Attestable n =>
q n -> ZeroPoint x -> ZeroPoint (DeviationHom n x)
dvZeroPoint' q n
_ ZeroPoint x
z = ZeroPoint x -> Any n -> ZeroPoint (DeviationHom n x)
forall x (n :: N').
ZeroPoint x -> Any n -> ZeroPoint (DeviationHom n x)
dvZeroPoint ZeroPoint x
z Any n
forall (n :: N'). Attestable n => W n
attest

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

-- deviationHom -


-- | the induced homomorphism between 'Deviation's.

deviationHomTo ::
  ( Distributive x
  , NaturalKernelCokernel (IsoO Dst Op) k c d
  , Attestable n
  )
  => VarianceGHom To k c d n x -> DeviationHom (n+1) x
deviationHomTo :: forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Attestable n) =>
VarianceGHom 'To k c d n x -> DeviationHom (n + 1) x
deviationHomTo (VarianceGHom VarianceG 'To k c d n x
a VarianceG 'To k c d n x
b FinList (n + 3) x
fs) = Diagram 'Discrete ('S n) N0 x
-> Diagram 'Discrete ('S n) N0 x
-> FinList ('S n) x
-> DiagramTrafo 'Discrete ('S n) N0 x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a
-> Diagram t n m a -> FinList n a -> DiagramTrafo t n m a
DiagramTrafo Deviation (n + 1) x
Diagram 'Discrete ('S n) N0 x
a' Deviation (n + 1) x
Diagram 'Discrete ('S n) N0 x
b' FinList (n + 1) x
FinList ('S n) x
fs' where
  a' :: Deviation (n + 1) x
a'  = VarianceG 'To k c d n x -> Deviation (n + 1) x
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Typeable t, Attestable n) =>
VarianceG t k c d n x -> Deviation (n + 1) x
deviations VarianceG 'To k c d n x
a
  b' :: Deviation (n + 1) x
b'  = VarianceG 'To k c d n x -> Deviation (n + 1) x
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Typeable t, Attestable n) =>
VarianceG t k c d n x -> Deviation (n + 1) x
deviations VarianceG 'To k c d n x
b
  fs' :: FinList (n + 1) x
fs' = VarianceG 'To k c d n x
-> VarianceG 'To k c d n x
-> FinList (n + 3) x
-> FinList (n + 1) x
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, Conic k, Conic c) =>
VarianceG 'To k c d n x
-> VarianceG 'To k c d n x
-> FinList (n + 3) x
-> FinList (n + 1) x
trfs VarianceG 'To k c d n x
a VarianceG 'To k c d n x
b FinList (n + 3) x
fs

  trf ::
    ( Distributive x
    , Conic k, Conic c
    )
    => VarianceG To k c d n x -> VarianceG To k c d n x -> x -> x
  trf :: forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, Conic k, Conic c) =>
VarianceG 'To k c d n x -> VarianceG 'To k c d n x -> x -> x
trf VarianceG 'To k c d n x
a VarianceG 'To k c d n x
b x
f = x
f'' where
    VarianceG (ConsecutiveZero (DiagramChainTo Point x
_ FinList (n + 2) x
_)) ((KernelG k d N1 x
aKer,CokernelG c d N1 x
aCoker):|FinList n1 (KernelG k d N1 x, CokernelG c d N1 x)
_) = VarianceG 'To k c d n x
a
    VarianceG (ConsecutiveZero (DiagramChainTo Point x
_ FinList (n + 2) x
_)) ((KernelG k d N1 x
bKer,CokernelG c d N1 x
bCoker):|FinList n1 (KernelG k d N1 x, CokernelG c d N1 x)
_) = VarianceG 'To k c d n x
b

    f' :: x
f' = KernelG k d N1 x
-> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 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 KernelG k d N1 x
bKer (d ('Parallel 'LeftToRight) N2 N1 x
-> x -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 N1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel (KernelG k d N1 x -> d ('Parallel 'LeftToRight) N2 N1 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 x -> d t n m x
universalDiagram KernelG k d N1 x
bKer) (x
fx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
ak)) where
      ak :: x
ak = KernelConic k d N1 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Conic c =>
KernelConic c d n x -> x
kernelFactor (KernelG k d N1 x -> KernelConic k d N1 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 KernelG k d N1 x
aKer)
    f'' :: x
f'' = CokernelG c d N1 x
-> Cone Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 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 CokernelG c d N1 x
aCoker (d ('Parallel 'RightToLeft) N2 N1 x
-> x -> Cone Dst 'Injective d ('Parallel 'RightToLeft) N2 N1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) N2 m a
ConeCokernel (CokernelG c d N1 x -> d ('Parallel 'RightToLeft) N2 N1 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 x -> d t n m x
universalDiagram CokernelG c d N1 x
aCoker) (x
bcx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
f')) where
      bc :: x
bc = CokernelConic c d N1 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Conic c =>
CokernelConic c d n x -> x
cokernelFactor (CokernelG c d N1 x -> CokernelConic c d N1 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 CokernelG c d N1 x
bCoker)

  trfs :: 
    ( Distributive x
    , Conic k, Conic c
    )
    => VarianceG To k c d n x -> VarianceG To k c d n x -> FinList (n+3) x -> FinList (n+1) x
  trfs :: forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, Conic k, Conic c) =>
VarianceG 'To k c d n x
-> VarianceG 'To k c d n x
-> FinList (n + 3) x
-> FinList (n + 1) x
trfs VarianceG 'To k c d n x
a VarianceG 'To k c d n x
b (x
_:|x
f:|FinList n1 x
fs) = VarianceG 'To k c d n x -> VarianceG 'To k c d n x -> x -> x
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, Conic k, Conic c) =>
VarianceG 'To k c d n x -> VarianceG 'To k c d n x -> x -> x
trf VarianceG 'To k c d n x
a VarianceG 'To k c d n x
b x
f x -> FinList n x -> FinList (n + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| case VarianceG 'To k c d n x
a of
    VarianceG ConsecutiveZero 'To n x
_ ((KernelG k d N1 x, CokernelG c d N1 x)
_:|FinList n1 (KernelG k d N1 x, CokernelG c d N1 x)
Nil)  -> FinList n x
FinList N0 x
forall a. FinList N0 a
Nil
    VarianceG ConsecutiveZero 'To n x
_ ((KernelG k d N1 x, CokernelG c d N1 x)
_:|(KernelG k d N1 x, CokernelG c d N1 x)
_:|FinList n1 (KernelG k d N1 x, CokernelG c d N1 x)
_) -> VarianceG 'To k c d n1 x
-> VarianceG 'To k c d n1 x
-> FinList (n1 + 3) x
-> FinList (n1 + 1) x
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, Conic k, Conic c) =>
VarianceG 'To k c d n x
-> VarianceG 'To k c d n x
-> FinList (n + 3) x
-> FinList (n + 1) x
trfs (VarianceG 'To k c d (n1 + 1) x -> VarianceG 'To k c d n1 x
forall x (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
Distributive x =>
VarianceG t k c d (n + 1) x -> VarianceG t k c d n x
vrcTail VarianceG 'To k c d n x
VarianceG 'To k c d (n1 + 1) x
a) (VarianceG 'To k c d (n1 + 1) x -> VarianceG 'To k c d n1 x
forall x (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
Distributive x =>
VarianceG t k c d (n + 1) x -> VarianceG t k c d n x
vrcTail VarianceG 'To k c d n x
VarianceG 'To k c d (n1 + 1) x
b) (x
fx -> FinList n1 x -> FinList (n1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList n1 x
fs)

-- | the induced homomorphism between 'Deviation's.

deviationHom ::
  ( Distributive x
  , NaturalKernelCokernel (IsoO Dst Op) k c d
  , Attestable n
  )
  => VarianceGHom t k c d n x -> DeviationHom (n+1) x
deviationHom :: forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (t :: Site).
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Attestable n) =>
VarianceGHom t k c d n x -> DeviationHom (n + 1) x
deviationHom VarianceGHom t k c d n x
h = case VarianceGHom t k c d n x -> Either (t :~: 'From) (t :~: 'To)
forall (t :: Site)
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
VarianceGHom t k c d n x -> Either (t :~: 'From) (t :~: 'To)
vrcHomSite VarianceGHom t k c d n x
h of
  Right t :~: 'To
Refl -> VarianceGHom 'To k c d n x -> DeviationHom (n + 1) x
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Attestable n) =>
VarianceGHom 'To k c d n x -> DeviationHom (n + 1) x
deviationHomTo VarianceGHom t k c d n x
VarianceGHom 'To k c d n x
h
  Left t :~: 'From
Refl  -> DeviationHom (n + 1) x
DiagramTrafo 'Discrete ('S n) N0 x
dh where
    Contravariant2 IsoO Dst Op x (Op x)
i = Variant2 'Contravariant (IsoO Dst Op) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst

    SDualBi (Left1 Dual1 (VarianceGHom 'From k c d n) (Op x)
hOp) = IsoO Dst Op x (Op x)
-> SDualBi (VarianceGHom 'From k c d n) x
-> SDualBi (VarianceGHom 'From k c d n) (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Dst Op x (Op x)
i (Either1 (Dual1 (VarianceGHom t k c d n)) (VarianceGHom t k c d n) x
-> SDualBi (VarianceGHom t k c d n) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (VarianceGHom t k c d n x
-> Either1 (VarianceGHom 'To c k d n) (VarianceGHom t k c d n) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 VarianceGHom t k c d n x
h))
    dhOp :: DeviationHom (n + 1) (Op x)
dhOp                = VarianceGHom 'To c k d n (Op x) -> DeviationHom (n + 1) (Op x)
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (t :: Site).
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Attestable n) =>
VarianceGHom t k c d n x -> DeviationHom (n + 1) x
deviationHom Dual1 (VarianceGHom 'From k c d n) (Op x)
VarianceGHom 'To c k d n (Op x)
hOp
    SDualBi (Right1 DiagramTrafo 'Discrete ('S n) N0 x
dh) = Inv2 (HomDisjEmpty Dst Op) (Op x) x
-> SDualBi (DiagramTrafo 'Discrete ('S n) N0) (Op x)
-> SDualBi (DiagramTrafo 'Discrete ('S n) N0) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Dst Op x (Op x) -> Inv2 (HomDisjEmpty Dst Op) (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Dst Op x (Op x)
i) (Either1
  (Dual1 (DiagramTrafo 'Discrete ('S n) N0))
  (DiagramTrafo 'Discrete ('S n) N0)
  (Op x)
-> SDualBi (DiagramTrafo 'Discrete ('S n) N0) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Dual1 (DiagramTrafo 'Discrete ('S n) N0) (Op x)
-> Either1
     (Dual1 (DiagramTrafo 'Discrete ('S n) N0))
     (DiagramTrafo 'Discrete ('S n) N0)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Dual1 (DiagramTrafo 'Discrete ('S n) N0) (Op x)
DeviationHom (n + 1) (Op x)
dhOp))

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

-- prpDeviation -


-- | validity of some properties for @__d__ ~ 'Orientation' 'Symbol'@.

prpDeviationOrntSymbol :: Statement
prpDeviationOrntSymbol :: Statement
prpDeviationOrntSymbol = String -> Label
Prp String
"Deviation" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ X (SomeConsecutiveZeroHom OS)
-> (SomeConsecutiveZeroHom OS -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (N -> X (SomeConsecutiveZeroHom OS)
xSomeConsecutiveZeroHomOrnt N
20)
          (\(SomeConsecutiveZeroHom ConsecutiveZeroHom t n OS
t)
           -> DeviationHom ('S n) OS -> Statement
forall a. Validable a => a -> Statement
valid (VarianceGHom t Cone Cone Diagram n OS -> DeviationHom (n + 1) OS
VarianceGHom t Cone Cone Diagram n OS -> DeviationHom ('S n) OS
forall x
       (k :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') (t :: Site).
(Distributive x, NaturalKernelCokernel (IsoO Dst Op) k c d,
 Attestable n) =>
VarianceGHom t k c d n x -> DeviationHom (n + 1) x
deviationHom (VarianceGHom t Cone Cone Diagram n OS -> DeviationHom ('S n) OS)
-> VarianceGHom t Cone Cone Diagram n OS -> DeviationHom ('S n) OS
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Kernels N1 OS
-> Cokernels N1 OS
-> ConsecutiveZeroHom t n OS
-> VarianceGHom t Cone Cone Diagram n OS
forall x (t :: Site) (n :: N').
(Distributive x, Typeable t, Attestable n) =>
Kernels N1 x
-> Cokernels N1 x -> ConsecutiveZeroHom t n x -> VarianceHom t n x
varianceHom Kernels N1 OS
forall {n :: N'}. Kernels n OS
kers Cokernels N1 OS
forall {n :: N'}. Cokernels n OS
cokers ConsecutiveZeroHom t n OS
t)
          )
      ]
  where kers :: Kernels n OS
kers   = Symbol -> Kernels n OS
forall p (n :: N'). Entity p => p -> Kernels n (Orientation p)
kernelsOrnt Symbol
X
        cokers :: Cokernels n OS
cokers = Symbol -> Cokernels n OS
forall p (n :: N'). Entity p => p -> Cokernels n (Orientation p)
cokernelsOrnt Symbol
Y