{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}

-- |
-- Module      : OAlg.Limes.KernelsAndCokernels
-- Description : kernels and cokernels
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- kernels and cokernels, i.e. limits in a 'Distributive' structure of @'Diagram' ('Parallel' __d__)@
-- making all arrows 'zero'.
module OAlg.Limes.KernelsAndCokernels
  (
    -- * Kernels
    Kernels, Kernel, KernelCone, KernelDiagram
  , kernelFactor
  , kernelDiagram

    -- ** Construction
  , kernels, kernels0, kernels1
  , krnEqls, eqlKrns
  , kernelZero

    -- *** Orientation
  , kernelsOrnt

    -- * Cokernels
  , Cokernels, Cokernel, CokernelCone, CokernelDiagram
  , cokernelFactor
  , cokernelDiagram

    -- ** Construction
  , cokernels, cokernels'

    -- *** Orientation
  , cokernelsOrnt

    -- * Duality
  , krnLimesDuality, cokrnLimesDuality

    -- * Proposition
  , prpIsKernel, prpIsCokernel
  )
  where

import Data.Typeable

import OAlg.Prelude

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

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

import OAlg.Limes.Cone
import OAlg.Limes.Definition
import OAlg.Limes.Limits
import OAlg.Limes.EqualizersAndCoequalizers

--------------------------------------------------------------------------------
-- Kernels -

-- | 'Diagram' for a kernel.
type KernelDiagram n = Diagram (Parallel LeftToRight) N2 n

-- | 'Cone' for a kernel.
type KernelCone n = Cone Dst Projective (Parallel LeftToRight) N2 n

-- | kernel as a 'Limes'.
type Kernel n = Limes Dst Projective (Parallel LeftToRight) N2 n

-- | kernels for 'Distributive' structures.
type Kernels n       = Limits Dst Projective (Parallel LeftToRight) N2 n

--------------------------------------------------------------------------------
-- kernelFactor -

-- | the factor of its shell.
kernelFactor :: KernelCone N1 c -> c
kernelFactor :: forall c. KernelCone N1 c -> c
kernelFactor (ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 c
_ c
f) = c
f

--------------------------------------------------------------------------------
-- kernelDiagram -

-- | the kernel diagram of a given factor.
kernelDiagram :: Oriented c => c -> KernelDiagram N1 c
kernelDiagram :: forall c. Oriented c => c -> KernelDiagram N1 c
kernelDiagram c
f = forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) N2 m a
DiagramParallelLR (forall q. Oriented q => q -> Point q
start c
f) (forall q. Oriented q => q -> Point q
end c
f) (c
fforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)

--------------------------------------------------------------------------------
-- kernelZero -

-- | the kernel of the 'zero' factor given by the orientation, i.e. 'one'
kernelZero :: Distributive c => p c -> Orientation (Point c) -> Kernel N1 c
kernelZero :: forall c (p :: * -> *).
Distributive c =>
p c -> Orientation (Point c) -> Kernel N1 c
kernelZero p c
_ Orientation (Point c)
o = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 c
oKer forall c. KernelCone N1 c -> c
kernelFactor where
  z :: c
z = forall a. Additive a => Root a -> a
zero Orientation (Point c)
o
  oKer :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 c
oKer = forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel (forall c. Oriented c => c -> KernelDiagram N1 c
kernelDiagram c
z) (forall c. Multiplicative c => Point c -> c
one (forall q. Oriented q => q -> Point q
start c
z))

  
--------------------------------------------------------------------------------
-- kernels0 -

-- | kernels for zero arrows.
kernels0 :: Distributive a => Kernels N0 a
kernels0 :: forall a. Distributive a => Kernels N0 a
kernels0 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits forall a. Distributive a => KernelDiagram N0 a -> Kernel N0 a
krn where
  krn :: Distributive a => KernelDiagram N0 a -> Kernel N0 a
  krn :: forall a. Distributive a => KernelDiagram N0 a -> Kernel N0 a
krn d :: KernelDiagram N0 a
d@(DiagramParallelLR Point a
p Point a
_ FinList N0 a
Nil) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N0 a
l forall a. KernelCone N0 a -> a
u where
    l :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N0 a
l = forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel KernelDiagram N0 a
d (forall c. Multiplicative c => Point c -> c
one Point a
p)
    u :: KernelCone N0 a -> a
    u :: forall a. KernelCone N0 a -> a
u (ConeKernel Diagram ('Parallel 'LeftToRight) N2 N0 a
_ a
f) = a
f

--------------------------------------------------------------------------------
-- krnEqls -

-- | the induced equalizers where its first arrow is 'zero'.
krnEqls :: (Distributive a, Abelian a) => Kernels n a -> Equalizers (n+1) a
krnEqls :: forall a (n :: N').
(Distributive a, Abelian a) =>
Kernels n a -> Equalizers (n + 1) a
krnEqls Kernels n a
krn = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a (n :: N').
(Distributive a, Abelian a) =>
Kernels n a -> EqualizerDiagram (n + 1) a -> Equalizer (n + 1) a
eql Kernels n a
krn) where
  eql :: (Distributive a, Abelian a)
    => Kernels n a -> EqualizerDiagram (n+1) a -> Equalizer (n+1) a
  eql :: forall a (n :: N').
(Distributive a, Abelian a) =>
Kernels n a -> EqualizerDiagram (n + 1) a -> Equalizer (n + 1) a
eql Kernels n a
krn EqualizerDiagram (n + 1) a
d = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a
l Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a -> a
u where
    LimesProjective (ConeKernel Diagram ('Parallel 'LeftToRight) N2 n a
dKrn a
k) Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a -> a
uKrn = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Kernels n a
krn (forall a (d :: Direction) (n :: N') (m :: N').
Abelian a =>
Diagram ('Parallel d) n (m + 1) a -> Diagram ('Parallel d) n m a
dgPrlDiffTail EqualizerDiagram (n + 1) a
d)
    a0 :: a
a0 = 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 EqualizerDiagram (n + 1) a
d
    
    l :: Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a
l = 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 EqualizerDiagram (n + 1) a
d (forall q. Oriented q => q -> Point q
start a
k) (a
kforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|a
a0forall c. Multiplicative c => c -> c -> c
*a
kforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)
    u :: Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a -> a
u Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a
c = Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a -> a
uKrn (forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel Diagram ('Parallel 'LeftToRight) N2 n a
dKrn (forall (n :: N') a. FinList (n + 1) a -> a
head 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 -> FinList n a
shell Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a
c))

--------------------------------------------------------------------------------
-- eqlKrns -

-- | the induced kernels given by adjoining a 'zero' arrow as first arrow.
eqlKrns :: Distributive a => Equalizers (n+1) a -> Kernels n a
eqlKrns :: forall a (n :: N').
Distributive a =>
Equalizers (n + 1) a -> Kernels n a
eqlKrns Equalizers (n + 1) a
eql = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a (n :: N').
Distributive a =>
Equalizers (n + 1) a -> KernelDiagram n a -> Kernel n a
krn Equalizers (n + 1) a
eql) where
  krn :: Distributive a => Equalizers (n+1) a -> KernelDiagram n a -> Kernel n a
  krn :: forall a (n :: N').
Distributive a =>
Equalizers (n + 1) a -> KernelDiagram n a -> Kernel n a
krn Equalizers (n + 1) a
eql KernelDiagram n a
d = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a
l Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a -> a
u where
    LimesProjective Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a
lEql Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a -> a
uEql = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Equalizers (n + 1) a
eql (forall a (n :: N') (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) n m a
-> Diagram ('Parallel 'LeftToRight) n (m + 1) a
dgPrlAdjZero KernelDiagram n a
d)
    
    l :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a
l = forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel KernelDiagram n a
d (forall (n :: N') a. FinList (n + 1) a -> a
head 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 -> FinList n a
shell Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a
lEql)
    u :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a -> a
u Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a
c = Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a -> a
uEql (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 s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone Mlt 'Projective ('Parallel 'LeftToRight) N2 ('S n) a
lEql) (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a
c) (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a
c))

--------------------------------------------------------------------------------
-- kenrels1 -

-- | promoting kernels.
kernels1 :: Distributive a => Kernels N1 a -> Kernels (n+1) a
kernels1 :: forall a (n :: N').
Distributive a =>
Kernels N1 a -> Kernels (n + 1) a
kernels1 Kernels N1 a
krn1 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a (n :: N').
Distributive a =>
Kernels N1 a -> KernelDiagram (n + 1) a -> Kernel (n + 1) a
krn Kernels N1 a
krn1) where
  krn :: Distributive a => Kernels N1 a -> KernelDiagram (n+1) a -> Kernel (n+1) a
  krn :: forall a (n :: N').
Distributive a =>
Kernels N1 a -> KernelDiagram (n + 1) a -> Kernel (n + 1) a
krn Kernels N1 a
krn1 d :: KernelDiagram (n + 1) a
d@(DiagramParallelLR Point a
_ Point a
_ (a
_:|FinList n a
Nil))        = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Kernels N1 a
krn1 KernelDiagram (n + 1) a
d
  krn Kernels N1 a
krn1 d :: KernelDiagram (n + 1) a
d@(DiagramParallelLR Point a
p Point a
q (a
a0:|aN :: FinList n a
aN@(a
_:|FinList n a
_))) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Dst 'Projective ('Parallel 'LeftToRight) N2 ('S ('S n)) a
l Cone Dst 'Projective ('Parallel 'LeftToRight) N2 ('S ('S n)) a -> a
u where
    dN :: Diagram ('Parallel 'LeftToRight) N2 n a
dN = forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) N2 m a
DiagramParallelLR Point a
p Point a
q FinList n a
aN
    LimesProjective (ConeKernel Diagram ('Parallel 'LeftToRight) N2 (n + 1) a
_ a
h) Cone Dst 'Projective ('Parallel 'LeftToRight) N2 (n + 1) a -> a
Cone Dst 'Projective ('Parallel 'LeftToRight) N2 ('S n) a -> a
uN = forall a (n :: N').
Distributive a =>
Kernels N1 a -> KernelDiagram (n + 1) a -> Kernel (n + 1) a
krn Kernels N1 a
krn1 Diagram ('Parallel 'LeftToRight) N2 n a
dN

    d1 :: Diagram ('Parallel 'LeftToRight) N2 N1 a
d1 = forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) N2 m a
DiagramParallelLR (forall q. Oriented q => q -> Point q
start a
h) Point a
q (a
a0forall c. Multiplicative c => c -> c -> c
*a
hforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)
    LimesProjective (ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 a
_ a
k) Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 a -> a
u1 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Kernels N1 a
krn1 Diagram ('Parallel 'LeftToRight) N2 N1 a
d1
    l :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 ('S ('S n)) a
l = forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel KernelDiagram (n + 1) a
d (a
hforall c. Multiplicative c => c -> c -> c
*a
k)
    u :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 ('S ('S n)) a -> a
u (ConeKernel Diagram ('Parallel 'LeftToRight) N2 ('S ('S n)) a
_ a
x) = a
uk where
      uk :: a
uk = Cone Dst 'Projective ('Parallel 'LeftToRight) N2 N1 a -> a
u1 (forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel Diagram ('Parallel 'LeftToRight) N2 N1 a
d1 a
uh)
      uh :: a
uh = Cone Dst 'Projective ('Parallel 'LeftToRight) N2 ('S n) a -> a
uN (forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel Diagram ('Parallel 'LeftToRight) N2 n a
dN a
x)

--------------------------------------------------------------------------------
-- kernels -

-- | promoting kernels.
kernels :: Distributive a => Kernels N1 a -> Kernels n a
kernels :: forall a (n :: N'). Distributive a => Kernels N1 a -> Kernels n a
kernels Kernels N1 a
krn1 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a (n :: N').
Distributive a =>
Kernels N1 a -> KernelDiagram n a -> Kernel n a
krn Kernels N1 a
krn1) where
  krn :: Distributive a
    => Kernels N1 a -> KernelDiagram n a -> Kernel n a
  krn :: forall a (n :: N').
Distributive a =>
Kernels N1 a -> KernelDiagram n a -> Kernel n a
krn Kernels N1 a
krn1 KernelDiagram n a
d = case forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows KernelDiagram n a
d of
    FinList n a
Nil     -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes forall a. Distributive a => Kernels N0 a
kernels0 KernelDiagram n a
d
    a
_:|FinList n a
Nil  -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Kernels N1 a
krn1 KernelDiagram n a
d
    a
_:|a
_:|FinList n a
_ -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes (forall a (n :: N').
Distributive a =>
Kernels N1 a -> Kernels (n + 1) a
kernels1 Kernels N1 a
krn1) KernelDiagram n a
d

--------------------------------------------------------------------------------
-- kernelsOrnt -

-- | kernels for 'Orientation'.
kernelsOrnt :: Entity p => p -> Kernels n (Orientation p)
kernelsOrnt :: forall p (n :: N'). Entity p => p -> Kernels n (Orientation p)
kernelsOrnt p
t = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall p a (n :: N').
(Entity p, a ~ Orientation p) =>
p -> KernelDiagram n a -> Kernel n a
krn p
t) where
  krn :: (Entity p, a ~ Orientation p) => p -> KernelDiagram n a -> Kernel n a
  krn :: forall p a (n :: N').
(Entity p, a ~ Orientation p) =>
p -> KernelDiagram n a -> Kernel n a
krn p
t d :: KernelDiagram n a
d@(DiagramParallelLR Point a
p Point a
_ FinList n a
_) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a
l Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a -> a
u where
    l :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a
l = forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel KernelDiagram n a
d (p
tforall p. p -> p -> Orientation p
:>Point a
p)
    u :: Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a -> a
u (ConeKernel KernelDiagram n a
_ a
x) = forall q. Oriented q => q -> Point q
start a
x forall p. p -> p -> Orientation p
:> p
t
  

--------------------------------------------------------------------------------
-- Cokernels -

-- | 'Diagram' for a cokernel.
type CokernelDiagram n = Diagram (Parallel RightToLeft) N2 n

-- | 'Cone' for a cokernel.
type CokernelCone n = Cone Dst Injective (Parallel RightToLeft) N2 n

-- | cokernel as 'Limes'.
type Cokernel n = Limes Dst Injective (Parallel RightToLeft) N2 n

-- | cokernels for 'Distributive' structures.
type Cokernels n       = Limits Dst Injective (Parallel RightToLeft) N2 n

--------------------------------------------------------------------------------
-- cokernelFactor -

-- | the factor of its shell.
cokernelFactor :: CokernelCone N1 c -> c
cokernelFactor :: forall c. CokernelCone N1 c -> c
cokernelFactor (ConeCokernel Diagram ('Parallel 'RightToLeft) N2 N1 c
_ c
f) = c
f

--------------------------------------------------------------------------------
-- cokernelDiagram -

-- | the cokernel diagram of a given factor.
cokernelDiagram :: Oriented c => c -> CokernelDiagram N1 c
cokernelDiagram :: forall c. Oriented c => c -> CokernelDiagram N1 c
cokernelDiagram c
f = forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) N2 m a
DiagramParallelRL (forall q. Oriented q => q -> Point q
end c
f) (forall q. Oriented q => q -> Point q
start c
f) (c
fforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)

--------------------------------------------------------------------------------
-- Cokernels - Duality -

-- | duality between cokernels and kernels.
cokrnLimitsDuality :: Distributive a
  => LimitsDuality Dst (Cokernels n) (Kernels n) a
cokrnLimitsDuality :: forall a (n :: N').
Distributive a =>
LimitsDuality Dst (Cokernels n) (Kernels n) a
cokrnLimitsDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limits s p t n m a)
-> (g (Op a) :~: Dual (Limits s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimitsDuality s f g a
LimitsDuality forall a. Distributive a => ConeStruct Dst a
ConeStructDst forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- cokrnLimesDuality -

-- | duality between 'Cokernel' to 'Kernel'.
cokrnLimesDuality :: Distributive a
  => LimesDuality Dst (Cokernel n) (Kernel n) a
cokrnLimesDuality :: forall a (n :: N').
Distributive a =>
LimesDuality Dst (Cokernel n) (Kernel n) a
cokrnLimesDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limes s p t n m a)
-> (g (Op a) :~: Dual (Limes s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimesDuality s f g a
LimesDuality forall a. Distributive a => ConeStruct Dst a
ConeStructDst forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- krnLimesDuality -

-- | duality from 'Kernel' to 'Cokernel'.
krnLimesDuality :: Distributive a
  => LimesDuality Dst (Kernel n) (Cokernel n) a
krnLimesDuality :: forall a (n :: N').
Distributive a =>
LimesDuality Dst (Kernel n) (Cokernel n) a
krnLimesDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limes s p t n m a)
-> (g (Op a) :~: Dual (Limes s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimesDuality s f g a
LimesDuality forall a. Distributive a => ConeStruct Dst a
ConeStructDst forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- cokernels -

-- | promoting cokernels.
cokernels :: Distributive a => Cokernels N1 a -> Cokernels n a
cokernels :: forall a (n :: N').
Distributive a =>
Cokernels N1 a -> Cokernels n a
cokernels Cokernels N1 a
ckrn = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Distributive a =>
LimitsDuality Dst (Cokernels n) (Kernels n) a
cokrnLimitsDuality forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (n :: N'). Distributive a => Kernels N1 a -> Kernels n a
kernels Kernels N1 (Op a)
krn where
  krn :: Kernels N1 (Op a)
krn = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> f a -> g (Op a)
lmsToOp forall a (n :: N').
Distributive a =>
LimitsDuality Dst (Cokernels n) (Kernels n) a
cokrnLimitsDuality Cokernels N1 a
ckrn

-- | 'cokernels' given by an additional proxy for @n@.
cokernels' :: Distributive a => p n -> Cokernels N1 a -> Cokernels n a
cokernels' :: forall a (p :: N' -> *) (n :: N').
Distributive a =>
p n -> Cokernels N1 a -> Cokernels n a
cokernels' p n
_ = forall a (n :: N').
Distributive a =>
Cokernels N1 a -> Cokernels n a
cokernels

--------------------------------------------------------------------------------
-- cokernelsOrnt -

-- | cokernels for 'Orientation'.
cokernelsOrnt :: Entity p => p -> Cokernels n (Orientation p)
cokernelsOrnt :: forall p (n :: N'). Entity p => p -> Cokernels n (Orientation p)
cokernelsOrnt p
t = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall p a (n :: N').
(Entity p, a ~ Orientation p) =>
p -> CokernelDiagram n a -> Cokernel n a
cokrn p
t) where
  cokrn :: (Entity p, a ~ Orientation p) => p -> CokernelDiagram n a -> Cokernel n a
  cokrn :: forall p a (n :: N').
(Entity p, a ~ Orientation p) =>
p -> CokernelDiagram n a -> Cokernel n a
cokrn p
t d :: CokernelDiagram n a
d@(DiagramParallelRL Point a
p Point a
_ FinList n a
_) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> (Cone s 'Injective t n m a -> a) -> Limes s 'Injective t n m a
LimesInjective Cone Dst 'Injective ('Parallel 'RightToLeft) N2 n a
l Cone Dst 'Injective ('Parallel 'RightToLeft) N2 n a -> a
u where
    l :: Cone Dst 'Injective ('Parallel 'RightToLeft) N2 n a
l = forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel CokernelDiagram n a
d (Point a
pforall p. p -> p -> Orientation p
:>p
t)
    u :: Cone Dst 'Injective ('Parallel 'RightToLeft) N2 n a -> a
u (ConeCokernel CokernelDiagram n a
_ a
x) = p
t forall p. p -> p -> Orientation p
:> forall q. Oriented q => q -> Point q
end a
x

--------------------------------------------------------------------------------
-- prpIsKernel -

relIsKernel :: Eq a => Kernel n a -> FinList n a -> a -> Statement
relIsKernel :: forall a (n :: N').
Eq a =>
Kernel n a -> FinList n a -> a -> Statement
relIsKernel (LimesProjective (ConeKernel Diagram ('Parallel 'LeftToRight) N2 n a
d a
k') Cone Dst 'Projective ('Parallel 'LeftToRight) N2 n a -> a
_) FinList n a
fs a
k
  = [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (FinList n a
fs forall a. Eq a => a -> a -> Bool
== forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows Diagram ('Parallel 'LeftToRight) N2 n a
d) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"fs"String -> String -> Parameter
:=forall a. Show a => a -> String
show FinList n a
fs, String
"d"String -> String -> Parameter
:= forall a. Show a => a -> String
show Diagram ('Parallel 'LeftToRight) N2 n a
d]
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (a
k forall a. Eq a => a -> a -> Bool
== a
k') Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"k"String -> String -> Parameter
:= forall a. Show a => a -> String
show a
k, String
"k'"String -> String -> Parameter
:= forall a. Show a => a -> String
show a
k']
        ]
    
-- | checks if the arrows of the kernel diagram are equal to the given ones and if its
-- shell is equal to the given arrow.
--
-- __Property__ Let
-- @'LimesProjective' ('ConeKerenl d k') _ = ker@ be in @'Kernel' __n__ __a__@,
-- @fs@ in @'FinList' __n__ __a__@ and @k@ be in @__a__@, then the statement
-- @'prpIsKernel' ker fs k@ holds if and only if
--
-- (1) @fs '==' 'dgArrows' d@.
--
-- (2) @k '==' k'@.
prpIsKernel :: Distributive a => Kernel n a -> FinList n a -> a -> Statement
prpIsKernel :: forall a (n :: N').
Distributive a =>
Kernel n a -> FinList n a -> a -> Statement
prpIsKernel Kernel n a
ker FinList n a
fs a
k = String -> Label
Prp String
"IsKernel" Label -> Statement -> Statement
:<=>: forall a (n :: N').
Eq a =>
Kernel n a -> FinList n a -> a -> Statement
relIsKernel Kernel n a
ker FinList n a
fs a
k

--------------------------------------------------------------------------------
-- prpIsCokernel -

-- | checks if the arrows of the cokernel diagram are equal to the given ones and if its
-- shell is equal to the given arrow.
--
-- __Property__ Let
-- @'LimesInjective' ('ConeCokerenl d k') _ = coker@ be in @'Cokernel' __n__ __a__@,
-- @fs@ in @'FinList' __n__ __a__@ and @k@ be in @__a__@, then the statement
-- @'prpIsCokernel' coker fs k@ holds if and only if
--
-- (1) @fs '==' 'dgArrows' d@.
--
-- (2) @k '==' k'@.
prpIsCokernel :: Distributive a => Cokernel n a -> FinList n a -> a -> Statement
prpIsCokernel :: forall a (n :: N').
Distributive a =>
Cokernel n a -> FinList n a -> a -> Statement
prpIsCokernel Cokernel n a
coker FinList n a
fs a
k = String -> Label
Prp String
"IsCokernel" Label -> Statement -> Statement
:<=>: forall a (n :: N').
Eq a =>
Kernel n a -> FinList n a -> a -> Statement
relIsKernel Kernel n (Op a)
ker (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall x. x -> Op x
Op FinList n a
fs) (forall x. x -> Op x
Op a
k)
  where ker :: Kernel n (Op a)
ker = forall s (f :: * -> *) (g :: * -> *) a.
LimesDuality s f g a -> f a -> g (Op a)
lmToOp forall a (n :: N').
Distributive a =>
LimesDuality Dst (Cokernel n) (Kernel n) a
cokrnLimesDuality Cokernel n a
coker