{-# LANGUAGE NoImplicitPrelude #-}

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

{-# LANGUAGE FlexibleContexts, RankNTypes #-}


-- |
-- Module      : OAlg.Limes.Cone.Definition
-- Description : definition of cones over diagrams
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- definition of 'Cone's over 'Diagram's.
module OAlg.Limes.Cone.Definition
  (
    -- * Cone
    Cone(..), Perspective(..)
  , cnDiagram, cnDiagramTypeRefl
  , tip, shell, cnArrows, cnPoints
  , cnMap, cnMapMlt, cnMapDst
  
    -- ** Distributive
  , cnZeroHead
  , cnKernel, cnCokernel
  , cnDiffHead
  , ConeZeroHead(..)
  , coConeZeroHead, czFromOpOp, coConeZeroHeadInv
  
    -- ** Duality
  , cnToOp, cnFromOp, ConeDuality(..)
  , coCone, coConeInv, cnFromOpOp

    -- * Cone Struct
  , ConeStruct(..), cnStructOp, cnStructMlt, cnStruct
 
    -- * Orientation
  , cnPrjOrnt, cnInjOrnt

    -- * Chain
  , cnPrjChainTo, cnPrjChainToInv
  , cnPrjChainFrom, cnPrjChainFromInv
  , FactorChain(..)
  ) where

import Control.Monad

import Data.Typeable
import Data.Array hiding (range)

import OAlg.Prelude

import OAlg.Entity.Natural hiding ((++))
import OAlg.Entity.FinList
import OAlg.Entity.Diagram

import OAlg.Structure.Oriented
import OAlg.Structure.Fibred
import OAlg.Structure.Multiplicative as Mlt
import OAlg.Structure.Additive
import OAlg.Structure.Distributive

import OAlg.Hom.Oriented
import OAlg.Hom.Multiplicative
import OAlg.Hom.Distributive
import OAlg.Hom.Definition

import OAlg.Limes.Perspective

--------------------------------------------------------------------------------
-- Cone -

-- | cone over a diagram.
--
-- __Properties__ Let @c@ be in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ then holds:
--
-- (1) If @c@ matches @'ConeProjective' d t cs@ for a 'Multiplicative' structure __@a@__
-- then holds:
--
--     (1) For all @ci@ in @cs@ holds: @'start' ci '==' t@ and
--     @'end' ci '==' pi@ where @pi@ in @'dgPoints' d@.
--
--     (2) For all @aij@ in @'dgArrows' d@ holds: @aij 'Mlt.*' ci '==' cj@
--     where @ci@, @cj@ in @cs@.
--
-- (2) If @c@ matches @'ConeInjective' d t cs@ for a 'Multiplicative' structure __@a@__
-- then holds:
--
--     (1) For all @ci@ in @cs@ holds: @'end' ci '==' t@ and
--     @'start' ci '==' pi@ where @pi@ in @'dgPoints' d@.
--
--     (2) For all @aij@ in @'dgArrows' d@ holds: @cj 'Mlt.*' aij '==' ci@
--     where @ci@, @cj@ in @cs@.
--
-- (3) If @c@ matches @'ConeKernel' p k@ for a 'Distributive' structure __@a@__ then holds:
--
--     (1) @'end' k '==' p0@ where @p0@ in @'dgPoints' p@
--
--     (2) For all @a@ in @'dgArrows' p@ holds: @a 'Mlt.*' k '==' 'zero' (t ':>' p1)@
--     where @t = 'start' k@ and @p0@, @p1@ in @'dgPoints' p@.
--
-- (4) If @c@ matches @'ConeCokernel' p k@ for a 'Distributive' structure __@a@__ then
-- holds:
--
--     (1) @'start' k '==' p0@ where @p0@ in @'cnPoints' c@
--
--     (2) For all @a@ in @'dgArrows' p@ holds: @k 'Mlt.*' a '==' 'zero' (p1 ':>' t)@ where
--     @t = 'end' k@ and @p0@, @p1@ in @'dgPoints' p@.
data Cone s p t n m a where
  ConeProjective :: Multiplicative a
    => Diagram t n m a -> Point a -> FinList n a -> Cone Mlt Projective t n m a
  ConeInjective  :: Multiplicative a
    => Diagram t n m a -> Point a -> FinList n a -> Cone Mlt Injective t n m a
  ConeKernel     :: Distributive a
    => Diagram (Parallel LeftToRight) N2 m a -> a
    -> Cone Dst Projective (Parallel LeftToRight)  N2 m a
  ConeCokernel   :: Distributive a
    => Diagram (Parallel RightToLeft) N2 m a -> a
    -> Cone Dst Injective (Parallel RightToLeft) N2 m a


--------------------------------------------------------------------------------
-- ConeStruct -

-- | cone structures.
data ConeStruct s a where
  ConeStructMlt :: Multiplicative a => ConeStruct Mlt a
  ConeStructDst :: Distributive a => ConeStruct Dst a

deriving instance Show (ConeStruct s a)
deriving instance Eq (ConeStruct s a)

--------------------------------------------------------------------------------
-- cnStructOp -

-- | the opposite cone structure.
cnStructOp :: ConeStruct s a -> ConeStruct s (Op a)
cnStructOp :: forall s a. ConeStruct s a -> ConeStruct s (Op a)
cnStructOp ConeStruct s a
cs = case ConeStruct s a
cs of
  ConeStruct s a
ConeStructMlt -> forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt
  ConeStruct s a
ConeStructDst -> forall a. Distributive a => ConeStruct Dst a
ConeStructDst

--------------------------------------------------------------------------------
-- cnStructMlt -

-- | the 'Multiplicative' structure of a cone structure.
cnStructMlt :: ConeStruct s a -> Struct Mlt a
cnStructMlt :: forall s a. ConeStruct s a -> Struct Mlt a
cnStructMlt ConeStruct s a
cs = case ConeStruct s a
cs of
  ConeStruct s a
ConeStructMlt -> forall s x. Structure s x => Struct s x
Struct
  ConeStruct s a
ConeStructDst -> forall s x. Structure s x => Struct s x
Struct

--------------------------------------------------------------------------------
-- cnStruct -

-- | the associated structure of a cone structure.
cnStruct :: ConeStruct s a -> Struct s a
cnStruct :: forall s a. ConeStruct s a -> Struct s a
cnStruct ConeStruct s a
cs = case ConeStruct s a
cs of
  ConeStruct s a
ConeStructMlt -> forall s x. Structure s x => Struct s x
Struct
  ConeStruct s a
ConeStructDst -> forall s x. Structure s x => Struct s x
Struct

--------------------------------------------------------------------------------
-- cnDiagram -

-- | the underlying diagram.
cnDiagram :: Cone s p t n m a -> Diagram t n m a
cnDiagram :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram (ConeProjective Diagram t n m a
d Point a
_ FinList n a
_) = Diagram t n m a
d
cnDiagram (ConeInjective Diagram t n m a
d Point a
_ FinList n a
_)  = Diagram t n m a
d
cnDiagram (ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
d a
_)       = Diagram ('Parallel 'LeftToRight) ('S N1) m a
d
cnDiagram (ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m a
d a
_)     = Diagram ('Parallel 'RightToLeft) ('S N1) m a
d

--------------------------------------------------------------------------------
-- cnDiagramTypeRefl -

-- | reflexivity of the underlying diagram type.
cnDiagramTypeRefl :: Cone s p t n m a -> Dual (Dual t) :~: t
cnDiagramTypeRefl :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Dual t) :~: t
cnDiagramTypeRefl (ConeProjective Diagram t n m a
d Point a
_ FinList n a
_) = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Dual t) :~: t
dgTypeRefl Diagram t n m a
d
cnDiagramTypeRefl (ConeInjective Diagram t n m a
d Point a
_ FinList n a
_)  = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Dual t) :~: t
dgTypeRefl Diagram t n m a
d
cnDiagramTypeRefl (ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
d a
_)       = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Dual t) :~: t
dgTypeRefl Diagram ('Parallel 'LeftToRight) ('S N1) m a
d
cnDiagramTypeRefl (ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m a
d a
_)     = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Dual t) :~: t
dgTypeRefl Diagram ('Parallel 'RightToLeft) ('S N1) m a
d


--------------------------------------------------------------------------------
-- cnMap -

cnMapMltStruct :: Hom Mlt h => Struct Mlt b -> h a b
  -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMltStruct :: forall (h :: * -> * -> *) b a (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
Struct Mlt b -> h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMltStruct Struct Mlt b
Struct h a b
h Cone Mlt p t n m a
c = case Cone Mlt p t n m a
c of
  ConeProjective Diagram t n m a
d Point a
t FinList n a
as -> forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective (forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap h a b
h Diagram t n m a
d) (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a b
h Point a
t) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
h) FinList n a
as)
  ConeInjective Diagram t n m a
d Point a
t FinList n a
as -> forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective t n m a
ConeInjective (forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap h a b
h Diagram t n m a
d) (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a b
h Point a
t) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
h) FinList n a
as)

-- | mapping of a cone under a 'Multiplicative' homomorphism.
cnMapMlt :: Hom Mlt h => h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt :: forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt h a b
h = forall (h :: * -> * -> *) b a (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
Struct Mlt b -> h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMltStruct (forall s t x. Transformable s t => Struct s x -> Struct t x
tau forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h a b
h) h a b
h

cnMapDstStruct :: Hom Dst h => Struct Dst b -> h a b
  -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDstStruct :: forall (h :: * -> * -> *) b a (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
Struct Dst b -> h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDstStruct Struct Dst b
Struct h a b
h Cone Dst p t n m a
c = case Cone Dst p t n m a
c of
  ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
d a
a   -> forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel (forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap h a b
h Diagram ('Parallel 'LeftToRight) ('S N1) m a
d) (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
h a
a)
  ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m a
d a
a -> forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) ('S N1) m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) ('S N1) m a
ConeCokernel (forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap h a b
h Diagram ('Parallel 'RightToLeft) ('S N1) m a
d) (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
h a
a)

-- | mapping of a cone under a 'Distributive' homomorphism.
cnMapDst :: Hom Dst h => h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst :: forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst h a b
h = forall (h :: * -> * -> *) b a (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
Struct Dst b -> h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDstStruct (forall s t x. Transformable s t => Struct s x -> Struct t x
tau forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h a b
h) h a b
h

-- | mapping of a cone.
cnMap :: Hom s h => h a b -> Cone s p t n m a -> Cone s p t n m b
cnMap :: forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
Hom s h =>
h a b -> Cone s p t n m a -> Cone s p t n m b
cnMap h a b
h Cone s p t n m a
c = case Cone s p t n m a
c of
  ConeProjective Diagram t n m a
_ Point a
_ FinList n a
_ -> forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt h a b
h Cone s p t n m a
c
  ConeInjective Diagram t n m a
_ Point a
_ FinList n a
_  -> forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt h a b
h Cone s p t n m a
c
  ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
_ a
_       -> forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst h a b
h Cone s p t n m a
c
  ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m a
_ a
_     -> forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst h a b
h Cone s p t n m a
c
  
instance HomMultiplicative h => Applicative1 h (Cone Mlt p t n m) where
  amap1 :: forall a b. h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
amap1 = forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt

instance HomDistributive h => Applicative1 h (Cone Dst p t n m) where
  amap1 :: forall a b. h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
amap1 = forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst

--------------------------------------------------------------------------------
-- Cone - Dual -

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

--------------------------------------------------------------------------------
-- coCone -

-- | to the dual cone, with its inverse 'coConeInv'.
coCone :: Cone s p t n m a -> Dual (Cone s p t n m a)
coCone :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s p t n m a
c = case Cone s p t n m a
c of
  ConeProjective Diagram t n m a
d Point a
t FinList n a
as -> forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective t n m a
ConeInjective (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram Diagram t n m a
d) Point a
t (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op FinList n a
as)
  ConeInjective Diagram t n m a
d Point a
t FinList n a
as  -> forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram Diagram t n m a
d) Point a
t (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op FinList n a
as)
  ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
d a
a        -> forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) ('S N1) m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) ('S N1) m a
ConeCokernel (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram Diagram ('Parallel 'LeftToRight) ('S N1) m a
d) (forall x. x -> Op x
Op a
a)
  ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m a
d a
a      -> forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Diagram t n m a)
coDiagram Diagram ('Parallel 'RightToLeft) ('S N1) m a
d) (forall x. x -> Op x
Op a
a)

--------------------------------------------------------------------------------
-- cnFromOpOp -

-- | from @'Op' '.' 'Op'@.
cnFromOpOp :: ConeStruct s a -> Cone s p t n m (Op (Op a)) -> Cone s p t n m a
cnFromOpOp :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a -> Cone s p t n m (Op (Op a)) -> Cone s p t n m a
cnFromOpOp ConeStruct s a
ConeStructMlt = forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt forall a. Multiplicative a => IsoOp Mlt (Op (Op a)) a
isoFromOpOpMlt
cnFromOpOp ConeStruct s a
ConeStructDst = forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst forall a. Distributive a => IsoOp Dst (Op (Op a)) a
isoFromOpOpDst 

--------------------------------------------------------------------------------
-- coConeInv -

-- | from the dual cone, with its inverse 'coCone'.
coConeInv :: ConeStruct s a -> Dual (Dual p) :~: p -> Dual (Dual t) :~: t
  -> Dual (Cone s p t n m a) -> Cone s p t n m a
coConeInv :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Cone s p t n m a)
-> Cone s p t n m a
coConeInv ConeStruct s a
cs Dual (Dual p) :~: p
Refl Dual (Dual t) :~: t
Refl = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a -> Cone s p t n m (Op (Op a)) -> Cone s p t n m a
cnFromOpOp ConeStruct s a
cs forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone

--------------------------------------------------------------------------------
-- ConeDuality -

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

--------------------------------------------------------------------------------
-- cnToOp -

-- | to @__g__ ('Op' __a__)@.
cnToOp :: ConeDuality s f g a -> f a -> g (Op a)
cnToOp :: forall s (f :: * -> *) (g :: * -> *) a.
ConeDuality s f g a -> f a -> g (Op a)
cnToOp (ConeDuality ConeStruct s a
_ f a :~: Cone s p t n m a
Refl g (Op a) :~: Dual (Cone s p t n m a)
Refl Dual (Dual p) :~: p
_ Dual (Dual t) :~: t
_) = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone

--------------------------------------------------------------------------------
-- cnFromOp -

-- | from @__g__ ('Op' __a__)@.
cnFromOp :: ConeDuality s f g a -> g (Op a) -> f a
cnFromOp :: forall s (f :: * -> *) (g :: * -> *) a.
ConeDuality s f g a -> g (Op a) -> f a
cnFromOp (ConeDuality ConeStruct s a
cs f a :~: Cone s p t n m a
Refl g (Op a) :~: Dual (Cone s p t n m a)
Refl Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt) = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Cone s p t n m a)
-> Cone s p t n m a
coConeInv ConeStruct s a
cs Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt

--------------------------------------------------------------------------------
-- tip -

-- | the tip of a cone.
--
-- __Property__ Let @c@ be in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ for a
-- 'Oriented' structure then holds:
--
-- (1) If __@p@__ is equal to __'Projective'__ then holds:
-- @'start' ci '==' 'tip' c@ for all @ci@ in @'shell' c@.
--
-- (2) If __@p@__ is equal to __'Injective'__ then holds:
-- @'end' ci '==' 'tip' c@ for all @ci@ in @'shell' c@.
tip :: Cone s p t n m a -> Point a
tip :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone s p t n m a
c = case Cone s p t n m a
c of
  ConeProjective Diagram t n m a
_ Point a
t FinList n a
_ -> Point a
t
  ConeInjective Diagram t n m a
_ Point a
t FinList n a
_  -> Point a
t
  ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
_ a
k       -> forall q. Oriented q => q -> Point q
start a
k
  ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m a
_ a
k     -> forall q. Oriented q => q -> Point q
end a
k

--------------------------------------------------------------------------------
-- shell -

-- | the shell of a cone.
--
-- __Property__ Let @c@ be in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ for a
-- 'Oriented' structure then holds:
--
-- (1) If __@p@__ is equal to __'Projective'__ then holds:
-- @'fmap' 'end' ('shell' c) '==' 'cnPoints' c@.
--
-- (2) If __@p@__ is equal to __'Injective'__ then holds:
-- @'fmap' 'start' ('shell' c) '==' 'cnPoints' c@.
shell :: Cone s p t n m a -> FinList n a
shell :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell (ConeProjective Diagram t n m a
_ Point a
_ FinList n a
as) = FinList n a
as
shell (ConeInjective Diagram t n m a
_ Point a
_ FinList n a
as)  = FinList n a
as
shell (ConeKernel (DiagramParallelLR Point a
_ Point a
q FinList m a
_) a
k)     = a
kforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall a. Additive a => Root a -> a
zero (forall q. Oriented q => q -> Point q
start a
k forall p. p -> p -> Orientation p
:> Point a
q)forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall a. FinList N0 a
Nil
shell (ConeCokernel (DiagramParallelRL Point a
_ Point a
q FinList m a
_) a
k) =  a
kforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall a. Additive a => Root a -> a
zero (Point a
q forall p. p -> p -> Orientation p
:> forall q. Oriented q => q -> Point q
end a
k)forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall a. FinList N0 a
Nil

--------------------------------------------------------------------------------
-- cnPoints -

-- | the points of the underlying diagram, i.e. @'dgPoints' '.' 'cnDiagram'@. 
cnPoints :: Oriented a => Cone s p t n m a -> FinList n (Point a)
cnPoints :: forall a s (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
Oriented a =>
Cone s p t n m a -> FinList n (Point a)
cnPoints = forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram

--------------------------------------------------------------------------------
-- cnArrows -

-- | the arrows of the underlying diagram, i.e. @'dgArrows' '.' 'cnDiagram'@.
cnArrows :: Cone s p t n m a -> FinList m a
cnArrows :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList m a
cnArrows = forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram

--------------------------------------------------------------------------------
-- cnDstAdjZero -

-- | adjoins a 'zero' arrow to the diagram and the cone.
cnDstAdjZero :: Cone Dst p t n m a -> Cone Mlt p t n (m+1) a
cnDstAdjZero :: forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p t n m a -> Cone Mlt p t n (m + 1) a
cnDstAdjZero (ConeKernel d :: Diagram ('Parallel 'LeftToRight) ('S N1) m a
d@(DiagramParallelLR Point a
_ Point a
r FinList m a
_) a
k)
  = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective (forall a (n :: N') (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) n m a
-> Diagram ('Parallel 'LeftToRight) n (m + 1) a
dgPrlAdjZero Diagram ('Parallel 'LeftToRight) ('S N1) m a
d) Point a
t (a
kforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall a. Additive a => Root a -> a
zero (Point a
tforall p. p -> p -> Orientation p
:>Point a
r)forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall a. FinList N0 a
Nil) where t :: Point a
t = forall q. Oriented q => q -> Point q
start a
k
cnDstAdjZero c :: Cone Dst p t n m a
c@(ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m a
_ a
_)
  = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Cone s p t n m a)
-> Cone s p t n m a
coConeInv forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p t n m a -> Cone Mlt p t n (m + 1) a
cnDstAdjZero forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone Dst p t n m a
c

--------------------------------------------------------------------------------
-- ConeZeroHead -

-- | predicate for cones where the first arrow of its underlying diagram is equal to 'zero'.
newtype ConeZeroHead s p t n m a = ConeZeroHead (Cone s p t n m a) deriving (Int -> ConeZeroHead s p t n m a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Int -> ConeZeroHead s p t n m a -> ShowS
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
[ConeZeroHead s p t n m a] -> ShowS
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
ConeZeroHead s p t n m a -> String
showList :: [ConeZeroHead s p t n m a] -> ShowS
$cshowList :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
[ConeZeroHead s p t n m a] -> ShowS
show :: ConeZeroHead s p t n m a -> String
$cshow :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
ConeZeroHead s p t n m a -> String
showsPrec :: Int -> ConeZeroHead s p t n m a -> ShowS
$cshowsPrec :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Int -> ConeZeroHead s p t n m a -> ShowS
Show,ConeZeroHead s p t n m a -> ConeZeroHead s p t n m a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
ConeZeroHead s p t n m a -> ConeZeroHead s p t n m a -> Bool
/= :: ConeZeroHead s p t n m a -> ConeZeroHead s p t n m a -> Bool
$c/= :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
ConeZeroHead s p t n m a -> ConeZeroHead s p t n m a -> Bool
== :: ConeZeroHead s p t n m a -> ConeZeroHead s p t n m a -> Bool
$c== :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
ConeZeroHead s p t n m a -> ConeZeroHead s p t n m a -> Bool
Eq)

--------------------------------------------------------------------------------
-- ConeZeroHead - Validable -

instance Distributive a
  => Validable (ConeZeroHead s p d n (S m) a) where
  valid :: ConeZeroHead s p d n ('S m) a -> Statement
valid (ConeZeroHead Cone s p d n ('S m) a
c)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid Cone s p d n ('S m) a
c
          , forall a. Additive a => a -> Statement
relIsZero forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (n :: N') a. FinList (n + 1) a -> a
head forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone s p d n ('S m) a
c
          ]

instance ( Distributive a
         , Typeable s, Typeable p, Typeable t, Typeable n, Typeable m
         )
  => Entity (ConeZeroHead s p t n (S m) a)

--------------------------------------------------------------------------------
-- ConeZeroHead - Dual -

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

-- | to the dual, with its inverse 'coConeZeroHead'.
coConeZeroHead :: ConeZeroHead s p t n m a -> Dual (ConeZeroHead s p t n m a)
coConeZeroHead :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
ConeZeroHead s p t n m a -> Dual (ConeZeroHead s p t n m a)
coConeZeroHead (ConeZeroHead Cone s p t n m a
c) = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> ConeZeroHead s p t n m a
ConeZeroHead forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s p t n m a
c

-- | from the bidual.
czFromOpOp :: ConeStruct s a
  -> ConeZeroHead s p t n m (Op (Op a)) -> ConeZeroHead s p t n m a
czFromOpOp :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> ConeZeroHead s p t n m (Op (Op a)) -> ConeZeroHead s p t n m a
czFromOpOp ConeStruct s a
sa (ConeZeroHead Cone s p t n m (Op (Op a))
c) = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> ConeZeroHead s p t n m a
ConeZeroHead forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a -> Cone s p t n m (Op (Op a)) -> Cone s p t n m a
cnFromOpOp ConeStruct s a
sa Cone s p t n m (Op (Op a))
c

-- | from the dual, with its inverse 'coConeZeroHead'.
coConeZeroHeadInv :: ConeStruct s a -> Dual (Dual p) :~: p -> Dual (Dual t) :~: t
  -> Dual (ConeZeroHead s p t n m a) -> ConeZeroHead s p t n m a
coConeZeroHeadInv :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (ConeZeroHead s p t n m a)
-> ConeZeroHead s p t n m a
coConeZeroHeadInv ConeStruct s a
sa Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt (ConeZeroHead Cone s (Dual p) (Dual t) n m (Op a)
c)
  = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> ConeZeroHead s p t n m a
ConeZeroHead forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Cone s p t n m a)
-> Cone s p t n m a
coConeInv ConeStruct s a
sa Dual (Dual p) :~: p
rp Dual (Dual t) :~: t
rt Cone s (Dual p) (Dual t) n m (Op a)
c

--------------------------------------------------------------------------------
-- cnDiffHead -

-- | subtracts to every arrow of the underlying parallel diagram the first arrow and
-- adapts the shell accordingly.
cnDiffHead :: (Distributive a, Abelian a)
  => Cone Mlt p (Parallel d) n (m+1) a -> ConeZeroHead Mlt p (Parallel d)  n (m+1) a
cnDiffHead :: forall a (p :: Perspective) (d :: Direction) (n :: N') (m :: N').
(Distributive a, Abelian a) =>
Cone Mlt p ('Parallel d) n (m + 1) a
-> ConeZeroHead Mlt p ('Parallel d) n (m + 1) a
cnDiffHead (ConeProjective Diagram ('Parallel d) n (m + 1) a
d Point a
t (a
a:|FinList n a
as)) = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> ConeZeroHead s p t n m a
ConeZeroHead forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ case Diagram ('Parallel d) n (m + 1) a
d of
  DiagramParallelLR Point a
_ Point a
_ FinList (m + 1) a
_ -> forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective (forall a (d :: Direction) (n :: N') (m :: N').
Abelian a =>
Diagram ('Parallel d) n (m + 1) a
-> Diagram ('Parallel d) n (m + 1) a
dgPrlDiffHead Diagram ('Parallel d) n (m + 1) a
d) Point a
t (a
aforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {f} {a}. (Root f ~ Root a, Additive a, Fibred f) => f -> a
toZero FinList n a
as)
  DiagramParallelRL Point a
_ Point a
_ FinList (m + 1) a
_ -> forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective (forall a (d :: Direction) (n :: N') (m :: N').
Abelian a =>
Diagram ('Parallel d) n (m + 1) a
-> Diagram ('Parallel d) n (m + 1) a
dgPrlDiffHead Diagram ('Parallel d) n (m + 1) a
d) Point a
t (forall {f} {a}. (Root f ~ Root a, Additive a, Fibred f) => f -> a
toZero a
aforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|FinList n a
as)
  where toZero :: f -> a
toZero f
a = forall a. Additive a => Root a -> a
zero (forall f. Fibred f => f -> Root f
root f
a)
cnDiffHead c :: Cone Mlt p ('Parallel d) n (m + 1) a
c@(ConeInjective Diagram ('Parallel d) n (m + 1) a
d Point a
_ FinList n a
_) = case Diagram ('Parallel d) n (m + 1) a
d of
  DiagramParallelLR Point a
_ Point a
_ FinList (m + 1) a
_ ->   forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (ConeZeroHead s p t n m a)
-> ConeZeroHead s p t n m a
coConeZeroHeadInv forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl
                             forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (p :: Perspective) (d :: Direction) (n :: N') (m :: N').
(Distributive a, Abelian a) =>
Cone Mlt p ('Parallel d) n (m + 1) a
-> ConeZeroHead Mlt p ('Parallel d) n (m + 1) a
cnDiffHead forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone Mlt p ('Parallel d) n (m + 1) a
c
  DiagramParallelRL Point a
_ Point a
_ FinList (m + 1) a
_ ->   forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (ConeZeroHead s p t n m a)
-> ConeZeroHead s p t n m a
coConeZeroHeadInv forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl
                             forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (p :: Perspective) (d :: Direction) (n :: N') (m :: N').
(Distributive a, Abelian a) =>
Cone Mlt p ('Parallel d) n (m + 1) a
-> ConeZeroHead Mlt p ('Parallel d) n (m + 1) a
cnDiffHead forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone Mlt p ('Parallel d) n (m + 1) a
c

--------------------------------------------------------------------------------
-- cnZeroHead -

-- | embedding of a cone in a distributive structure to its multiplicative cone.
cnZeroHead :: Cone Dst p t n m a -> ConeZeroHead Mlt p t n (m+1) a
cnZeroHead :: forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p t n m a -> ConeZeroHead Mlt p t n (m + 1) a
cnZeroHead = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> ConeZeroHead s p t n m a
ConeZeroHead forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p t n m a -> Cone Mlt p t n (m + 1) a
cnDstAdjZero 

--------------------------------------------------------------------------------
-- cnKernel -

-- | the kernel cone of a zero headed parallel cone, i.e. the inverse of 'cnZeroHead'.
cnKernel :: (Distributive a, p ~ Projective, t ~ Parallel LeftToRight)
  => ConeZeroHead Mlt p t n (m+1) a -> Cone Dst p t n m a
cnKernel :: forall a (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(Distributive a, p ~ 'Projective, t ~ 'Parallel 'LeftToRight) =>
ConeZeroHead Mlt p t n (m + 1) a -> Cone Dst p t n m a
cnKernel (ConeZeroHead (ConeProjective Diagram t n (m + 1) a
d Point a
_ FinList n a
cs)) = case Diagram t n (m + 1) a
d of
  DiagramParallelLR Point a
l Point a
r FinList (m + 1) a
as -> forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel (forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR Point a
l Point a
r (forall (n :: N') a. FinList (n + 1) a -> FinList n a
tail FinList (m + 1) a
as)) (forall (n :: N') a. FinList (n + 1) a -> a
head FinList n a
cs)

--------------------------------------------------------------------------------
-- cnCokernel

-- | the cokernel cone of a zero headed parallel cone, i.e. the inverse of 'cnZeroHead'.
cnCokernel :: (Distributive a, p ~ Injective, t ~ Parallel RightToLeft)
  => ConeZeroHead Mlt p t n (m+1) a -> Cone Dst p t n m a
cnCokernel :: forall a (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(Distributive a, p ~ 'Injective, t ~ 'Parallel 'RightToLeft) =>
ConeZeroHead Mlt p t n (m + 1) a -> Cone Dst p t n m a
cnCokernel = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (Cone s p t n m a)
-> Cone s p t n m a
coConeInv forall a. Distributive a => ConeStruct Dst a
ConeStructDst forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(Distributive a, p ~ 'Projective, t ~ 'Parallel 'LeftToRight) =>
ConeZeroHead Mlt p t n (m + 1) a -> Cone Dst p t n m a
cnKernel forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
ConeZeroHead s p t n m a -> Dual (ConeZeroHead s p t n m a)
coConeZeroHead

--------------------------------------------------------------------------------
-- relConePrjMlt -

prm :: N -> Message
prm :: N -> Message
prm N
i = [Parameter] -> Message
Params[String
"i"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
i]

lE, lS, lO, lC, lB :: Label
lE :: Label
lE = String -> Label
Label String
"end"
lS :: Label
lS = String -> Label
Label String
"start"
lO :: Label
lO = String -> Label
Label String
"orientation"
lC :: Label
lC = String -> Label
Label String
"commutative"
lB :: Label
lB = String -> Label
Label String
"bound"

tp2 :: FinList N2 a -> (a,a)
tp2 :: forall a. FinList ('S N1) a -> (a, a)
tp2 (a
a:|a
b:|FinList n a
Nil) = (a
a,a
b)

ht :: FinList (n+1) a -> (a,FinList n a)
ht :: forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht (a
x:|FinList n a
xs) = (a
x,FinList n a
xs)

relConePrjMlt :: Multiplicative a
  => Diagram t n m a -> Point a -> FinList n a -> Statement
relConePrjMlt :: forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a -> Point a -> FinList n a -> Statement
relConePrjMlt Diagram t n m a
DiagramEmpty Point a
t FinList n a
Nil = forall a. Validable a => a -> Statement
valid Point a
t

relConePrjMlt (DiagramDiscrete FinList n (Point a)
ps) Point a
t FinList n a
cs = forall a. Validable a => a -> Statement
valid Point a
t forall b. Boolean b => b -> b -> b
&& forall a (n :: N').
Multiplicative a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vld N
0 Point a
t FinList n (Point a)
ps FinList n a
cs where
  vld :: Multiplicative a => N -> Point a -> FinList n (Point a) -> FinList n a
         -> Statement
  vld :: forall a (n :: N').
Multiplicative a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vld N
_ Point a
_ FinList n (Point a)
Nil FinList n a
Nil = Statement
SValid
  vld N
i Point a
t (Point a
p:|FinList n (Point a)
ps) (a
c:|FinList n a
cs)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid Point a
p
          , forall a. Validable a => a -> Statement
valid a
c
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
c forall a. Eq a => a -> a -> Bool
== Point a
t forall p. p -> p -> Orientation p
:> Point a
p) Bool -> Message -> Statement
:?> N -> Message
prm N
i
          , forall a (n :: N').
Multiplicative a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vld (forall a. Enum a => a -> a
succ N
i) Point a
t FinList n (Point a)
ps FinList n a
cs
          ]

relConePrjMlt (DiagramChainTo Point a
l FinList m a
as) Point a
t FinList n a
cs = forall a. Validable a => a -> Statement
valid a
cl forall b. Boolean b => b -> b -> b
&& forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld N
0 Point a
l FinList m a
as Point a
t a
cl FinList m a
cs' where
  (a
cl,FinList m a
cs') = forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht FinList n a
cs
  vld :: Multiplicative a
    => N -> Point a -> FinList m a -> Point a -> a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld N
i Point a
l FinList m a
Nil Point a
t a
cl FinList m a
Nil
    = Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
cl forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>Point a
l)Bool -> Message -> Statement
:?>N -> Message
prm N
i
  vld N
i Point a
l (a
a:|FinList n a
as) Point a
t a
cl (a
c:|FinList n a
cs)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
          , forall a. Validable a => a -> Statement
valid a
c
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Point q
end a
a forall a. Eq a => a -> a -> Bool
== Point a
l)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
c forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>forall q. Oriented q => q -> Point q
start a
a)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aforall c. Multiplicative c => c -> c -> c
*a
c forall a. Eq a => a -> a -> Bool
== a
cl)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld (forall a. Enum a => a -> a
succ N
i) (forall q. Oriented q => q -> Point q
start a
a) FinList n a
as Point a
t a
c FinList n a
cs 
          ]

relConePrjMlt (DiagramChainFrom Point a
l FinList m a
as) Point a
t FinList n a
cs = forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld N
0 Point a
l FinList m a
as Point a
t a
cl FinList m a
cs' where
  (a
cl,FinList m a
cs') = forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht FinList n a
cs
  vld :: Multiplicative a
    => N -> Point a -> FinList m a -> Point a -> a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld N
i Point a
l FinList m a
Nil Point a
t a
cl FinList m a
Nil
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
cl
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
cl forall a. Eq a => a -> a -> Bool
== Point a
t forall p. p -> p -> Orientation p
:> Point a
l)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          ]
  vld N
i Point a
l (a
a:|FinList n a
as) Point a
t a
cl (a
c:|FinList n a
cs)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
          , forall a. Validable a => a -> Statement
valid a
cl
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Point q
start a
a forall a. Eq a => a -> a -> Bool
== Point a
l)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
cl forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>forall q. Oriented q => q -> Point q
start a
a)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aforall c. Multiplicative c => c -> c -> c
*a
cl forall a. Eq a => a -> a -> Bool
== a
c)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld (forall a. Enum a => a -> a
succ N
i) (forall q. Oriented q => q -> Point q
end a
a) FinList n a
as Point a
t a
c FinList n a
cs
          ]

relConePrjMlt (DiagramParallelLR Point a
p Point a
q FinList m a
as) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
cp
        , forall a. Validable a => a -> Statement
valid a
cq
        , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
cp forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>Point a
p)Bool -> Message -> Statement
:?>N -> Message
prm N
0
        , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
cq forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>Point a
q)Bool -> Message -> Statement
:?>N -> Message
prm N
1
        , forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld N
0 (Point a
pforall p. p -> p -> Orientation p
:>Point a
q) FinList m a
as a
cp a
cq
        ] where
  (a
cp,a
cq) = forall a. FinList ('S N1) a -> (a, a)
tp2 FinList n a
cs
  vld :: Multiplicative a => N -> Orientation (Point a)
    -> FinList m a -> a -> a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld N
_ Orientation (Point a)
_ FinList m a
Nil a
_ a
_ = Statement
SValid
  vld N
i Orientation (Point a)
o (a
a:|FinList n a
as) a
cp a
cq
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
a forall a. Eq a => a -> a -> Bool
== Orientation (Point a)
o)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aforall c. Multiplicative c => c -> c -> c
*a
cp forall a. Eq a => a -> a -> Bool
== a
cq)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld (forall a. Enum a => a -> a
succ N
i) Orientation (Point a)
o FinList n a
as a
cp a
cq
          ]
relConePrjMlt (DiagramParallelRL Point a
p Point a
q FinList m a
as) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
cp
        , forall a. Validable a => a -> Statement
valid a
cq
        , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
cp forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>Point a
p)Bool -> Message -> Statement
:?>N -> Message
prm N
0
        , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
cq forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>Point a
q)Bool -> Message -> Statement
:?>N -> Message
prm N
1
        , forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld N
0 (Point a
qforall p. p -> p -> Orientation p
:>Point a
p) FinList m a
as a
cp a
cq
        ] where
  (a
cp,a
cq) = forall a. FinList ('S N1) a -> (a, a)
tp2 FinList n a
cs
  vld :: Multiplicative a => N -> Orientation (Point a)
    -> FinList n a -> a -> a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld N
_ Orientation (Point a)
_ FinList n a
Nil a
_ a
_ = Statement
SValid
  vld N
i Orientation (Point a)
o (a
a:|FinList n a
as) a
cp a
cq
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
a forall a. Eq a => a -> a -> Bool
== Orientation (Point a)
o)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aforall c. Multiplicative c => c -> c -> c
*a
cq forall a. Eq a => a -> a -> Bool
== a
cp)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld (forall a. Enum a => a -> a
succ N
i) Orientation (Point a)
o FinList n a
as a
cp a
cq
          ]

relConePrjMlt (DiagramSource Point a
s FinList m a
as) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
c0
        , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
c0 forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>Point a
s)Bool -> Message -> Statement
:?>N -> Message
prm N
0
        , forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld N
0 Point a
t Point a
s FinList m a
as a
c0 FinList m a
cs'
        ] where
  (a
c0,FinList m a
cs')  = forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht FinList n a
cs 
  vld :: Multiplicative a => N -> Point a -> Point a
         -> FinList m a -> a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld N
_ Point a
_ Point a
_ FinList m a
Nil a
_ FinList m a
Nil = Statement
SValid
  vld N
i Point a
t Point a
s (a
a:|FinList n a
as) a
c0 (a
c:|FinList n a
cs)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
          , Label
lS Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Point q
start a
a forall a. Eq a => a -> a -> Bool
== Point a
s)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
c forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>forall q. Oriented q => q -> Point q
end a
a)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aforall c. Multiplicative c => c -> c -> c
*a
c0 forall a. Eq a => a -> a -> Bool
== a
c)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld (forall a. Enum a => a -> a
succ N
i) Point a
t Point a
s FinList n a
as a
c0 FinList n a
cs
          ]

relConePrjMlt (DiagramSink Point a
e FinList m a
as) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
c0
        , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
c0 forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>Point a
e)Bool -> Message -> Statement
:?>N -> Message
prm N
0
        , forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld N
0 Point a
t Point a
e FinList m a
as a
c0 FinList m a
cs'
        ] where
  (a
c0,FinList m a
cs') = forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht FinList n a
cs
  vld :: Multiplicative a => N -> Point a -> Point a
         -> FinList m a -> a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld N
_ Point a
_ Point a
_ FinList m a
Nil a
_ FinList m a
Nil = Statement
SValid
  vld N
i Point a
t Point a
e (a
a:|FinList n a
as) a
c0 (a
c:|FinList n a
cs)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
          , Label
lE Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Point q
end a
a forall a. Eq a => a -> a -> Bool
== Point a
e)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
c forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>forall q. Oriented q => q -> Point q
start a
a)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aforall c. Multiplicative c => c -> c -> c
*a
c forall a. Eq a => a -> a -> Bool
== a
c0)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld (forall a. Enum a => a -> a
succ N
i) Point a
t Point a
e FinList n a
as a
c0 FinList n a
cs
          ]
relConePrjMlt (DiagramGeneral FinList n (Point a)
ps FinList m (a, Orientation N)
aijs) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ forall a (n :: N').
Oriented a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vldO N
0 Point a
t FinList n (Point a)
ps FinList n a
cs
        , forall a (m :: N').
Multiplicative a =>
N -> Array N a -> FinList m (a, Orientation N) -> Statement
vldC N
0 (forall (n :: N') a. FinList n a -> Array N a
toArray FinList n a
cs) FinList m (a, Orientation N)
aijs
        ] where
  vldO :: Oriented a => N -> Point a
    -> FinList n (Point a) -> FinList n a -> Statement
  vldO :: forall a (n :: N').
Oriented a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vldO N
_ Point a
_ FinList n (Point a)
Nil FinList n a
Nil = Statement
SValid
  vldO N
i Point a
t (Point a
p:|FinList n (Point a)
ps) (a
c:|FinList n a
cs)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
c
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
c forall a. Eq a => a -> a -> Bool
== Point a
tforall p. p -> p -> Orientation p
:>Point a
p)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , forall a (n :: N').
Oriented a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vldO (forall a. Enum a => a -> a
succ N
i) Point a
t FinList n (Point a)
ps FinList n a
cs
          ]

  vldC :: Multiplicative a => N -> Array N a
    -> FinList m (a,Orientation N) -> Statement
  vldC :: forall a (m :: N').
Multiplicative a =>
N -> Array N a -> FinList m (a, Orientation N) -> Statement
vldC N
_ Array N a
_ FinList m (a, Orientation N)
Nil = Statement
SValid
  vldC N
l Array N a
cs ((a
a,N
i:>N
j):|FinList n (a, Orientation N)
aijs)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
a
          , Label
lB Label -> Statement -> Statement
:<=>: (forall a. Ix a => (a, a) -> a -> Bool
inRange (forall i e. Array i e -> (i, i)
bounds Array N a
cs) N
i) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
l,String
"i"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
i]
          , Label
lB Label -> Statement -> Statement
:<=>: (forall a. Ix a => (a, a) -> a -> Bool
inRange (forall i e. Array i e -> (i, i)
bounds Array N a
cs) N
j) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
l,String
"j"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
j]
          , Label
lO Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation a
a forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
end a
ci forall p. p -> p -> Orientation p
:> forall q. Oriented q => q -> Point q
end a
cj)
                     Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
l,String
"(i,j)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
i,N
j)]
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aforall c. Multiplicative c => c -> c -> c
*a
ci forall a. Eq a => a -> a -> Bool
== a
cj)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show N
l,String
"(i,j)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (N
i,N
j)]
          , forall a (m :: N').
Multiplicative a =>
N -> Array N a -> FinList m (a, Orientation N) -> Statement
vldC (forall a. Enum a => a -> a
succ N
l) Array N a
cs FinList n (a, Orientation N)
aijs
          ] where ci :: a
ci = Array N a
cs forall i e. Ix i => Array i e -> i -> e
! N
i
                  cj :: a
cj = Array N a
cs forall i e. Ix i => Array i e -> i -> e
! N
j


--------------------------------------------------------------------------------
-- relCone -

-- | validity of a 'Cone'.
relCone :: Cone s p t n m a -> Statement
relCone :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Statement
relCone (ConeProjective Diagram t n m a
d Point a
t FinList n a
cs) = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a -> Point a -> FinList n a -> Statement
relConePrjMlt Diagram t n m a
d Point a
t FinList n a
cs
relCone c :: Cone s p t n m a
c@(ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
_ a
_)      = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Statement
relCone (forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p t n m a -> Cone Mlt p t n (m + 1) a
cnDstAdjZero Cone s p t n m a
c)
relCone Cone s p t n m a
c                       = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Statement
relCone (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s p t n m a
c)

--------------------------------------------------------------------------------
-- Cone - Validable -

instance Validable (Cone s p t n m a) where
  valid :: Cone s p t n m a -> Statement
valid Cone s p t n m a
c = String -> Label
Label String
"Cone" Label -> Statement -> Statement
:<=>: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Statement
relCone Cone s p t n m a
c 

--------------------------------------------------------------------------------
-- Cone - Entity -

deriving instance Show (Cone s p t n m a)
deriving instance Eq (Cone s p t n m a)

instance ( Typeable s, Typeable p, Typeable t, Typeable n, Typeable m, Typeable a
         ) => Entity (Cone s p t n m a)


--------------------------------------------------------------------------------
-- Cone - Oriented -

instance (Oriented a, Typeable s, Typeable p, Typeable d, Typeable m)
  => Oriented (Cone s p (Parallel d) N2 m a) where
  type Point (Cone s p (Parallel d) N2 m a) = Point a
  orientation :: Cone s p ('Parallel d) ('S N1) m a
-> Orientation (Point (Cone s p ('Parallel d) ('S N1) m a))
orientation Cone s p ('Parallel d) ('S N1) m a
c = forall q. Oriented q => q -> Orientation (Point q)
orientation forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone s p ('Parallel d) ('S N1) m a
c
  
--------------------------------------------------------------------------------
-- cnPrjOrnt -

-- | the projective cone on 'Orientation' with the underlying given diagram and tip with the given
-- point. 
cnPrjOrnt :: Entity p
  => p -> Diagram t n m (Orientation p) -> Cone Mlt Projective t n m (Orientation p)
cnPrjOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p
-> Diagram t n m (Orientation p)
-> Cone Mlt 'Projective t n m (Orientation p)
cnPrjOrnt p
p Diagram t n m (Orientation p)
d = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram t n m (Orientation p)
d p
p (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (p
pforall p. p -> p -> Orientation p
:>) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m (Orientation p)
d)

cnPrjDstOrnt :: (Entity p, t ~ Parallel LeftToRight, n ~ N2)
  => p -> Diagram t n m (Orientation p) -> Cone Dst Projective t n m (Orientation p)
cnPrjDstOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N').
(Entity p, t ~ 'Parallel 'LeftToRight, n ~ 'S N1) =>
p
-> Diagram t n m (Orientation p)
-> Cone Dst 'Projective t n m (Orientation p)
cnPrjDstOrnt p
t d :: Diagram t n m (Orientation p)
d@(DiagramParallelLR Point (Orientation p)
p Point (Orientation p)
_ FinList m (Orientation p)
_) = forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel Diagram t n m (Orientation p)
d (p
tforall p. p -> p -> Orientation p
:>Point (Orientation p)
p)

--------------------------------------------------------------------------------
-- cnInjOrnt -

-- | the injective cone on 'Orientation' with the underlying given diagram and tip with the given
-- point. 
cnInjOrnt :: Entity p
  => p -> Diagram t n m (Orientation p) -> Cone Mlt Injective t n m (Orientation p)
cnInjOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p
-> Diagram t n m (Orientation p)
-> Cone Mlt 'Injective t n m (Orientation p)
cnInjOrnt p
p Diagram t n m (Orientation p)
d = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective t n m a
ConeInjective Diagram t n m (Orientation p)
d p
p (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall p. p -> p -> Orientation p
:>p
p) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m (Orientation p)
d)

cnInjDstOrnt :: (Entity p, t ~ Parallel RightToLeft, n ~ N2)
  => p -> Diagram t n m (Orientation p) -> Cone Dst Injective t n m (Orientation p)
cnInjDstOrnt :: forall p (t :: DiagramType) (n :: N') (m :: N').
(Entity p, t ~ 'Parallel 'RightToLeft, n ~ 'S N1) =>
p
-> Diagram t n m (Orientation p)
-> Cone Dst 'Injective t n m (Orientation p)
cnInjDstOrnt p
t d :: Diagram t n m (Orientation p)
d@(DiagramParallelRL Point (Orientation p)
_ Point (Orientation p)
q FinList m (Orientation p)
_) = forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) ('S N1) m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) ('S N1) m a
ConeCokernel Diagram t n m (Orientation p)
d (Point (Orientation p)
qforall p. p -> p -> Orientation p
:>p
t)
  
instance ( Entity p
         , XStandard p, XStandard (Diagram t n m (Orientation p))
         ) => XStandard (Cone Mlt Projective t n m (Orientation p)) where
  xStandard :: X (Cone Mlt 'Projective t n m (Orientation p))
xStandard = do
    Diagram t n m (Orientation p)
dg <- forall x. XStandard x => X x
xStandard
    p
p  <- forall x. XStandard x => X x
xStandard
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p
-> Diagram t n m (Orientation p)
-> Cone Mlt 'Projective t n m (Orientation p)
cnPrjOrnt p
p Diagram t n m (Orientation p)
dg)

instance ( Entity p, t ~ Parallel LeftToRight, n ~ N2
         , XStandard p, XStandard (Diagram t n m (Orientation p))
         ) => XStandard (Cone Dst Projective t n m (Orientation p)) where
  xStandard :: X (Cone Dst 'Projective t n m (Orientation p))
xStandard = do
    Diagram t n m (Orientation p)
dg <- forall x. XStandard x => X x
xStandard
    p
t  <- forall x. XStandard x => X x
xStandard
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall p (t :: DiagramType) (n :: N') (m :: N').
(Entity p, t ~ 'Parallel 'LeftToRight, n ~ 'S N1) =>
p
-> Diagram t n m (Orientation p)
-> Cone Dst 'Projective t n m (Orientation p)
cnPrjDstOrnt p
t Diagram t n m (Orientation p)
dg)
                                 
instance ( Entity p
         , XStandard p, XStandard (Diagram t n m (Orientation p))
         ) => XStandard (Cone Mlt Injective t n m (Orientation p)) where
  xStandard :: X (Cone Mlt 'Injective t n m (Orientation p))
xStandard = do
    Diagram t n m (Orientation p)
dg <- forall x. XStandard x => X x
xStandard
    p
p  <- forall x. XStandard x => X x
xStandard
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p
-> Diagram t n m (Orientation p)
-> Cone Mlt 'Injective t n m (Orientation p)
cnInjOrnt p
p Diagram t n m (Orientation p)
dg)

instance ( Entity p, t ~ Parallel RightToLeft, n ~ N2
         , XStandard p, XStandard (Diagram t n m (Orientation p))
         ) => XStandard (Cone Dst Injective t n m (Orientation p)) where
  xStandard :: X (Cone Dst 'Injective t n m (Orientation p))
xStandard = do
    Diagram t n m (Orientation p)
dg <- forall x. XStandard x => X x
xStandard
    p
t  <- forall x. XStandard x => X x
xStandard
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall p (t :: DiagramType) (n :: N') (m :: N').
(Entity p, t ~ 'Parallel 'RightToLeft, n ~ 'S N1) =>
p
-> Diagram t n m (Orientation p)
-> Cone Dst 'Injective t n m (Orientation p)
cnInjDstOrnt p
t Diagram t n m (Orientation p)
dg)

--------------------------------------------------------------------------------
-- cnChain -

-- | predicate for a factor with 'end' point at the starting point of the given chain.
--
-- __Property__
--
-- (1) Let @'FactorChain' f d@ be in @'FactorChain' 'To'  __n__ __a__@
-- for a 'Multiplicative' structure @__a__@ then holds:
-- @'end' f '==' 'chnToStart' d@.
--
-- (2) Let @'FactorChain' f d@ be in @'FactorChain' 'From'  __n__ __a__@
-- for a 'Multiplicative' structure @__a__@ then holds:
-- @'end' f '==' 'chnFromStart' d@.
data FactorChain s n a = FactorChain a (Diagram (Chain s) (n+1) n a)
  deriving (Int -> FactorChain s n a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (s :: Site) (n :: N') a.
Oriented a =>
Int -> FactorChain s n a -> ShowS
forall (s :: Site) (n :: N') a.
Oriented a =>
[FactorChain s n a] -> ShowS
forall (s :: Site) (n :: N') a.
Oriented a =>
FactorChain s n a -> String
showList :: [FactorChain s n a] -> ShowS
$cshowList :: forall (s :: Site) (n :: N') a.
Oriented a =>
[FactorChain s n a] -> ShowS
show :: FactorChain s n a -> String
$cshow :: forall (s :: Site) (n :: N') a.
Oriented a =>
FactorChain s n a -> String
showsPrec :: Int -> FactorChain s n a -> ShowS
$cshowsPrec :: forall (s :: Site) (n :: N') a.
Oriented a =>
Int -> FactorChain s n a -> ShowS
Show,FactorChain s n a -> FactorChain s n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (s :: Site) (n :: N') a.
Oriented a =>
FactorChain s n a -> FactorChain s n a -> Bool
/= :: FactorChain s n a -> FactorChain s n a -> Bool
$c/= :: forall (s :: Site) (n :: N') a.
Oriented a =>
FactorChain s n a -> FactorChain s n a -> Bool
== :: FactorChain s n a -> FactorChain s n a -> Bool
$c== :: forall (s :: Site) (n :: N') a.
Oriented a =>
FactorChain s n a -> FactorChain s n a -> Bool
Eq)

instance Oriented a => Validable (FactorChain To n a) where
  valid :: FactorChain 'To n a -> Statement
valid (FactorChain a
f Diagram ('Chain 'To) (n + 1) n a
d)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
f
          , forall a. Validable a => a -> Statement
valid Diagram ('Chain 'To) (n + 1) n a
d
          , forall q. Oriented q => q -> Point q
end a
f forall a. Eq a => a -> a -> Statement
.==. forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart Diagram ('Chain 'To) (n + 1) n a
d
          ]

instance Oriented a => Validable (FactorChain From n a) where
  valid :: FactorChain 'From n a -> Statement
valid (FactorChain a
f Diagram ('Chain 'From) (n + 1) n a
d)
    = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid a
f
          , forall a. Validable a => a -> Statement
valid Diagram ('Chain 'From) (n + 1) n a
d
          , forall q. Oriented q => q -> Point q
end a
f forall a. Eq a => a -> a -> Statement
.==. forall (n :: N') (m :: N') a.
Diagram ('Chain 'From) n m a -> Point a
chnFromStart Diagram ('Chain 'From) (n + 1) n a
d
          ]

instance (Multiplicative a, Typeable n) => Entity (FactorChain To n a)
instance (Multiplicative a, Typeable n) => Entity (FactorChain From n a)

--------------------------------------------------------------------------------
-- cnPrjChainTo

-- | the induced 'Projective' cone with ending factor given by the given 'FactorChain'.
--
-- __Property__ Let @h = 'FactorChain' f d@ be in
-- @'FactorChain' 'To' __n__ __a__@ for a 'Multiplicative' structure @__a__@ and
-- @'ConeProjective' d' _ (_':|'..':|'c':|''Nil') = 'cnPrjChainTo' h@ then holds:
-- @d' '==' d@ and @c '==' f@.
cnPrjChainTo :: Multiplicative a
  => FactorChain To n a -> Cone Mlt Projective (Chain To) (n+1) n a
cnPrjChainTo :: forall a (n :: N').
Multiplicative a =>
FactorChain 'To n a
-> Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
cnPrjChainTo (FactorChain a
f d :: Diagram ('Chain 'To) (n + 1) n a
d@(DiagramChainTo Point a
_ FinList n a
as))
  = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram ('Chain 'To) (n + 1) n a
d (forall q. Oriented q => q -> Point q
start a
f) (forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp a
f FinList n a
as) where
  cmp :: Multiplicative a => a -> FinList n a -> FinList (n+1) a
  cmp :: forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp a
f FinList n a
Nil     = a
fforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall a. FinList N0 a
Nil
  cmp a
f (a
a:|FinList n a
as) = (a
aforall c. Multiplicative c => c -> c -> c
*a
c)forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|FinList (n + 1) a
cs where cs :: FinList (n + 1) a
cs@(a
c:|FinList n a
_) = forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp a
f FinList n a
as

--------------------------------------------------------------------------------
-- cnPrjChainToInv -

-- | the underlying factor chain of a projective chain to cone, i.e the inverse of
-- 'cnPrjChainToInv'.
cnPrjChainToInv :: Cone Mlt Projective (Chain To) (n+1) n a -> FactorChain To n a
cnPrjChainToInv :: forall (n :: N') a.
Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
-> FactorChain 'To n a
cnPrjChainToInv (ConeProjective Diagram ('Chain 'To) (n + 1) n a
d Point a
_ FinList (n + 1) a
cs) = forall (s :: Site) (n :: N') a.
a -> Diagram ('Chain s) (n + 1) n a -> FactorChain s n a
FactorChain (forall (n :: N') a. FinList (n + 1) a -> a
f FinList (n + 1) a
cs) Diagram ('Chain 'To) (n + 1) n a
d where
  f :: FinList (n+1) a -> a
  f :: forall (n :: N') a. FinList (n + 1) a -> a
f (a
c:|FinList n a
Nil)       = a
c
  f (a
_:|cs :: FinList n a
cs@(a
_:|FinList n a
_)) = forall (n :: N') a. FinList (n + 1) a -> a
f FinList n a
cs

--------------------------------------------------------------------------------
-- chPrjChainFrom -

-- | the induced 'Projective' cone with starting factor given by the given 'FactorChain'.
--
-- __Property__ Let @h = 'FactorChain' f d@ be in
-- @'FactorChain' 'From' __n__ __a__@ for a 'Multiplicative' structure @__a__@ and
-- @'ConeProjective' d' _ (c':|'_) = 'cnPrjChainFrom' h@ then holds:
-- @d' '==' d@ and @c '==' f@.
cnPrjChainFrom :: Multiplicative a
  => FactorChain From n a -> Cone Mlt Projective (Chain From) (n+1) n a
cnPrjChainFrom :: forall a (n :: N').
Multiplicative a =>
FactorChain 'From n a
-> Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
cnPrjChainFrom (FactorChain a
f d :: Diagram ('Chain 'From) (n + 1) n a
d@(DiagramChainFrom Point a
_ FinList n a
as))
  = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram ('Chain 'From) (n + 1) n a
d (forall q. Oriented q => q -> Point q
start a
f) (forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp a
f FinList n a
as) where
  cmp :: Multiplicative a => a -> FinList n a -> FinList (n+1) a
  cmp :: forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp a
f FinList n a
Nil     = a
fforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall a. FinList N0 a
Nil
  cmp a
f (a
a:|FinList n a
as) = a
f forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList (n + 1) a
cmp a
f' FinList n a
as where f' :: a
f' = a
aforall c. Multiplicative c => c -> c -> c
*a
f

--------------------------------------------------------------------------------
-- cnPrjChainFromInv -

-- | the underlying factor chain of a projective chain from cone, i.e. the inverse of
-- 'cnPrjChainFrom'.
cnPrjChainFromInv :: Cone Mlt Projective (Chain From) (n+1) n a -> FactorChain From n a
cnPrjChainFromInv :: forall (n :: N') a.
Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
-> FactorChain 'From n a
cnPrjChainFromInv (ConeProjective Diagram ('Chain 'From) (n + 1) n a
d Point a
_ (a
c:|FinList n a
_)) = forall (s :: Site) (n :: N') a.
a -> Diagram ('Chain s) (n + 1) n a -> FactorChain s n a
FactorChain a
c Diagram ('Chain 'From) (n + 1) n a
d