{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Exact.ConsecutiveZero

-- Description : chain diagrams with consecutive zero arrows. 

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- chain diagrams with consecutive zero arrows. 

module OAlg.Limes.Exact.ConsecutiveZero
  (
    -- * Consecutive Zero

    ConsecutiveZero(..), cnzSite
  , cnzDiagram, cnzPoints, cnzArrows
  , cnzHead, cnzTail

    -- ** Duality

  , cnzMapS, cnzMapCov, cnzMapCnt

    -- * Consecutive Zero Hom

  , ConsecutiveZeroHom(..), cnzHomSite, cnzHomArrows
  , cnzHomHead, cnzHomTail

    -- ** Duality

  , cnzHomMapS, cnzHomMapCov, cnzHomMapCnt 

    -- * X

  , xSomeConsecutiveZeroHomOrnt, SomeConsecutiveZeroHom(..)

  ) where

import Control.Monad
import Control.Applicative ((<|>))

import Data.Typeable

import OAlg.Prelude

import OAlg.Category.SDuality

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

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive
import OAlg.Structure.Distributive
import OAlg.Structure.Vectorial
import OAlg.Structure.Algebraic

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

import OAlg.Hom.Oriented
import OAlg.Hom.Distributive

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

-- ConsecutiveZero -


-- | chain diagrams with consecutive zero arrows.

--

-- __Properties__ Let @'ConsecutiveZero' c@ be in @'ConsecutiveZero' __t n x__@

-- for a  'Distributive' structure @__x__@, then holds:

--

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

-- @d 'OAlg.Structure.Multiplicative.*' d'@ is 'zero' for all @..d':|'d'..@ in @ds@.

--

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

-- @d' 'OAlg.Structure.Multiplicative.*' d@ is 'zero' for all @..d':|'d'..@ in @ds@.

newtype ConsecutiveZero t n x = ConsecutiveZero (Diagram (Chain t) (n+3) (n+2) x)
  deriving (Int -> ConsecutiveZero t n x -> ShowS
[ConsecutiveZero t n x] -> ShowS
ConsecutiveZero t n x -> String
(Int -> ConsecutiveZero t n x -> ShowS)
-> (ConsecutiveZero t n x -> String)
-> ([ConsecutiveZero t n x] -> ShowS)
-> Show (ConsecutiveZero t n x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
Int -> ConsecutiveZero t n x -> ShowS
forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
[ConsecutiveZero t n x] -> ShowS
forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
ConsecutiveZero t n x -> String
$cshowsPrec :: forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
Int -> ConsecutiveZero t n x -> ShowS
showsPrec :: Int -> ConsecutiveZero t n x -> ShowS
$cshow :: forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
ConsecutiveZero t n x -> String
show :: ConsecutiveZero t n x -> String
$cshowList :: forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
[ConsecutiveZero t n x] -> ShowS
showList :: [ConsecutiveZero t n x] -> ShowS
Show,ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool
(ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool)
-> (ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool)
-> Eq (ConsecutiveZero t n x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: Site) (n :: N') x.
(EqPoint x, Eq x) =>
ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool
$c== :: forall (t :: Site) (n :: N') x.
(EqPoint x, Eq x) =>
ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool
== :: ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool
$c/= :: forall (t :: Site) (n :: N') x.
(EqPoint x, Eq x) =>
ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool
/= :: ConsecutiveZero t n x -> ConsecutiveZero t n x -> Bool
Eq)

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

-- cnzSite -


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

cnzSite :: ConsecutiveZero t n x -> Either (t :~: From) (t :~: To)
cnzSite :: forall (t :: Site) (n :: N') x.
ConsecutiveZero t n x -> Either (t :~: 'From) (t :~: 'To)
cnzSite (ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
d) = case Diagram ('Chain t) (n + 3) (n + 2) x
d of
  DiagramChainFrom Point x
_ FinList (n + 2) x
_ -> (t :~: 'From) -> Either (t :~: 'From) (t :~: 'To)
forall a b. a -> Either a b
Left t :~: t
t :~: 'From
forall {k} (a :: k). a :~: a
Refl
  DiagramChainTo Point x
_ FinList (n + 2) x
_   -> (t :~: 'To) -> Either (t :~: 'From) (t :~: 'To)
forall a b. b -> Either a b
Right t :~: t
t :~: 'To
forall {k} (a :: k). a :~: a
Refl
  
--------------------------------------------------------------------------------

-- cnzDiagram -


-- | the underlying chain diagram.

cnzDiagram :: ConsecutiveZero t n x -> Diagram (Chain t) (n+3) (n+2) x
cnzDiagram :: forall (t :: Site) (n :: N') x.
ConsecutiveZero t n x -> Diagram ('Chain t) (n + 3) (n + 2) x
cnzDiagram (ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
c) = Diagram ('Chain t) (n + 3) (n + 2) x
c

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

-- cnzArrows -


-- | the arrows according to its underlying diagram.

cnzArrows :: ConsecutiveZero t n x -> FinList (n+2) x
cnzArrows :: forall (t :: Site) (n :: N') x.
ConsecutiveZero t n x -> FinList (n + 2) x
cnzArrows = Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> FinList ('S ('S n)) x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows (Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
 -> FinList ('S ('S n)) x)
-> (ConsecutiveZero t n x
    -> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
-> ConsecutiveZero t n x
-> FinList ('S ('S n)) x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ConsecutiveZero t n x -> Diagram ('Chain t) (n + 3) (n + 2) x
ConsecutiveZero t n x
-> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall (t :: Site) (n :: N') x.
ConsecutiveZero t n x -> Diagram ('Chain t) (n + 3) (n + 2) x
cnzDiagram

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

-- cnzPoints -


-- | the points according to its underlying diagram.

cnzPoints :: Oriented x => ConsecutiveZero t n x -> FinList (n+3) (Point x)
cnzPoints :: forall x (t :: Site) (n :: N').
Oriented x =>
ConsecutiveZero t n x -> FinList (n + 3) (Point x)
cnzPoints = Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> FinList ('S ('S ('S n))) (Point x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints (Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
 -> FinList ('S ('S ('S n))) (Point x))
-> (ConsecutiveZero t n x
    -> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
-> ConsecutiveZero t n x
-> FinList ('S ('S ('S n))) (Point 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
. ConsecutiveZero t n x -> Diagram ('Chain t) (n + 3) (n + 2) x
ConsecutiveZero t n x
-> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall (t :: Site) (n :: N') x.
ConsecutiveZero t n x -> Diagram ('Chain t) (n + 3) (n + 2) x
cnzDiagram

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

-- cnzMapCov -


-- | covariant mapping of 'ConsecutiveZero'.

cnzMapCov :: HomDistributiveDisjunctive h
  => Variant2 Covariant h x y -> ConsecutiveZero t n x -> ConsecutiveZero t n y
cnzMapCov :: 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 Diagram ('Chain t) (n + 3) (n + 2) x
c) = Diagram ('Chain t) (n + 3) (n + 2) y -> ConsecutiveZero t n y
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero (Variant2 'Covariant h x y
-> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedDisjunctive h =>
Variant2 'Covariant h x y -> Diagram t n m x -> Diagram t n m y
dgMapCov Variant2 'Covariant h x y
h Diagram ('Chain t) (n + 3) (n + 2) x
Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
c)

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

-- cnzMapCnt -


-- | contravariant mapping of 'ConsecutiveZero'.

cnzMapCnt :: HomDistributiveDisjunctive h
  => Variant2 Contravariant h x y -> ConsecutiveZero t n x -> ConsecutiveZero (Dual t) n y
cnzMapCnt :: 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 Diagram ('Chain t) (n + 3) (n + 2) x
c) = Diagram ('Chain (Dual t)) (n + 3) (n + 2) y
-> ConsecutiveZero (Dual t) n y
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero (Variant2 'Contravariant h x y
-> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> Dual1 (Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n))) y
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOrientedDisjunctive h =>
Variant2 'Contravariant h x y
-> Diagram t n m x -> Dual1 (Diagram t n m) y
dgMapCnt Variant2 'Contravariant h x y
h Diagram ('Chain t) (n + 3) (n + 2) x
Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
c)

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

-- Duality -


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

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

-- cnzMapS -


-- | mapping of 'ConsecutiveZero'.

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

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

-- Functorial -


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

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

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

-- prpConsecutiveZero -

-- | validity according to 'ConsecutiveZero' for @'Chain' 'To'@.

relConsecutiveZeroTo :: Distributive x => ConsecutiveZero To n x -> Statement
relConsecutiveZeroTo :: forall x (n :: N').
Distributive x =>
ConsecutiveZero 'To n x -> Statement
relConsecutiveZeroTo (ConsecutiveZero c :: Diagram ('Chain 'To) (n + 3) (n + 2) x
c@(DiagramChainTo Point x
_ FinList (n + 2) x
ds)) = [Statement] -> Statement
And [Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) x -> Statement
forall a. Validable a => a -> Statement
valid Diagram ('Chain 'To) (n + 3) (n + 2) x
Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) x
c, N -> FinList ('S ('S n)) x -> Statement
forall x (m :: N'). Distributive x => N -> FinList m x -> Statement
vldCnz N
0 FinList (n + 2) x
FinList ('S ('S n)) x
ds] where
  
  vldCnz :: Distributive x => N -> FinList m x -> Statement
  vldCnz :: forall x (m :: N'). Distributive x => N -> FinList m x -> Statement
vldCnz N
_ FinList m x
Nil         = Statement
SValid
  vldCnz N
_ (x
_:|FinList n1 x
Nil)    = Statement
SValid
  vldCnz N
i (x
d:|x
d':|FinList n1 x
ds) = [Statement] -> Statement
And [ x -> Bool
forall a. Additive a => a -> Bool
isZero (x
d x -> x -> x
forall c. Multiplicative c => c -> c -> c
* x
d') Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
i, String
"d"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
d, String
"d'"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
d']
                             , N -> FinList ('S n1) x -> Statement
forall x (m :: N'). Distributive x => N -> FinList m x -> Statement
vldCnz (N -> N
forall a. Enum a => a -> a
succ N
i) (x
d'x -> FinList n1 x -> FinList (n1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList n1 x
ds)
                             ]

-- | validity according to 'ConsecutiveZero'.

relConsecutiveZero :: Distributive x => ConsecutiveZero t n x -> Statement
relConsecutiveZero :: forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZero t n x -> Statement
relConsecutiveZero c :: ConsecutiveZero t n x
c@(ConsecutiveZero (DiagramChainTo Point x
_ FinList (n + 2) x
_))   = ConsecutiveZero 'To n x -> Statement
forall x (n :: N').
Distributive x =>
ConsecutiveZero 'To n x -> Statement
relConsecutiveZeroTo ConsecutiveZero t n x
ConsecutiveZero 'To n x
c
relConsecutiveZero c :: ConsecutiveZero t n x
c@(ConsecutiveZero (DiagramChainFrom Point x
_ FinList (n + 2) x
_)) = ConsecutiveZero 'To n (Op x) -> Statement
forall x (n :: N').
Distributive x =>
ConsecutiveZero 'To n x -> Statement
relConsecutiveZeroTo Dual1 (ConsecutiveZero 'From n) (Op x)
ConsecutiveZero 'To n (Op x)
c' where
  Contravariant2 IsoO Dst Op x (Op x)
i = Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty 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))

-- | validity according to 'ConsecutiveZero'.

prpConsecutiveZero :: Distributive x => ConsecutiveZero t n x -> Statement
prpConsecutiveZero :: forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZero t n x -> Statement
prpConsecutiveZero ConsecutiveZero t n x
c = String -> Label
Prp String
"ConsecutiveZero" Label -> Statement -> Statement
:<=>: ConsecutiveZero t n x -> Statement
forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZero t n x -> Statement
relConsecutiveZero ConsecutiveZero t n x
c

instance Distributive x => Validable (ConsecutiveZero t n x) where
  valid :: ConsecutiveZero t n x -> Statement
valid = ConsecutiveZero t n x -> Statement
forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZero t n x -> Statement
prpConsecutiveZero

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

-- cnzHead -


-- | the two first arrows as a 'ConsecutiveZero'.

cnzHead :: Distributive x => ConsecutiveZero t n x -> ConsecutiveZero t N0 x
cnzHead :: forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZero t n x -> ConsecutiveZero t 'N0 x
cnzHead (ConsecutiveZero (DiagramChainTo Point x
e (x
d:|x
d':|FinList n1 x
_)))
  = Diagram ('Chain t) ('N0 + 3) ('N0 + 2) x -> ConsecutiveZero t 'N0 x
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero (Point x
-> FinList ('S ('S 'N0)) x
-> Diagram ('Chain 'To) ('S ('S 'N0) + 1) ('S ('S 'N0)) x
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo Point x
e (x
dx -> FinList ('S 'N0) x -> FinList ('S 'N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
d'x -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil))
cnzHead c :: ConsecutiveZero t n x
c@(ConsecutiveZero (DiagramChainFrom Point x
_ FinList (n + 2) x
_)) = ConsecutiveZero t 'N0 x
c'' where
  Contravariant2 IsoO Dst Op x (Op x)
i     = Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty 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 (Right1 ConsecutiveZero t 'N0 x
c'') = Inv2 (HomDisjEmpty Dst Op) (Op x) x
-> SDualBi (ConsecutiveZero 'From 'N0) (Op x)
-> SDualBi (ConsecutiveZero 'From '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 (ConsecutiveZero 'From 'N0))
  (ConsecutiveZero 'From 'N0)
  (Op x)
-> SDualBi (ConsecutiveZero 'From 'N0) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConsecutiveZero 'To 'N0 (Op x)
-> Either1
     (ConsecutiveZero 'To 'N0) (ConsecutiveZero 'From 'N0) (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (ConsecutiveZero 'To 'N0 (Op x)
 -> Either1
      (ConsecutiveZero 'To 'N0) (ConsecutiveZero 'From 'N0) (Op x))
-> ConsecutiveZero 'To 'N0 (Op x)
-> Either1
     (ConsecutiveZero 'To 'N0) (ConsecutiveZero 'From 'N0) (Op x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ConsecutiveZero 'To n (Op x) -> ConsecutiveZero 'To 'N0 (Op x)
forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZero t n x -> ConsecutiveZero t 'N0 x
cnzHead Dual1 (ConsecutiveZero 'From n) (Op x)
ConsecutiveZero 'To n (Op x)
c'))
  
--------------------------------------------------------------------------------

-- cnzTail -


-- | dropping the first arrow.

cnzTail :: Distributive d => ConsecutiveZero t (n+1) d -> ConsecutiveZero t n d
cnzTail :: forall d (t :: Site) (n :: N').
Distributive d =>
ConsecutiveZero t (n + 1) d -> ConsecutiveZero t n d
cnzTail (ConsecutiveZero (DiagramChainTo Point d
_ (d
a:|FinList n1 d
as))) = Diagram ('Chain t) (n + 3) (n + 2) d -> ConsecutiveZero t n d
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero (Point d -> FinList n1 d -> Diagram ('Chain 'To) (n1 + 1) n1 d
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'To) (m + 1) m a
DiagramChainTo (d -> Point d
forall q. Oriented q => q -> Point q
start d
a) FinList n1 d
as)
                                                                                       -- a is dropped

cnzTail c :: ConsecutiveZero t (n + 1) d
c@(ConsecutiveZero (DiagramChainFrom Point d
_ FinList ((n + 1) + 2) d
_))   = ConsecutiveZero t n d
c'' where
  Contravariant2 IsoO Dst Op d (Op d)
i    = Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) d (Op d)
forall x.
Distributive x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) x (Op x)
toDualOpDst
  SDualBi (Left1 Dual1 (ConsecutiveZero 'From ('S n)) (Op d)
c')   = IsoO Dst Op d (Op d)
-> SDualBi (ConsecutiveZero 'From ('S n)) d
-> SDualBi (ConsecutiveZero 'From ('S n)) (Op d)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Dst Op d (Op d)
i (Either1
  (Dual1 (ConsecutiveZero 'From ('S n)))
  (ConsecutiveZero 'From ('S n))
  d
-> SDualBi (ConsecutiveZero 'From ('S n)) d
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConsecutiveZero 'From ('S n) d
-> Either1
     (Dual1 (ConsecutiveZero 'From ('S n)))
     (ConsecutiveZero 'From ('S n))
     d
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 ConsecutiveZero t (n + 1) d
ConsecutiveZero 'From ('S n) d
c))
  SDualBi (Right1 ConsecutiveZero t n d
c'') = Inv2 (HomDisjEmpty Dst Op) (Op d) d
-> SDualBi (ConsecutiveZero 'From n) (Op d)
-> SDualBi (ConsecutiveZero 'From n) d
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Dst Op d (Op d) -> Inv2 (HomDisjEmpty Dst Op) (Op d) d
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Dst Op d (Op d)
i) (Either1
  (Dual1 (ConsecutiveZero 'From n)) (ConsecutiveZero 'From n) (Op d)
-> SDualBi (ConsecutiveZero 'From n) (Op d)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConsecutiveZero 'To n (Op d)
-> Either1 (ConsecutiveZero 'To n) (ConsecutiveZero 'From n) (Op d)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (ConsecutiveZero 'To n (Op d)
 -> Either1
      (ConsecutiveZero 'To n) (ConsecutiveZero 'From n) (Op d))
-> ConsecutiveZero 'To n (Op d)
-> Either1 (ConsecutiveZero 'To n) (ConsecutiveZero 'From n) (Op d)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ConsecutiveZero 'To (n + 1) (Op d) -> ConsecutiveZero 'To n (Op d)
forall d (t :: Site) (n :: N').
Distributive d =>
ConsecutiveZero t (n + 1) d -> ConsecutiveZero t n d
cnzTail Dual1 (ConsecutiveZero 'From ('S n)) (Op d)
ConsecutiveZero 'To (n + 1) (Op d)
c'))
  

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

-- ConsecutiveZeroHom -


-- | homomorphism between two consecutive zero chains.

--

-- __Property__ Let @'ConsecutiveZeroHom' t@ be in @'ConsecutiveZeroHom' __t n x__@ within a

-- 'Distributive' structure @__x__@, then holds

--

-- (1) @'start' t@ and @'end' t@ are consecutive zero chains.

--

newtype ConsecutiveZeroHom t n x
  = ConsecutiveZeroHom (DiagramTrafo (Chain t) (n+3) (n+2) x)
  deriving (Int -> ConsecutiveZeroHom t n x -> ShowS
[ConsecutiveZeroHom t n x] -> ShowS
ConsecutiveZeroHom t n x -> String
(Int -> ConsecutiveZeroHom t n x -> ShowS)
-> (ConsecutiveZeroHom t n x -> String)
-> ([ConsecutiveZeroHom t n x] -> ShowS)
-> Show (ConsecutiveZeroHom t n x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
Int -> ConsecutiveZeroHom t n x -> ShowS
forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
[ConsecutiveZeroHom t n x] -> ShowS
forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
ConsecutiveZeroHom t n x -> String
$cshowsPrec :: forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
Int -> ConsecutiveZeroHom t n x -> ShowS
showsPrec :: Int -> ConsecutiveZeroHom t n x -> ShowS
$cshow :: forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
ConsecutiveZeroHom t n x -> String
show :: ConsecutiveZeroHom t n x -> String
$cshowList :: forall (t :: Site) (n :: N') x.
(ShowPoint x, Show x) =>
[ConsecutiveZeroHom t n x] -> ShowS
showList :: [ConsecutiveZeroHom t n x] -> ShowS
Show,ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool
(ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool)
-> (ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool)
-> Eq (ConsecutiveZeroHom t n x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: Site) (n :: N') x.
(EqPoint x, Eq x) =>
ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool
$c== :: forall (t :: Site) (n :: N') x.
(EqPoint x, Eq x) =>
ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool
== :: ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool
$c/= :: forall (t :: Site) (n :: N') x.
(EqPoint x, Eq x) =>
ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool
/= :: ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x -> Bool
Eq)

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

-- cnzHomSite -


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

cnzHomSite :: ConsecutiveZeroHom t n x -> Either (t :~: From) (t :~: To)
cnzHomSite :: forall (t :: Site) (n :: N') x.
ConsecutiveZeroHom t n x -> Either (t :~: 'From) (t :~: 'To)
cnzHomSite (ConsecutiveZeroHom (DiagramTrafo Diagram ('Chain t) (n + 3) (n + 2) x
d Diagram ('Chain t) (n + 3) (n + 2) x
_ FinList (n + 3) x
_)) = case Diagram ('Chain t) (n + 3) (n + 2) x
d of
  DiagramChainFrom Point x
_ FinList (n + 2) x
_ -> (t :~: 'From) -> Either (t :~: 'From) (t :~: 'To)
forall a b. a -> Either a b
Left t :~: t
t :~: 'From
forall {k} (a :: k). a :~: a
Refl
  DiagramChainTo Point x
_ FinList (n + 2) x
_   -> (t :~: 'To) -> Either (t :~: 'From) (t :~: 'To)
forall a b. b -> Either a b
Right t :~: t
t :~: 'To
forall {k} (a :: k). a :~: a
Refl
  
--------------------------------------------------------------------------------

-- cnzHomMapCov -


-- | covariant mapping of 'ConsecutiveZeroHom'.

cnzHomMapCov :: HomDistributiveDisjunctive h
  => Variant2 Covariant h x y -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n y
cnzHomMapCov :: forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
HomDistributiveDisjunctive h =>
Variant2 'Covariant h x y
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n y
cnzHomMapCov Variant2 'Covariant h x y
h (ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
t) = DiagramTrafo ('Chain t) (n + 3) (n + 2) y
-> ConsecutiveZeroHom t n y
forall (t :: Site) (n :: N') x.
DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
ConsecutiveZeroHom (Variant2 'Covariant h x y
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) y
forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicativeDisjunctive h =>
Variant2 'Covariant h a b
-> DiagramTrafo t n m a -> DiagramTrafo t n m b
dgtMapCov Variant2 'Covariant h x y
h DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t)

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

-- cnzHomMapCnt -


-- | contravariant mapping of 'ConsecutiveZeroHom'.

cnzHomMapCnt :: HomDistributiveDisjunctive h
  => Variant2 Contravariant h x y -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom (Dual t) n y
cnzHomMapCnt :: forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
HomDistributiveDisjunctive h =>
Variant2 'Contravariant h x y
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom (Dual t) n y
cnzHomMapCnt Variant2 'Contravariant h x y
h (ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
t) = DiagramTrafo ('Chain (Dual t)) (n + 3) (n + 2) y
-> ConsecutiveZeroHom (Dual t) n y
forall (t :: Site) (n :: N') x.
DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
ConsecutiveZeroHom (Variant2 'Contravariant h x y
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo (Dual ('Chain t)) ('S ('S ('S n))) ('S ('S n)) y
forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
HomMultiplicativeDisjunctive h =>
Variant2 'Contravariant h a b
-> DiagramTrafo t n m a -> DiagramTrafo (Dual t) n m b
dgtMapCnt Variant2 'Contravariant h x y
h DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t)

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

-- Duality -


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

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

-- cnzHomMapS -


-- | mapping of 'ConsecutiveZeroHom'.

cnzHomMapS :: (HomDistributiveDisjunctive h, t ~ Dual (Dual t))
  => h x y -> SDualBi (ConsecutiveZeroHom t n) x -> SDualBi (ConsecutiveZeroHom t n) y
cnzHomMapS :: forall (h :: * -> * -> *) (t :: Site) x y (n :: N').
(HomDistributiveDisjunctive h, t ~ Dual (Dual t)) =>
h x y
-> SDualBi (ConsecutiveZeroHom t n) x
-> SDualBi (ConsecutiveZeroHom t n) y
cnzHomMapS = (Variant2 'Covariant h x y
 -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n y)
-> (Variant2 'Covariant h x y
    -> Dual1 (ConsecutiveZeroHom t n) x
    -> Dual1 (ConsecutiveZeroHom t n) y)
-> (Variant2 'Contravariant h x y
    -> ConsecutiveZeroHom t n x -> Dual1 (ConsecutiveZeroHom t n) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (ConsecutiveZeroHom t n) x -> ConsecutiveZeroHom t n y)
-> h x y
-> SDualBi (ConsecutiveZeroHom t n) x
-> SDualBi (ConsecutiveZeroHom 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
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
HomDistributiveDisjunctive h =>
Variant2 'Covariant h x y
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n y
cnzHomMapCov Variant2 'Covariant h x y
-> Dual1 (ConsecutiveZeroHom t n) x
-> Dual1 (ConsecutiveZeroHom t n) y
Variant2 'Covariant h x y
-> ConsecutiveZeroHom (Dual t) n x
-> ConsecutiveZeroHom (Dual t) n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
HomDistributiveDisjunctive h =>
Variant2 'Covariant h x y
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n y
cnzHomMapCov Variant2 'Contravariant h x y
-> ConsecutiveZeroHom t n x -> Dual1 (ConsecutiveZeroHom t n) y
Variant2 'Contravariant h x y
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom (Dual t) n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
HomDistributiveDisjunctive h =>
Variant2 'Contravariant h x y
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom (Dual t) n y
cnzHomMapCnt Variant2 'Contravariant h x y
-> Dual1 (ConsecutiveZeroHom t n) x -> ConsecutiveZeroHom t n y
Variant2 'Contravariant h x y
-> ConsecutiveZeroHom (Dual t) n x
-> ConsecutiveZeroHom (Dual (Dual t)) n y
forall (h :: * -> * -> *) x y (t :: Site) (n :: N').
HomDistributiveDisjunctive h =>
Variant2 'Contravariant h x y
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom (Dual t) n y
cnzHomMapCnt

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

-- Functorial -


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

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

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

-- Validable -


instance (Distributive x, Typeable t, Typeable n) => Validable (ConsecutiveZeroHom t n x) where
  valid :: ConsecutiveZeroHom t n x -> Statement
valid (ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
t) = String -> Label
Label String
"ConsecutiveZeroHom" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x -> Statement
forall a. Validable a => a -> Statement
valid DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t
        , String -> Label
Label String
"start" Label -> Statement -> Statement
:<=>: ConsecutiveZero t n x -> Statement
forall a. Validable a => a -> Statement
valid (Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> ConsecutiveZero t n x
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero (Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
 -> ConsecutiveZero t n x)
-> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> ConsecutiveZero t n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> Point (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
forall q. Oriented q => q -> Point q
start DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t)
        , String -> Label
Label String
"end" Label -> Statement -> Statement
:<=>: ConsecutiveZero t n x -> Statement
forall a. Validable a => a -> Statement
valid (Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> ConsecutiveZero t n x
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero (Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
 -> ConsecutiveZero t n x)
-> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> ConsecutiveZero t n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> Point (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
forall q. Oriented q => q -> Point q
end DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t)
        ]
    
--------------------------------------------------------------------------------

-- ConsecutiveZeroHom - Algebraic -


type instance Point (ConsecutiveZeroHom t n x) = ConsecutiveZero t n x

instance (Show x, ShowPoint x) => ShowPoint (ConsecutiveZeroHom t n x)
instance (Eq x, EqPoint x) => EqPoint (ConsecutiveZeroHom t n x)
instance Distributive x => ValidablePoint (ConsecutiveZeroHom t n x)
instance (Typeable x, Typeable t, Typeable n) => TypeablePoint (ConsecutiveZeroHom t n x)

instance (Distributive x, Typeable t, Typeable n) => Oriented (ConsecutiveZeroHom t n x) where
  orientation :: ConsecutiveZeroHom t n x
-> Orientation (Point (ConsecutiveZeroHom t n x))
orientation (ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
t) = Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero Point (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
Diagram ('Chain t) (n + 3) (n + 2) x
a ConsecutiveZero t n x
-> ConsecutiveZero t n x -> Orientation (ConsecutiveZero t n x)
forall p. p -> p -> Orientation p
:> Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero Point (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
Diagram ('Chain t) (n + 3) (n + 2) x
b where
    Point (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
a :> Point (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
b = DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> Orientation
     (Point (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x))
forall q. Oriented q => q -> Orientation (Point q)
orientation DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t

instance (Distributive x, Typeable t, Typeable n) => Multiplicative (ConsecutiveZeroHom t n x) where
  one :: Point (ConsecutiveZeroHom t n x) -> ConsecutiveZeroHom t n x
one (ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
c) = DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) 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) ('S ('S ('S n))) ('S ('S n)) x
 -> ConsecutiveZeroHom t n x)
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> ConsecutiveZeroHom t n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Point (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall c. Multiplicative c => Point c -> c
one Point (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
Diagram ('Chain t) (n + 3) (n + 2) x
c
  ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
f * :: ConsecutiveZeroHom t n x
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x
* ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
g = 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
fDiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall c. Multiplicative c => c -> c -> c
*DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
g)
  npower :: ConsecutiveZeroHom t n x -> N -> ConsecutiveZeroHom t n x
npower (ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
f) N
n = 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) ('S ('S ('S n))) ('S ('S n)) x
-> N -> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall c. Multiplicative c => c -> N -> c
npower DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
f N
n)
  
type instance Root (ConsecutiveZeroHom t n x) = Orientation (ConsecutiveZero t n x)

instance (Show x, ShowPoint x) => ShowRoot (ConsecutiveZeroHom t n x)
instance (Eq x, EqPoint x) => EqRoot (ConsecutiveZeroHom t n x)
instance Distributive x => ValidableRoot (ConsecutiveZeroHom t n x)
instance (Typeable x, Typeable t, Typeable n) => TypeableRoot (ConsecutiveZeroHom t n x)

instance (Distributive x, Typeable t, Typeable n) => Fibred (ConsecutiveZeroHom t n x)
  
instance (Distributive x, Typeable t, Typeable n) => FibredOriented (ConsecutiveZeroHom t n x)

instance (Distributive x, Typeable t, Typeable n) => Additive (ConsecutiveZeroHom t n x) where
  zero :: Root (ConsecutiveZeroHom t n x) -> ConsecutiveZeroHom t n x
zero (ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
a :> ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
b) = DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) 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) ('S ('S ('S n))) ('S ('S n)) x
 -> ConsecutiveZeroHom t n x)
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> ConsecutiveZeroHom t n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Root (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall a. Additive a => Root a -> a
zero (Diagram ('Chain t) (n + 3) (n + 2) x
Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
a Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> Orientation (Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
forall p. p -> p -> Orientation p
:> Diagram ('Chain t) (n + 3) (n + 2) x
Diagram ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
b)
  ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
f + :: ConsecutiveZeroHom t n x
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x
+ ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
g = 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
fDiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall a. Additive a => a -> a -> a
+DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
g)
  ntimes :: N -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x
ntimes N
n (ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
t) = 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 (N
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall a. Additive a => N -> a -> a
ntimes N
n DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t)
  
instance (Distributive x, Abelian x, Typeable t, Typeable n)
  => Abelian (ConsecutiveZeroHom t n x) where
  negate :: ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x
negate (ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
t) = DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) 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) ('S ('S ('S n))) ('S ('S n)) x
 -> ConsecutiveZeroHom t n x)
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> ConsecutiveZeroHom t n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall a. Abelian a => a -> a
negate DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t
  ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
f - :: ConsecutiveZeroHom t n x
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x
- ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
g = 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
fDiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall a. Abelian a => a -> a -> a
-DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
g)
  ztimes :: Z -> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x
ztimes Z
n (ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
t) = 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 (Z
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall a. Abelian a => Z -> a -> a
ztimes Z
n DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t)
  
instance (Distributive x, Typeable t, Typeable n) => Distributive (ConsecutiveZeroHom t n x)

instance (Algebraic x, Typeable t, Typeable n) => Vectorial (ConsecutiveZeroHom t n x) where
  type Scalar (ConsecutiveZeroHom t n x) = Scalar x
  Scalar (ConsecutiveZeroHom t n x)
x ! :: Scalar (ConsecutiveZeroHom t n x)
-> ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t n x
! ConsecutiveZeroHom DiagramTrafo ('Chain t) (n + 3) (n + 2) x
t = 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 (Scalar (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
Scalar (ConsecutiveZeroHom t n x)
xScalar (DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x)
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
-> DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
forall v. Vectorial v => Scalar v -> v -> v
!DiagramTrafo ('Chain t) (n + 3) (n + 2) x
DiagramTrafo ('Chain t) ('S ('S ('S n))) ('S ('S n)) x
t)

instance (Algebraic x, Typeable t, Typeable n) => Algebraic (ConsecutiveZeroHom t n x)

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

-- cnzHomHead -


-- | the first two arrows of the given 'ConsecutiveZeroHom'.

cnzHomHead :: Distributive x => ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t N0 x
cnzHomHead :: forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZeroHom t n x -> ConsecutiveZeroHom t 'N0 x
cnzHomHead (ConsecutiveZeroHom (DiagramTrafo Diagram ('Chain t) (n + 3) (n + 2) x
a Diagram ('Chain t) (n + 3) (n + 2) x
b (x
f0:|x
f1:|x
f2:|FinList n1 x
_)))
  = DiagramTrafo ('Chain t) ('N0 + 3) ('N0 + 2) x
-> ConsecutiveZeroHom t 'N0 x
forall (t :: Site) (n :: N') x.
DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
ConsecutiveZeroHom (Diagram ('Chain t) ('S ('S ('S 'N0))) ('S ('S 'N0)) x
-> Diagram ('Chain t) ('S ('S ('S 'N0))) ('S ('S 'N0)) x
-> FinList ('S ('S ('S 'N0))) x
-> DiagramTrafo ('Chain t) ('S ('S ('S 'N0))) ('S ('S '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 Diagram ('Chain t) ('N0 + 3) ('N0 + 2) x
Diagram ('Chain t) ('S ('S ('S 'N0))) ('S ('S 'N0)) x
a' Diagram ('Chain t) ('N0 + 3) ('N0 + 2) x
Diagram ('Chain t) ('S ('S ('S 'N0))) ('S ('S 'N0)) x
b' (x
f0x -> FinList ('S ('S 'N0)) x -> FinList ('S ('S 'N0) + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
f1x -> FinList ('S 'N0) x -> FinList ('S 'N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
f2x -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil)) where
  ConsecutiveZero Diagram ('Chain t) ('N0 + 3) ('N0 + 2) x
a' = 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 -> ConsecutiveZero t 'N0 x)
-> ConsecutiveZero t n x -> ConsecutiveZero t 'N0 x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
a
  ConsecutiveZero Diagram ('Chain t) ('N0 + 3) ('N0 + 2) x
b' = 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 -> ConsecutiveZero t 'N0 x)
-> ConsecutiveZero t n x -> ConsecutiveZero t 'N0 x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
b
  
--------------------------------------------------------------------------------

-- cnzHomTail -


-- | dropping the first arrow.

cnzHomTail :: Distributive x => ConsecutiveZeroHom t (n+1) x -> ConsecutiveZeroHom t n x
cnzHomTail :: forall x (t :: Site) (n :: N').
Distributive x =>
ConsecutiveZeroHom t (n + 1) x -> ConsecutiveZeroHom t n x
cnzHomTail (ConsecutiveZeroHom (DiagramTrafo Diagram ('Chain t) ((n + 1) + 3) ((n + 1) + 2) x
a Diagram ('Chain t) ((n + 1) + 3) ((n + 1) + 2) x
b FinList ((n + 1) + 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 (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 ('S ('S ('S n)) + 1) x -> FinList ('S ('S ('S n))) x
forall (n :: N') a. FinList (n + 1) a -> FinList n a
tail FinList ((n + 1) + 3) x
FinList ('S ('S ('S n)) + 1) x
fs)) where
  ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
a' = ConsecutiveZero t (n + 1) x -> ConsecutiveZero t n x
ConsecutiveZero t ('S n) 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 ('S n) x -> ConsecutiveZero t n x)
-> ConsecutiveZero t ('S n) x -> ConsecutiveZero t n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram ('Chain t) ('S n + 3) ('S n + 2) x
-> ConsecutiveZero t ('S n) x
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero Diagram ('Chain t) ((n + 1) + 3) ((n + 1) + 2) x
Diagram ('Chain t) ('S n + 3) ('S n + 2) x
a
  ConsecutiveZero Diagram ('Chain t) (n + 3) (n + 2) x
b' = ConsecutiveZero t (n + 1) x -> ConsecutiveZero t n x
ConsecutiveZero t ('S n) 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 ('S n) x -> ConsecutiveZero t n x)
-> ConsecutiveZero t ('S n) x -> ConsecutiveZero t n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram ('Chain t) ('S n + 3) ('S n + 2) x
-> ConsecutiveZero t ('S n) x
forall (t :: Site) (n :: N') x.
Diagram ('Chain t) (n + 3) (n + 2) x -> ConsecutiveZero t n x
ConsecutiveZero Diagram ('Chain t) ((n + 1) + 3) ((n + 1) + 2) x
Diagram ('Chain t) ('S n + 3) ('S n + 2) x
b

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

-- cnzHomArrows -


-- | the underlying arrows.

cnzHomArrows :: ConsecutiveZeroHom t n x -> FinList (n+3) x
cnzHomArrows :: forall (t :: Site) (n :: N') x.
ConsecutiveZeroHom t n x -> FinList (n + 3) x
cnzHomArrows (ConsecutiveZeroHom (DiagramTrafo Diagram ('Chain t) (n + 3) (n + 2) x
_ Diagram ('Chain t) (n + 3) (n + 2) x
_ FinList (n + 3) x
fs)) = FinList (n + 3) x
fs

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

-- SomeConsecutiveZeroHom -


-- | some 'ConsecutiveZeroHom'.

data SomeConsecutiveZeroHom x where
  SomeConsecutiveZeroHom :: (Typeable t, Attestable n)
    => ConsecutiveZeroHom t n x -> SomeConsecutiveZeroHom x

instance Distributive x => Validable (SomeConsecutiveZeroHom x) where
  valid :: SomeConsecutiveZeroHom x -> Statement
valid (SomeConsecutiveZeroHom ConsecutiveZeroHom t n x
t) = String -> Label
Label String
"SomeConsecutiveZeroHom" Label -> Statement -> Statement
:<=>: ConsecutiveZeroHom t n x -> Statement
forall a. Validable a => a -> Statement
valid ConsecutiveZeroHom t n x
t
  
--------------------------------------------------------------------------------

-- xSomeConsecutiveZeroHomOrnt -


-- | random variable for @'ConsecutiveZeroHom' __t n__ 'OS'@ with a maximal @__n__@ of the given one.

xSomeConsecutiveZeroHomOrnt :: N -> X (SomeConsecutiveZeroHom OS)
xSomeConsecutiveZeroHomOrnt :: N -> X (SomeConsecutiveZeroHom OS)
xSomeConsecutiveZeroHomOrnt N
n = N -> X (SomeConsecutiveZeroHom OS)
xscnzHomTo N
n X (SomeConsecutiveZeroHom OS)
-> X (SomeConsecutiveZeroHom OS) -> X (SomeConsecutiveZeroHom OS)
forall a. X a -> X a -> X a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> N -> X (SomeConsecutiveZeroHom OS)
xscnzHomFrom N
n where

  xTo :: Any n -> X (Diagram (Chain To) (n+3) (n+2) OS)
  xTo :: forall (n :: N').
Any n -> X (Diagram ('Chain 'To) (n + 3) (n + 2) OS)
xTo Any n
n = (Dual (Dual ('Chain 'To)) :~: 'Chain 'To)
-> XDiagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
-> X (Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram Dual (Dual ('Chain 'To)) :~: 'Chain 'To
'Chain 'To :~: 'Chain 'To
forall {k} (a :: k). a :~: a
Refl (XDiagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
 -> X (Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS))
-> XDiagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
-> X (Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Any ('S ('S n))
-> XOrtSite 'To OS
-> XDiagram ('Chain 'To) ('S ('S n) + 1) ('S ('S n)) OS
forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Chain 'To) (m + 1) m a
XDiagramChainTo (W ('S n) -> W ('S n + 1)
W ('S n) -> Any ('S ('S n))
forall (n1 :: N'). W n1 -> W (n1 + 1)
SW (W ('S n) -> Any ('S ('S n))) -> W ('S n) -> Any ('S ('S n))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Any n -> W (n + 1)
forall (n1 :: N'). W n1 -> W (n1 + 1)
SW Any n
n) XOrtSite 'To OS
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite
  
  xFrom :: Any n -> X (Diagram (Chain From) (n+3) (n+2) OS)
  xFrom :: forall (n :: N').
Any n -> X (Diagram ('Chain 'From) (n + 3) (n + 2) OS)
xFrom Any n
n = (Dual (Dual ('Chain 'From)) :~: 'Chain 'From)
-> XDiagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
-> X (Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram Dual (Dual ('Chain 'From)) :~: 'Chain 'From
'Chain 'From :~: 'Chain 'From
forall {k} (a :: k). a :~: a
Refl (XDiagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
 -> X (Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS))
-> XDiagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
-> X (Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Any ('S ('S n))
-> XOrtSite 'From OS
-> XDiagram ('Chain 'From) ('S ('S n) + 1) ('S ('S n)) OS
forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Chain 'From) (m + 1) m a
XDiagramChainFrom (W ('S n) -> W ('S n + 1)
W ('S n) -> Any ('S ('S n))
forall (n1 :: N'). W n1 -> W (n1 + 1)
SW (W ('S n) -> Any ('S ('S n))) -> W ('S n) -> Any ('S ('S n))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Any n -> W (n + 1)
forall (n1 :: N'). W n1 -> W (n1 + 1)
SW Any n
n) XOrtSite 'From OS
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite
  
  xcnzHomTo :: Any n -> X (ConsecutiveZeroHom To n OS)
  xcnzHomTo :: forall (n :: N'). Any n -> X (ConsecutiveZeroHom 'To n OS)
xcnzHomTo Any n
n = do
    Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
a <- Any n -> X (Diagram ('Chain 'To) (n + 3) (n + 2) OS)
forall (n :: N').
Any n -> X (Diagram ('Chain 'To) (n + 3) (n + 2) OS)
xTo Any n
n
    Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
b <- Any n -> X (Diagram ('Chain 'To) (n + 3) (n + 2) OS)
forall (n :: N').
Any n -> X (Diagram ('Chain 'To) (n + 3) (n + 2) OS)
xTo Any n
n
    ConsecutiveZeroHom 'To n OS -> X (ConsecutiveZeroHom 'To n OS)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ConsecutiveZeroHom 'To n OS -> X (ConsecutiveZeroHom 'To n OS))
-> ConsecutiveZeroHom 'To n OS -> X (ConsecutiveZeroHom 'To n OS)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ DiagramTrafo ('Chain 'To) (n + 3) (n + 2) OS
-> ConsecutiveZeroHom 'To n OS
DiagramTrafo ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
-> ConsecutiveZeroHom 'To n OS
forall (t :: Site) (n :: N') x.
DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
ConsecutiveZeroHom
           (DiagramTrafo ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
 -> ConsecutiveZeroHom 'To n OS)
-> DiagramTrafo ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
-> ConsecutiveZeroHom 'To n OS
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
-> Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
-> FinList ('S ('S ('S n))) OS
-> DiagramTrafo ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
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 ('S n))) ('S ('S n)) OS
a Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
b
           (FinList ('S ('S ('S n))) OS
 -> DiagramTrafo ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS)
-> FinList ('S ('S ('S n))) OS
-> DiagramTrafo ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Symbol, Symbol) -> OS)
-> FinList ('S ('S ('S n))) (Symbol, Symbol)
-> FinList ('S ('S ('S n))) OS
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 ((Symbol -> Symbol -> OS) -> (Symbol, Symbol) -> OS
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Symbol -> OS
forall p. p -> p -> Orientation p
(:>))
           (FinList ('S ('S ('S n))) (Symbol, Symbol)
 -> FinList ('S ('S ('S n))) OS)
-> FinList ('S ('S ('S n))) (Symbol, Symbol)
-> FinList ('S ('S ('S n))) OS
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
-> FinList ('S ('S ('S n))) (Point OS)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
a FinList ('S ('S ('S n))) Symbol
-> FinList ('S ('S ('S n))) Symbol
-> FinList ('S ('S ('S n))) (Symbol, Symbol)
forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
-> FinList ('S ('S ('S n))) (Point OS)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram ('Chain 'To) ('S ('S ('S n))) ('S ('S n)) OS
b) 

  xcnzHomFrom :: Any n -> X (ConsecutiveZeroHom From n OS)
  xcnzHomFrom :: forall (n :: N'). Any n -> X (ConsecutiveZeroHom 'From n OS)
xcnzHomFrom Any n
n = do
    Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
a <- Any n -> X (Diagram ('Chain 'From) (n + 3) (n + 2) OS)
forall (n :: N').
Any n -> X (Diagram ('Chain 'From) (n + 3) (n + 2) OS)
xFrom Any n
n
    Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
b <- Any n -> X (Diagram ('Chain 'From) (n + 3) (n + 2) OS)
forall (n :: N').
Any n -> X (Diagram ('Chain 'From) (n + 3) (n + 2) OS)
xFrom Any n
n
    ConsecutiveZeroHom 'From n OS -> X (ConsecutiveZeroHom 'From n OS)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (ConsecutiveZeroHom 'From n OS
 -> X (ConsecutiveZeroHom 'From n OS))
-> ConsecutiveZeroHom 'From n OS
-> X (ConsecutiveZeroHom 'From n OS)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ DiagramTrafo ('Chain 'From) (n + 3) (n + 2) OS
-> ConsecutiveZeroHom 'From n OS
DiagramTrafo ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
-> ConsecutiveZeroHom 'From n OS
forall (t :: Site) (n :: N') x.
DiagramTrafo ('Chain t) (n + 3) (n + 2) x
-> ConsecutiveZeroHom t n x
ConsecutiveZeroHom
           (DiagramTrafo ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
 -> ConsecutiveZeroHom 'From n OS)
-> DiagramTrafo ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
-> ConsecutiveZeroHom 'From n OS
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
-> Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
-> FinList ('S ('S ('S n))) OS
-> DiagramTrafo ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
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 'From) ('S ('S ('S n))) ('S ('S n)) OS
a Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
b
           (FinList ('S ('S ('S n))) OS
 -> DiagramTrafo ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS)
-> FinList ('S ('S ('S n))) OS
-> DiagramTrafo ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ((Symbol, Symbol) -> OS)
-> FinList ('S ('S ('S n))) (Symbol, Symbol)
-> FinList ('S ('S ('S n))) OS
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 ((Symbol -> Symbol -> OS) -> (Symbol, Symbol) -> OS
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Symbol -> OS
forall p. p -> p -> Orientation p
(:>))
           (FinList ('S ('S ('S n))) (Symbol, Symbol)
 -> FinList ('S ('S ('S n))) OS)
-> FinList ('S ('S ('S n))) (Symbol, Symbol)
-> FinList ('S ('S ('S n))) OS
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
-> FinList ('S ('S ('S n))) (Point OS)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
a FinList ('S ('S ('S n))) Symbol
-> FinList ('S ('S ('S n))) Symbol
-> FinList ('S ('S ('S n))) (Symbol, Symbol)
forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
-> FinList ('S ('S ('S n))) (Point OS)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram ('Chain 'From) ('S ('S ('S n))) ('S ('S n)) OS
b) 
  
  xscnzHomTo :: N -> X (SomeConsecutiveZeroHom OS)
  xscnzHomTo :: N -> X (SomeConsecutiveZeroHom OS)
xscnzHomTo N
n = do
    SomeNatural W n
n' <- (N -> SomeNatural) -> X N -> X SomeNatural
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 N -> SomeNatural
someNatural (X N -> X SomeNatural) -> X N -> X SomeNatural
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> N -> X N
xNB N
0 N
n
    ConsecutiveZeroHom 'To n OS
t              <- W n -> X (ConsecutiveZeroHom 'To n OS)
forall (n :: N'). Any n -> X (ConsecutiveZeroHom 'To n OS)
xcnzHomTo W n
n'
    SomeConsecutiveZeroHom OS -> X (SomeConsecutiveZeroHom OS)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeConsecutiveZeroHom OS -> X (SomeConsecutiveZeroHom OS))
-> SomeConsecutiveZeroHom OS -> X (SomeConsecutiveZeroHom OS)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ConsecutiveZeroHom 'To n OS -> SomeConsecutiveZeroHom OS
forall (t :: Site) (n :: N') x.
(Typeable t, Attestable n) =>
ConsecutiveZeroHom t n x -> SomeConsecutiveZeroHom x
SomeConsecutiveZeroHom ConsecutiveZeroHom 'To n OS
t

  xscnzHomFrom :: N -> X (SomeConsecutiveZeroHom OS)
  xscnzHomFrom :: N -> X (SomeConsecutiveZeroHom OS)
xscnzHomFrom N
n = do
    SomeNatural W n
n' <- (N -> SomeNatural) -> X N -> X SomeNatural
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 N -> SomeNatural
someNatural (X N -> X SomeNatural) -> X N -> X SomeNatural
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> N -> X N
xNB N
0 N
n
    ConsecutiveZeroHom 'From n OS
t              <- W n -> X (ConsecutiveZeroHom 'From n OS)
forall (n :: N'). Any n -> X (ConsecutiveZeroHom 'From n OS)
xcnzHomFrom W n
n'
    SomeConsecutiveZeroHom OS -> X (SomeConsecutiveZeroHom OS)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeConsecutiveZeroHom OS -> X (SomeConsecutiveZeroHom OS))
-> SomeConsecutiveZeroHom OS -> X (SomeConsecutiveZeroHom OS)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ ConsecutiveZeroHom 'From n OS -> SomeConsecutiveZeroHom OS
forall (t :: Site) (n :: N') x.
(Typeable t, Attestable n) =>
ConsecutiveZeroHom t n x -> SomeConsecutiveZeroHom x
SomeConsecutiveZeroHom ConsecutiveZeroHom 'From n OS
t