{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Exact.Free

-- Description : deviation for free chains.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- deviation for free chains.

module OAlg.Limes.Exact.Free
  (
    -- * Variance

    varianceFreeTo, VarianceFreeLiftable
    
    -- * Free Consecutive Zero

  , ConsecutiveZeroFree(..)
  
    -- ** Duality

  , cnzFreeMapS, cnzFreeMapCov, cnzFreeMapCnt
  
    -- * Proposition

  , prpConsecutiveZeroFree
  ) where

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Variant

import OAlg.Structure.Oriented
import OAlg.Structure.Distributive

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

import OAlg.Entity.Slice

import OAlg.Hom.Oriented
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.Deviation


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

-- ConsecutiveZeroFree -


-- | consecutive zero chain, where the tail of the points are free.

--

-- __Property__ Let @'ConsecutiveZeroFree' c fs@ be in @'ConsecutiveZeroFree' __t n x__@, then holds:

--

-- (1) @'sfrPoint' f '==' p@ for all @(f,p)@ in @fs '`zip`' 'tail' ('cnzPoints' c)@.

data ConsecutiveZeroFree t n x where
  ConsecutiveZeroFree
    :: ConsecutiveZero t n x
    -> FinList (n+2) (SomeFree x)
    -> ConsecutiveZeroFree t n x

deriving instance (Show x, ShowPoint x) => Show (ConsecutiveZeroFree t n x)
deriving instance (Eq x, EqPoint x) => Eq (ConsecutiveZeroFree t n x)

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

-- prpConsecutiveZeroFree -


relConsecutiveZeroFree :: Distributive x => ConsecutiveZeroFree t n x -> Statement
relConsecutiveZeroFree :: forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZeroFree t n x -> Statement
relConsecutiveZeroFree (ConsecutiveZeroFree ConsecutiveZero t n x
c FinList (n + 2) (SomeFree x)
fs)
  = [Statement] -> Statement
And [ ConsecutiveZero t n x -> Statement
forall a. Validable a => a -> Statement
valid ConsecutiveZero t n x
c
        , FinList ('S ('S n)) (SomeFree x) -> Statement
forall a. Validable a => a -> Statement
valid FinList (n + 2) (SomeFree x)
FinList ('S ('S n)) (SomeFree x)
fs
        , String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: N
-> FinList ('S ('S n)) (SomeFree x)
-> FinList ('S ('S n)) (Point x)
-> Statement
forall x (n :: N').
Distributive x =>
N -> FinList n (SomeFree x) -> FinList n (Point x) -> Statement
vld N
1 FinList (n + 2) (SomeFree x)
FinList ('S ('S n)) (SomeFree x)
fs (FinList ('S ('S n) + 1) (Point x) -> FinList ('S ('S n)) (Point x)
FinList ('S ('S ('S n))) (Point x) -> FinList ('S ('S n)) (Point x)
forall (n :: N') a. FinList (n + 1) a -> FinList n a
tail (FinList ('S ('S ('S n))) (Point x)
 -> FinList ('S ('S n)) (Point x))
-> FinList ('S ('S ('S n))) (Point x)
-> FinList ('S ('S n)) (Point x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ConsecutiveZero t n x -> FinList (n + 3) (Point x)
forall x (t :: Site) (n :: N').
Oriented x =>
ConsecutiveZero t n x -> FinList (n + 3) (Point x)
cnzPoints ConsecutiveZero t n x
c)
        ]
  where

    vld :: Distributive x => N -> FinList n (SomeFree x) -> FinList n (Point x) -> Statement
    vld :: forall x (n :: N').
Distributive x =>
N -> FinList n (SomeFree x) -> FinList n (Point x) -> Statement
vld N
_ FinList n (SomeFree x)
Nil FinList n (Point x)
_ = Statement
SValid
    vld N
i (SomeFree x
f:|FinList n1 (SomeFree x)
fs) (Point x
p:|FinList n1 (Point x)
ps)
      = [Statement] -> Statement
And [ (SomeFree x -> Point x
forall x. SomeFree x -> Point x
sfrPoint SomeFree x
f Point x -> Point x -> Bool
forall a. Eq a => a -> a -> Bool
== Point x
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
i, String
"f"String -> String -> Parameter
:=SomeFree x -> String
forall a. Show a => a -> String
show SomeFree x
f, String
"p"String -> String -> Parameter
:=Point x -> String
forall a. Show a => a -> String
show Point x
p]
            , N -> FinList n1 (SomeFree x) -> FinList n1 (Point x) -> Statement
forall x (n :: N').
Distributive x =>
N -> FinList n (SomeFree x) -> FinList n (Point x) -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) FinList n1 (SomeFree x)
fs FinList n1 (Point x)
FinList n1 (Point x)
ps
            ]

-- | validity according to 'ConsecutiveZeroFree'.

prpConsecutiveZeroFree :: Distributive x => ConsecutiveZeroFree t n x -> Statement
prpConsecutiveZeroFree :: forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZeroFree t n x -> Statement
prpConsecutiveZeroFree ConsecutiveZeroFree t n x
cf = String -> Label
Prp String
"ConsecutiveZeroFree" Label -> Statement -> Statement
:<=>: ConsecutiveZeroFree t n x -> Statement
forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZeroFree t n x -> Statement
relConsecutiveZeroFree ConsecutiveZeroFree t n x
cf
 
instance Distributive x => Validable (ConsecutiveZeroFree t n x) where
  valid :: ConsecutiveZeroFree t n x -> Statement
valid = ConsecutiveZeroFree t n x -> Statement
forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZeroFree t n x -> Statement
prpConsecutiveZeroFree
  
--------------------------------------------------------------------------------

-- cnzFreeMapCov -


-- | covairaint mapping of 'ConsecutiveZeroFree'.

cnzFreeMapCov ::
  ( HomDistributiveDisjunctive h
  , HomOrientedSlicedFree h
  )
  => Variant2 Covariant h x y -> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree t n y
cnzFreeMapCov :: forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, HomOrientedSlicedFree h) =>
Variant2 'Covariant h x y
-> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree t n y
cnzFreeMapCov Variant2 'Covariant h x y
h (ConsecutiveZeroFree ConsecutiveZero t n x
c FinList (n + 2) (SomeFree x)
fs) = ConsecutiveZero t n y
-> FinList (n + 2) (SomeFree y) -> ConsecutiveZeroFree t n y
forall (t :: Site) (n :: N') x.
ConsecutiveZero t n x
-> FinList (n + 2) (SomeFree x) -> ConsecutiveZeroFree t n x
ConsecutiveZeroFree ConsecutiveZero t n y
c' FinList (n + 2) (SomeFree y)
FinList ('S ('S n)) (SomeFree y)
fs' where
  c' :: ConsecutiveZero t n y
c'  = Variant2 'Covariant 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 h x y
h ConsecutiveZero t n x
c
  fs' :: FinList ('S ('S n)) (SomeFree y)
fs' = (SomeFree x -> SomeFree y)
-> FinList ('S ('S n)) (SomeFree x)
-> FinList ('S ('S n)) (SomeFree y)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Variant2 'Covariant h x y -> SomeFree x -> SomeFree y
forall (h :: * -> * -> *) (v :: Variant) x y.
HomOrientedSlicedFree h =>
Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMap Variant2 'Covariant h x y
h) FinList (n + 2) (SomeFree x)
FinList ('S ('S n)) (SomeFree x)
fs
  
--------------------------------------------------------------------------------

-- cnzFreeMapCnt -


-- | contravaraint mapping of 'ConsecutiveZeroFree'.

cnzFreeMapCnt ::
  ( HomDistributiveDisjunctive h
  , HomOrientedSlicedFree h
  )
  => Variant2 Contravariant h x y -> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree (Dual t) n y
cnzFreeMapCnt :: forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, HomOrientedSlicedFree h) =>
Variant2 'Contravariant h x y
-> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree (Dual t) n y
cnzFreeMapCnt Variant2 'Contravariant h x y
h (ConsecutiveZeroFree ConsecutiveZero t n x
c FinList (n + 2) (SomeFree x)
fs) = ConsecutiveZero (Dual t) n y
-> FinList (n + 2) (SomeFree y) -> ConsecutiveZeroFree (Dual t) n y
forall (t :: Site) (n :: N') x.
ConsecutiveZero t n x
-> FinList (n + 2) (SomeFree x) -> ConsecutiveZeroFree t n x
ConsecutiveZeroFree ConsecutiveZero (Dual t) n y
c' FinList (n + 2) (SomeFree y)
FinList ('S ('S n)) (SomeFree y)
fs' where
  c' :: ConsecutiveZero (Dual t) n y
c'  = Variant2 'Contravariant 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 h x y
h ConsecutiveZero t n x
c
  fs' :: FinList ('S ('S n)) (SomeFree y)
fs' = (SomeFree x -> SomeFree y)
-> FinList ('S ('S n)) (SomeFree x)
-> FinList ('S ('S n)) (SomeFree y)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Variant2 'Contravariant h x y -> SomeFree x -> SomeFree y
forall (h :: * -> * -> *) (v :: Variant) x y.
HomOrientedSlicedFree h =>
Variant2 v h x y -> SomeFree x -> SomeFree y
sfrMap Variant2 'Contravariant h x y
h) FinList (n + 2) (SomeFree x)
FinList ('S ('S n)) (SomeFree x)
fs

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

-- Duality -


type instance Dual1 (ConsecutiveZeroFree t n) = ConsecutiveZeroFree (Dual t) n

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

-- cnzFreeMapS -


-- | mapping of 'ConsecutiveZeroFree'.

cnzFreeMapS ::
  ( HomDistributiveDisjunctive h
  , HomOrientedSlicedFree h
  , t ~ Dual (Dual t)
  )
  => h x y -> SDualBi (ConsecutiveZeroFree t n) x -> SDualBi (ConsecutiveZeroFree t n ) y
cnzFreeMapS :: forall (h :: * -> * -> *) (t :: Site) x y (n :: N').
(HomDistributiveDisjunctive h, HomOrientedSlicedFree h,
 t ~ Dual (Dual t)) =>
h x y
-> SDualBi (ConsecutiveZeroFree t n) x
-> SDualBi (ConsecutiveZeroFree t n) y
cnzFreeMapS = (Variant2 'Covariant h x y
 -> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree t n y)
-> (Variant2 'Covariant h x y
    -> Dual1 (ConsecutiveZeroFree t n) x
    -> Dual1 (ConsecutiveZeroFree t n) y)
-> (Variant2 'Contravariant h x y
    -> ConsecutiveZeroFree t n x -> Dual1 (ConsecutiveZeroFree t n) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (ConsecutiveZeroFree t n) x -> ConsecutiveZeroFree t n y)
-> h x y
-> SDualBi (ConsecutiveZeroFree t n) x
-> SDualBi (ConsecutiveZeroFree t 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 h x y
-> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree t n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, HomOrientedSlicedFree h) =>
Variant2 'Covariant h x y
-> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree t n y
cnzFreeMapCov Variant2 'Covariant h x y
-> Dual1 (ConsecutiveZeroFree t n) x
-> Dual1 (ConsecutiveZeroFree t n) y
Variant2 'Covariant h x y
-> ConsecutiveZeroFree (Dual t) n x
-> ConsecutiveZeroFree (Dual t) n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, HomOrientedSlicedFree h) =>
Variant2 'Covariant h x y
-> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree t n y
cnzFreeMapCov Variant2 'Contravariant h x y
-> ConsecutiveZeroFree t n x -> Dual1 (ConsecutiveZeroFree t n) y
Variant2 'Contravariant h x y
-> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree (Dual t) n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, HomOrientedSlicedFree h) =>
Variant2 'Contravariant h x y
-> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree (Dual t) n y
cnzFreeMapCnt Variant2 'Contravariant h x y
-> Dual1 (ConsecutiveZeroFree t n) x -> ConsecutiveZeroFree t n y
Variant2 'Contravariant h x y
-> ConsecutiveZeroFree (Dual t) n x
-> ConsecutiveZeroFree (Dual (Dual t)) n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
(HomDistributiveDisjunctive h, HomOrientedSlicedFree h) =>
Variant2 'Contravariant h x y
-> ConsecutiveZeroFree t n x -> ConsecutiveZeroFree (Dual t) n y
cnzFreeMapCnt

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

-- FunctorialG -


instance
  ( HomDistributiveDisjunctive h
  , HomOrientedSlicedFree h
  , t ~ Dual (Dual t)
  )
  => ApplicativeG (SDualBi (ConsecutiveZeroFree t n)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (ConsecutiveZeroFree t n) x
   -> SDualBi (ConsecutiveZeroFree t n) y
amapG = h x y
-> SDualBi (ConsecutiveZeroFree t n) x
-> SDualBi (ConsecutiveZeroFree t n) y
forall (h :: * -> * -> *) (t :: Site) x y (n :: N').
(HomDistributiveDisjunctive h, HomOrientedSlicedFree h,
 t ~ Dual (Dual t)) =>
h x y
-> SDualBi (ConsecutiveZeroFree t n) x
-> SDualBi (ConsecutiveZeroFree t n) y
cnzFreeMapS

instance
  ( HomDistributiveDisjunctive h
  , FunctorialOriented h
  , HomOrientedSlicedFree h
  , t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (ConsecutiveZeroFree t n)) h (->)

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

-- VarianceFreeLiftable -


-- | variance according to the conic objects @'ConicFreeTip' 'Cone'@, 'ConeLiftable' over the

-- diagrammatic object 'SomeFreeSliceDiagram'.

type VarianceFreeLiftable t = VarianceG t (ConicFreeTip Cone) ConeLiftable SomeFreeSliceDiagram

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

-- varianceFreeTo -


-- | variance according to 'KernelsSomeFreeFreeTip' and 'CokernelsLiftableSomeFree'. 

varianceFreeTo :: Distributive x
  => KernelsSomeFreeFreeTip x
  -> CokernelsLiftableSomeFree x
  -> ConsecutiveZeroFree To n x -> VarianceFreeLiftable To n x
varianceFreeTo :: forall x (n :: N').
Distributive x =>
KernelsSomeFreeFreeTip x
-> CokernelsLiftableSomeFree x
-> ConsecutiveZeroFree 'To n x
-> VarianceFreeLiftable 'To n x
varianceFreeTo KernelsSomeFreeFreeTip x
kers CokernelsLiftableSomeFree x
cokers (ConsecutiveZeroFree ConsecutiveZero 'To n x
c FinList (n + 2) (SomeFree x)
fs) = ConsecutiveZero 'To n x
-> FinList
     (n + 1)
     (KernelG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x,
      CokernelG ConeLiftable SomeFreeSliceDiagram N1 x)
-> VarianceG
     'To (ConicFreeTip Cone) ConeLiftable SomeFreeSliceDiagram 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 (KernelsSomeFreeFreeTip x
-> CokernelsLiftableSomeFree x
-> ConsecutiveZero 'To n x
-> FinList (n + 2) (SomeFree x)
-> FinList
     (n + 1)
     (KernelG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x,
      CokernelG ConeLiftable SomeFreeSliceDiagram N1 x)
forall x (n :: N').
Distributive x =>
KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
-> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
-> ConsecutiveZero 'To n x
-> FinList (n + 2) (SomeFree x)
-> FinList
     (n + 1) (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
kcs KernelsSomeFreeFreeTip x
kers CokernelsLiftableSomeFree x
cokers ConsecutiveZero 'To n x
c FinList (n + 2) (SomeFree x)
fs) where

  kc :: Distributive x
    => KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
    -> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
    -> ConsecutiveZero To n x -> SomeFree x
    -> (KernelSomeFreeFreeTip x,CokernelLiftableSomeFree x)
  kc :: forall x (n :: N').
Distributive x =>
KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
-> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
-> ConsecutiveZero 'To n x
-> SomeFree x
-> (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
kc KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
kers CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
cokers (ConsecutiveZero (DiagramChainTo Point x
_ (x
v:|x
w:|FinList n1 x
_))) (SomeFree Free k x
f) = (LimesG
  (ConicFreeTip Cone)
  Dst
  'Projective
  SomeFreeSliceDiagram
  ('Parallel 'LeftToRight)
  N2
  N1
  x
k,CokernelLiftableSomeFree x
c) where
    k :: LimesG
  (ConicFreeTip Cone)
  Dst
  'Projective
  SomeFreeSliceDiagram
  ('Parallel 'LeftToRight)
  N2
  N1
  x
k  = KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
-> SomeFreeSliceDiagram ('Parallel 'LeftToRight) N2 N1 x
-> LimesG
     (ConicFreeTip Cone)
     Dst
     'Projective
     SomeFreeSliceDiagram
     ('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 KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
kers (Slice 'From (Free k) x
-> SomeFreeSliceDiagram ('Parallel 'LeftToRight) N2 N1 x
forall (k :: N') x.
(Attestable k, Sliced (Free k) x) =>
Slice 'From (Free k) x
-> SomeFreeSliceDiagram ('Parallel 'LeftToRight) N2 N1 x
SomeFreeSliceKernel (Free k x -> x -> Slice 'From (Free k) x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom Free k x
f x
v))
    w' :: x
w' = LimesG
  (ConicFreeTip Cone)
  Dst
  'Projective
  SomeFreeSliceDiagram
  ('Parallel 'LeftToRight)
  N2
  N1
  x
-> Cone
     Dst
     'Projective
     SomeFreeSliceDiagram
     ('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
  (ConicFreeTip Cone)
  Dst
  'Projective
  SomeFreeSliceDiagram
  ('Parallel 'LeftToRight)
  N2
  N1
  x
k (SomeFreeSliceDiagram ('Parallel 'LeftToRight) N2 N1 x
-> x
-> Cone
     Dst
     'Projective
     SomeFreeSliceDiagram
     ('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
  (ConicFreeTip Cone)
  Dst
  'Projective
  SomeFreeSliceDiagram
  ('Parallel 'LeftToRight)
  N2
  N1
  x
-> SomeFreeSliceDiagram ('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
  (ConicFreeTip Cone)
  Dst
  'Projective
  SomeFreeSliceDiagram
  ('Parallel 'LeftToRight)
  N2
  N1
  x
k) x
w)
    c :: CokernelLiftableSomeFree x
c  = case LimesG
  (ConicFreeTip Cone)
  Dst
  'Projective
  SomeFreeSliceDiagram
  ('Parallel 'LeftToRight)
  N2
  N1
  x
-> ConicFreeTip
     Cone
     Dst
     'Projective
     SomeFreeSliceDiagram
     ('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.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG
  (ConicFreeTip Cone)
  Dst
  'Projective
  SomeFreeSliceDiagram
  ('Parallel 'LeftToRight)
  N2
  N1
  x
k of
      ConicFreeTip Free k x
f' Cone
  Dst
  'Projective
  SomeFreeSliceDiagram
  ('Parallel 'LeftToRight)
  N2
  N1
  x
_ -> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
-> SomeFreeSliceDiagram ('Parallel 'RightToLeft) N2 N1 x
-> CokernelLiftableSomeFree 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 CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
cokers (Slice 'To (Free k) x
-> SomeFreeSliceDiagram ('Parallel 'RightToLeft) N2 N1 x
forall (k :: N') x.
(Attestable k, Sliced (Free k) x) =>
Slice 'To (Free k) x
-> SomeFreeSliceDiagram ('Parallel 'RightToLeft) N2 N1 x
SomeFreeSliceCokernel (Free k x -> x -> Slice 'To (Free k) x
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo Free k x
f' x
w'))

  kcs :: Distributive x
    => KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
    -> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
    -> ConsecutiveZero To n x -> FinList (n+2) (SomeFree x)
    -> FinList (n+1) (KernelSomeFreeFreeTip x,CokernelLiftableSomeFree x)
  kcs :: forall x (n :: N').
Distributive x =>
KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
-> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
-> ConsecutiveZero 'To n x
-> FinList (n + 2) (SomeFree x)
-> FinList
     (n + 1) (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
kcs KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
kers CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
cokers ConsecutiveZero 'To n x
c (SomeFree x
f:|FinList n1 (SomeFree x)
fs) = KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
-> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
-> ConsecutiveZero 'To n x
-> SomeFree x
-> (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
forall x (n :: N').
Distributive x =>
KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
-> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
-> ConsecutiveZero 'To n x
-> SomeFree x
-> (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
kc KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
kers CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
cokers ConsecutiveZero 'To n x
c SomeFree x
f (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
-> FinList n (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
-> FinList
     (n + 1) (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:| case FinList n1 (SomeFree x)
fs of
    SomeFree x
_ :| FinList n1 (SomeFree x)
Nil    -> FinList n (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
FinList 'N0 (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
forall a. FinList 'N0 a
Nil
    SomeFree x
_ :| SomeFree x
_ :| FinList n1 (SomeFree x)
_ -> KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
-> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
-> ConsecutiveZero 'To n1 x
-> FinList (n1 + 2) (SomeFree x)
-> FinList
     (n1 + 1) (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
forall x (n :: N').
Distributive x =>
KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
-> CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
-> ConsecutiveZero 'To n x
-> FinList (n + 2) (SomeFree x)
-> FinList
     (n + 1) (KernelSomeFreeFreeTip x, CokernelLiftableSomeFree x)
kcs KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 x
kers CokernelsG ConeLiftable SomeFreeSliceDiagram N1 x
cokers (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) FinList n1 (SomeFree x)
FinList (n1 + 2) (SomeFree x)
fs