{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# 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, KernelsG
  , Kernel, KernelG
  , KernelCone, KernelConic
  , KernelDiagram, KernelDiagrammatic
  , kernelFactor
  , kernelDiagram

    -- ** Construction

  , kernels, kernels', kernels0, kernels1
  , krnEqls, eqlKrns
  , kernelZero

    -- *** Orientation

  , kernelsOrnt

    -- * Cokernels

  , Cokernels, CokernelsG
  , Cokernel, CokernelG
  , CokernelCone, CokernelConic
  , CokernelDiagram, CokernelDiagrammatic
  , cokernelFactor
  , cokernelDiagram

    -- ** Construction

  , cokernels, cokernels'
  , coKernelsG

    -- *** Orientation

  , cokernelsOrnt

    -- * Proposition

  , prpIsKernel, prpIsCokernel

    -- * X

  , XStandardEligibleConeKernel, XStandardEligibleConeKernel1
  , XStandardEligibleConeFactorKernel, XStandardEligibleConeFactorKernel1
  , XStandardEligibleConeCokernel, XStandardEligibleConeCokernel1
  , XStandardEligibleConeFactorCokernel, XStandardEligibleConeFactorCokernel1

  )
  where

import Data.Kind

import OAlg.Prelude

import OAlg.Category.SDuality

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

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.Hom.Definition
import OAlg.Hom.Distributive

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

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

-- Kernels -


-- | 'Diagrammatic' object for a kernel.

type KernelDiagrammatic d (n :: N') = d (Parallel LeftToRight) N2 n :: Type -> Type

-- | 'Diagram' for a kernel.

type KernelDiagram n = KernelDiagrammatic Diagram n

-- | 'Conic' object for a kernel.

type KernelConic c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N')
  = c Dst Projective d (Parallel LeftToRight) N2 n :: Type -> Type

-- | 'Cone' for a kernel.

type KernelCone n = KernelConic Cone Diagram n

-- | generic kernel as a 'LimesG'.

type KernelG c d n = LimesG c Dst Projective d (Parallel LeftToRight) N2 n

-- | kernel as a 'KernelG'.

type Kernel n = KernelG Cone Diagram n

-- | generic kernels for 'Distributive' structures.

type KernelsG c d n = LimitsG c Dst Projective d (Parallel LeftToRight) N2 n

-- | kernels for 'Distributive' structures.

type Kernels n = KernelsG Cone Diagram n

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

-- kernelFactor -


-- | the factor of its shell.

kernelFactor :: Conic c => KernelConic c d n x -> x
kernelFactor :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Conic c =>
KernelConic c d n x -> x
kernelFactor KernelConic c d n x
c = case KernelConic c d n x
-> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 n x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone KernelConic c d n x
c of ConeKernel d ('Parallel 'LeftToRight) N2 n x
_ x
x -> x
x

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

-- kernelDiagram -


-- | the kernel diagram of a given factor.

kernelDiagram :: Oriented x => x -> KernelDiagram N1 x
kernelDiagram :: forall x. Oriented x => x -> KernelDiagram N1 x
kernelDiagram x
f = Point x
-> Point x
-> FinList N1 x
-> Diagram ('Parallel 'LeftToRight) N2 N1 x
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) N2 m a
DiagramParallelLR (x -> Point x
forall q. Oriented q => q -> Point q
start x
f) (x -> Point x
forall q. Oriented q => q -> Point q
end x
f) (x
fx -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil)

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

-- kernelZero -


-- | the kernel of the 'zero' factor given by the orientation, i.e. 'one'

kernelZero :: Distributive x => p x -> Orientation (Point x) -> Kernel N1 x
kernelZero :: forall x (p :: * -> *).
Distributive x =>
p x -> Orientation (Point x) -> Kernel N1 x
kernelZero p x
_ Orientation (Point x)
o = Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
-> (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
    -> x)
-> LimesG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
oKer Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Conic c =>
KernelConic c d n x -> x
kernelFactor where
  z :: x
z = Root x -> x
forall a. Additive a => Root a -> a
zero Orientation (Point x)
Root x
o
  oKer :: Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
oKer = Diagram ('Parallel 'LeftToRight) N2 N1 x
-> x
-> Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel (x -> Diagram ('Parallel 'LeftToRight) N2 N1 x
forall x. Oriented x => x -> KernelDiagram N1 x
kernelDiagram x
z) (Point x -> x
forall c. Multiplicative c => Point c -> c
one (x -> Point x
forall q. Oriented q => q -> Point q
start x
z))
  
--------------------------------------------------------------------------------

-- kernels0 -


-- | kernels for zero arrows.

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

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

-- krnEqls -


-- | the induced equalizers where its first arrow is 'zero'.

krnEqls :: (Distributive x, Abelian x) => Kernels n x -> Equalizers (n+1) x
krnEqls :: forall x (n :: N').
(Distributive x, Abelian x) =>
Kernels n x -> Equalizers (n + 1) x
krnEqls Kernels n x
krn = (Diagram ('Parallel 'LeftToRight) N2 ('S n) x
 -> LimesG
      Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x)
-> LimitsG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (Kernels n x -> EqualizerDiagram (n + 1) x -> Equalizer (n + 1) x
forall x (n :: N').
(Distributive x, Abelian x) =>
Kernels n x -> EqualizerDiagram (n + 1) x -> Equalizer (n + 1) x
eql Kernels n x
krn) where
  eql :: (Distributive x, Abelian x)
    => Kernels n x -> EqualizerDiagram (n+1) x -> Equalizer (n+1) x
  eql :: forall x (n :: N').
(Distributive x, Abelian x) =>
Kernels n x -> EqualizerDiagram (n + 1) x -> Equalizer (n + 1) x
eql Kernels n x
krn EqualizerDiagram (n + 1) x
d = Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> (Cone
      Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
    -> x)
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
l Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> x
u where
    LimesProjective (ConeKernel Diagram ('Parallel 'LeftToRight) N2 n x
dKrn x
k) Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x -> x
uKrn = Kernels n x
-> Diagram ('Parallel 'LeftToRight) N2 n x
-> LimesG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes Kernels n x
krn (EqualizerDiagram (n + 1) x
-> Diagram ('Parallel 'LeftToRight) N2 n x
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) x
d)
    a0 :: x
a0 = FinList (n + 1) x -> x
FinList ('S n) x -> x
forall (n :: N') a. FinList (n + 1) a -> a
head (FinList ('S n) x -> x) -> FinList ('S n) x -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram ('Parallel 'LeftToRight) N2 ('S n) x -> FinList ('S n) x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows EqualizerDiagram (n + 1) x
Diagram ('Parallel 'LeftToRight) N2 ('S n) x
d
    
    l :: Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
l = Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> Point x
-> FinList N2 x
-> Cone
     Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective EqualizerDiagram (n + 1) x
Diagram ('Parallel 'LeftToRight) N2 ('S n) x
d (x -> Point x
forall q. Oriented q => q -> Point q
start x
k) (x
kx -> FinList N1 x -> FinList (N1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
a0x -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
kx -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil)
    u :: Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> x
u Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
c = Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x -> x
uKrn (Diagram ('Parallel 'LeftToRight) N2 n x
-> x
-> Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel Diagram ('Parallel 'LeftToRight) N2 n x
dKrn (FinList (N1 + 1) x -> x
FinList N2 x -> x
forall (n :: N') a. FinList (n + 1) a -> a
head (FinList N2 x -> x) -> FinList N2 x -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> FinList N2 x
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> FinList n a
shell Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
c))

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

-- eqlKrns -


-- | the induced kernels given by adjoining a 'zero' arrow as first arrow.

eqlKrns :: Distributive x => Equalizers (n+1) x -> Kernels n x
eqlKrns :: forall x (n :: N').
Distributive x =>
Equalizers (n + 1) x -> Kernels n x
eqlKrns Equalizers (n + 1) x
eql = (Diagram ('Parallel 'LeftToRight) N2 n x
 -> LimesG
      Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x)
-> LimitsG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (Equalizers (n + 1) x
-> Diagram ('Parallel 'LeftToRight) N2 n x
-> LimesG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall x (n :: N').
Distributive x =>
Equalizers (n + 1) x -> KernelDiagram n x -> Kernel n x
krn Equalizers (n + 1) x
eql) where
  cnDiagram :: Cone s p Diagram t n m x -> Diagram t n m x
cnDiagram = Diagram t n m x -> Diagram t n m x
forall (t :: DiagramType) (n :: N') (m :: N') x.
Diagram t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram (Diagram t n m x -> Diagram t n m x)
-> (Cone s p Diagram t n m x -> Diagram t n m x)
-> Cone s p Diagram t n m x
-> Diagram t n m x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Cone s p Diagram t n m x -> Diagram t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> d t n m a
diagrammaticObject
  
  krn :: Distributive x => Equalizers (n+1) x -> KernelDiagram n x -> Kernel n x
  krn :: forall x (n :: N').
Distributive x =>
Equalizers (n + 1) x -> KernelDiagram n x -> Kernel n x
krn Equalizers (n + 1) x
eql KernelDiagram n x
d = Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
    -> x)
-> LimesG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
l Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x -> x
u where
    LimesProjective Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
lEql Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> x
uEql = LimitsG
  Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> LimesG
     Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes Equalizers (n + 1) x
LimitsG
  Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
eql (KernelDiagram n x -> Diagram ('Parallel 'LeftToRight) N2 (n + 1) x
forall a (n :: N') (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) n m a
-> Diagram ('Parallel 'LeftToRight) n (m + 1) a
dgPrlAdjZero KernelDiagram n x
d)
    
    l :: Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
l = KernelDiagram n x
-> x
-> Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel KernelDiagram n x
d (FinList (N1 + 1) x -> x
FinList N2 x -> x
forall (n :: N') a. FinList (n + 1) a -> a
head (FinList N2 x -> x) -> FinList N2 x -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> FinList N2 x
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> FinList n a
shell Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
lEql)
    u :: Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x -> x
u Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
c = Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> x
uEql (Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> Point x
-> FinList N2 x
-> Cone
     Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective (Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
-> Diagram ('Parallel 'LeftToRight) N2 ('S n) x
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'} {x}.
Cone s p Diagram t n m x -> Diagram t n m x
cnDiagram Cone Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 ('S n) x
lEql) (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> Point x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
c) (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> FinList N2 x
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> FinList n a
shell Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
c))

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

-- kenrels1 -


-- | promoting kernels.

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

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

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

-- kernels -


-- | promoting kernels.

kernels :: Distributive x => Kernels N1 x -> Kernels n x
kernels :: forall x (n :: N'). Distributive x => Kernels N1 x -> Kernels n x
kernels Kernels N1 x
krn1 = (Diagram ('Parallel 'LeftToRight) N2 n x
 -> LimesG
      Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x)
-> LimitsG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (Kernels N1 x
-> Diagram ('Parallel 'LeftToRight) N2 n x
-> LimesG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall x (n :: N').
Distributive x =>
Kernels N1 x -> KernelDiagram n x -> Kernel n x
krn Kernels N1 x
krn1) where
  krn :: Distributive x
    => Kernels N1 x -> KernelDiagram n x -> Kernel n x
  krn :: forall x (n :: N').
Distributive x =>
Kernels N1 x -> KernelDiagram n x -> Kernel n x
krn Kernels N1 x
krn1 KernelDiagram n x
d = case KernelDiagram n x -> FinList n x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows KernelDiagram n x
d of
    FinList n x
Nil     -> LimitsG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> KernelDiagram n x -> Kernel n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
Kernels 'N0 x
forall x. Distributive x => Kernels 'N0 x
kernels0 KernelDiagram n x
d
    x
_:|FinList n1 x
Nil  -> LimitsG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> KernelDiagram n x -> Kernel n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
Kernels N1 x
krn1 KernelDiagram n x
d
    x
_:|x
_:|FinList n1 x
_ -> LimitsG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> KernelDiagram n x -> Kernel n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes (Kernels N1 x -> Kernels ('S n1 + 1) x
forall x (n :: N').
Distributive x =>
Kernels N1 x -> Kernels (n + 1) x
kernels1 Kernels N1 x
krn1) KernelDiagram n x
d

-- | promoting kernels according to the given proxy type.

kernels' :: Distributive x => q n -> Kernels N1 x -> Kernels n x
kernels' :: forall x (q :: N' -> *) (n :: N').
Distributive x =>
q n -> Kernels N1 x -> Kernels n x
kernels' q n
_ = Kernels N1 x -> Kernels n x
forall x (n :: N'). Distributive x => Kernels N1 x -> Kernels n x
kernels

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

-- 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 = (Diagram ('Parallel 'LeftToRight) N2 n (Orientation p)
 -> LimesG
      Cone
      Dst
      'Projective
      Diagram
      ('Parallel 'LeftToRight)
      N2
      n
      (Orientation p))
-> LimitsG
     Cone
     Dst
     'Projective
     Diagram
     ('Parallel 'LeftToRight)
     N2
     n
     (Orientation p)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (p
-> Diagram ('Parallel 'LeftToRight) N2 n (Orientation p)
-> LimesG
     Cone
     Dst
     'Projective
     Diagram
     ('Parallel 'LeftToRight)
     N2
     n
     (Orientation p)
forall p x (n :: N').
(Entity p, x ~ Orientation p) =>
p -> KernelDiagram n x -> Kernel n x
krn p
t) where
  krn :: (Entity p, x ~ Orientation p) => p -> KernelDiagram n x -> Kernel n x
  krn :: forall p x (n :: N').
(Entity p, x ~ Orientation p) =>
p -> KernelDiagram n x -> Kernel n x
krn p
t d :: KernelDiagram n x
d@(DiagramParallelLR Point x
p Point x
_ FinList n x
_) = Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
-> (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
    -> x)
-> LimesG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
l Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x -> x
u where
    l :: Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
l = KernelDiagram n x
-> x
-> Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel KernelDiagram n x
d (p
tp -> p -> Orientation p
forall p. p -> p -> Orientation p
:>p
Point x
p)
    u :: Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x -> x
u (ConeKernel KernelDiagram n x
_ x
x) = x -> Point x
forall q. Oriented q => q -> Point q
start x
x p -> p -> Orientation p
forall p. p -> p -> Orientation p
:> p
t

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

-- Cokernels -


-- | 'Diagrammatic' object for a cokernel.

type CokernelDiagrammatic d (n :: N') = d (Parallel RightToLeft) N2 n :: Type -> Type

-- | 'Diagram' for a cokernel.

type CokernelDiagram n = CokernelDiagrammatic Diagram n

-- | 'Conic' object for a cokernel.

type CokernelConic c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N')
  = c Dst Injective d (Parallel RightToLeft) N2 n :: Type -> Type

-- | 'Cone' for a cokernel.

type CokernelCone n = CokernelConic Cone Diagram n

-- | generic cokernel as a 'LimesG'.

type CokernelG c d n = LimesG c Dst Injective d (Parallel RightToLeft) N2 n

-- | cokernel as a 'CokernelG'.

type Cokernel n = CokernelG Cone Diagram n

-- | generic cokernels for 'Distributive' structures.

type CokernelsG c d n = LimitsG c Dst Injective d (Parallel RightToLeft) N2 n

-- | cokernels for 'Distributive' structures.

type Cokernels n = CokernelsG Cone Diagram n

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

-- coKernelsG -


-- | to co-object of kernels.

coKernelsG ::
  ( Distributive x
  , TransformableGRefl o Dst
  , NaturalConicBi (IsoO Dst o) c Dst Projective d (Parallel LeftToRight) N2 n
  )
  => KernelsG c d n x -> CokernelsG c d n (o x)
coKernelsG :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Distributive x, TransformableGRefl o Dst,
 NaturalConicBi
   (IsoO Dst o) c Dst 'Projective d ('Parallel 'LeftToRight) N2 n) =>
KernelsG c d n x -> CokernelsG c d n (o x)
coKernelsG KernelsG c d n x
ks = Dual1
  (LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n) (o x)
LimitsG c Dst 'Injective d ('Parallel 'RightToLeft) N2 n (o x)
cks where
  Contravariant2 IsoO Dst o x (o x)
i    = Struct Dst x -> Variant2 'Contravariant (IsoO Dst o) x (o x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO (Struct Dst x
forall {x}. Distributive x => Struct Dst x
forall s x. Structure s x => Struct s x
Struct :: Distributive x => Struct Dst x)
  SDualBi (Left1 Dual1
  (LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n) (o x)
cks) = IsoO Dst o x (o x)
-> SDualBi
     (LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n) x
-> SDualBi
     (LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n) (o x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Dst o x (o x)
i (Either1
  (Dual1 (LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n))
  (LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n)
  x
-> SDualBi
     (LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (KernelsG c d n x
-> Either1
     (LimitsG c Dst 'Injective d ('Parallel 'RightToLeft) N2 n)
     (LimitsG c Dst 'Projective d ('Parallel 'LeftToRight) N2 n)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 KernelsG c d n x
ks))

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

-- cokernelFactor -


-- | the factor of its shell.

cokernelFactor :: Conic c => CokernelConic c d n x -> x
cokernelFactor :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Conic c =>
CokernelConic c d n x -> x
cokernelFactor CokernelConic c d n x
c = case CokernelConic c d n x
-> Cone Dst 'Injective d ('Parallel 'RightToLeft) N2 n x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone CokernelConic c d n x
c of ConeCokernel d ('Parallel 'RightToLeft) N2 n x
_ x
x -> x
x

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

-- cokernelDiagram -


-- | the cokernel diagram of a given factor.

cokernelDiagram :: Oriented x => x -> CokernelDiagram N1 x
cokernelDiagram :: forall x. Oriented x => x -> CokernelDiagram N1 x
cokernelDiagram x
f = Point x
-> Point x
-> FinList N1 x
-> Diagram ('Parallel 'RightToLeft) N2 N1 x
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) N2 m a
DiagramParallelRL (x -> Point x
forall q. Oriented q => q -> Point q
end x
f) (x -> Point x
forall q. Oriented q => q -> Point q
start x
f) (x
fx -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil)

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

-- cokernels -


-- | promoting cokernels.

cokernels :: Distributive x => Cokernels N1 x -> Cokernels n x
cokernels :: forall x (n :: N').
Distributive x =>
Cokernels N1 x -> Cokernels n x
cokernels Cokernels N1 x
ck1 = LimitsG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
cks where
  Contravariant2 IsoO Dst Op x (Op x)
i     = Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) x (Op x)
toDualOpDst
  SDualBi (Left1 Dual1
  (LimitsG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
  (Op x)
k1)   = IsoO Dst Op x (Op x)
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
     x
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
     (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Dst Op x (Op x)
i (Either1
  (Dual1
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1))
  (LimitsG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
  x
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Cokernels N1 x
-> Either1
     (LimitsG
        Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 N1)
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Cokernels N1 x
ck1))
  ks :: Kernels n (Op x)
ks                   = Kernels N1 (Op x) -> Kernels n (Op x)
forall x (n :: N'). Distributive x => Kernels N1 x -> Kernels n x
kernels Dual1
  (LimitsG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 N1)
  (Op x)
Kernels N1 (Op x)
k1
  SDualBi (Right1 LimitsG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
cks) = Inv2 (HomDisjEmpty Dst Op) (Op x) x
-> SDualBi
     (LimitsG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     (Op x)
-> SDualBi
     (LimitsG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Dst Op x (Op x) -> Inv2 (HomDisjEmpty Dst Op) (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Dst Op x (Op x)
i) (Either1
  (Dual1
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n))
  (LimitsG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
  (Op x)
-> SDualBi
     (LimitsG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Kernels n (Op x)
-> Either1
     (LimitsG
        Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n)
     (LimitsG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Kernels n (Op x)
ks))

-- | promoting cokernels according to the given proxy type.

cokernels' :: Distributive x => q n -> Cokernels N1 x -> Cokernels n x
cokernels' :: forall x (q :: N' -> *) (n :: N').
Distributive x =>
q n -> Cokernels N1 x -> Cokernels n x
cokernels' q n
_ = Cokernels N1 x -> Cokernels n x
forall x (n :: N').
Distributive x =>
Cokernels N1 x -> Cokernels n x
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 = (Diagram ('Parallel 'RightToLeft) N2 n (Orientation p)
 -> LimesG
      Cone
      Dst
      'Injective
      Diagram
      ('Parallel 'RightToLeft)
      N2
      n
      (Orientation p))
-> LimitsG
     Cone
     Dst
     'Injective
     Diagram
     ('Parallel 'RightToLeft)
     N2
     n
     (Orientation p)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (p
-> Diagram ('Parallel 'RightToLeft) N2 n (Orientation p)
-> LimesG
     Cone
     Dst
     'Injective
     Diagram
     ('Parallel 'RightToLeft)
     N2
     n
     (Orientation p)
forall p x (n :: N').
(Entity p, x ~ Orientation p) =>
p -> CokernelDiagram n x -> Cokernel n x
cokrn p
t) where
  cokrn :: (Entity p, x ~ Orientation p) => p -> CokernelDiagram n x -> Cokernel n x
  cokrn :: forall p x (n :: N').
(Entity p, x ~ Orientation p) =>
p -> CokernelDiagram n x -> Cokernel n x
cokrn p
t d :: CokernelDiagram n x
d@(DiagramParallelRL Point x
p Point x
_ FinList n x
_) = Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
-> (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
    -> x)
-> LimesG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Injective d t n m x
-> (Cone s 'Injective d t n m x -> x)
-> LimesG c s 'Injective d t n m x
LimesInjective Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
l Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x -> x
u where
    l :: Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
l = CokernelDiagram n x
-> x -> Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) N2 m a
ConeCokernel CokernelDiagram n x
d (p
Point x
pp -> p -> Orientation p
forall p. p -> p -> Orientation p
:>p
t)
    u :: Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n x -> x
u (ConeCokernel CokernelDiagram n x
_ x
x) = p
t p -> p -> Orientation p
forall p. p -> p -> Orientation p
:> x -> Point x
forall q. Oriented q => q -> Point q
end x
x

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

-- prpIsKernel -


relIsKernel :: Eq x => Kernel n x -> FinList n x -> x -> Statement
relIsKernel :: forall x (n :: N').
Eq x =>
Kernel n x -> FinList n x -> x -> Statement
relIsKernel (LimesProjective (ConeKernel Diagram ('Parallel 'LeftToRight) N2 n x
d x
k') Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n x -> x
_) FinList n x
fs x
k
  = [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (FinList n x
fs FinList n x -> FinList n x -> Bool
forall a. Eq a => a -> a -> Bool
== Diagram ('Parallel 'LeftToRight) N2 n x -> FinList n x
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows Diagram ('Parallel 'LeftToRight) N2 n x
d) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"fs"String -> String -> Parameter
:=FinList n x -> String
forall a. Show a => a -> String
show FinList n x
fs, String
"d"String -> String -> Parameter
:= Diagram ('Parallel 'LeftToRight) N2 n x -> String
forall a. Show a => a -> String
show Diagram ('Parallel 'LeftToRight) N2 n x
d]
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (x
k x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
k') Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"k"String -> String -> Parameter
:= x -> String
forall a. Show a => a -> String
show x
k, String
"k'"String -> String -> Parameter
:= x -> String
forall a. Show a => a -> String
show x
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
:<=>: Kernel n a -> FinList n a -> a -> Statement
forall x (n :: N').
Eq x =>
Kernel n x -> FinList n x -> x -> 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 x => Cokernel n x -> FinList n x -> x -> Statement
prpIsCokernel :: forall x (n :: N').
Distributive x =>
Cokernel n x -> FinList n x -> x -> Statement
prpIsCokernel Cokernel n x
coker FinList n x
fs x
k = String -> Label
Prp String
"IsCokernel" Label -> Statement -> Statement
:<=>: Kernel n (Op x) -> FinList n (Op x) -> Op x -> Statement
forall x (n :: N').
Eq x =>
Kernel n x -> FinList n x -> x -> Statement
relIsKernel Dual1
  (LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
  (Op x)
Kernel n (Op x)
ker FinList n (Op x)
fs' Op x
k' where
  Contravariant2 IsoO Dst Op x (Op x)
i    = Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) x (Op x)
toDualOpDst
  SDualBi (Left1 Dual1
  (LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
  (Op x)
ker) = IsoO Dst Op x (Op x)
-> SDualBi
     (LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     x
-> SDualBi
     (LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Dst Op x (Op x)
i (Either1
  (Dual1
     (LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n))
  (LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
  x
-> SDualBi
     (LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Cokernel n x
-> Either1
     (LimesG Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 n)
     (LimesG Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 n)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Cokernel n x
coker))
  fs' :: FinList n (Op x)
fs'                 = (x -> Op x) -> FinList n x -> FinList n (Op x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (IsoO Dst Op x (Op x) -> x -> Op x
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf IsoO Dst Op x (Op x)
i) FinList n x
fs
  k' :: Op x
k'                  = IsoO Dst Op x (Op x) -> x -> Op x
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf IsoO Dst Op x (Op x)
i x
k
  

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

-- XStandardEligibleConeKernel -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeG Cone Dst Projective Diagram (Parallel LeftToRight) N2 n x
  => XStandardEligibleConeKernel n x

instance XStandard p => XStandardEligibleConeKernel n (Orientation p)

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

-- XStandardEligibleConeFactorKernel -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeFactorG Cone Dst Projective Diagram (Parallel LeftToRight) N2 n x
  => XStandardEligibleConeFactorKernel n x

instance XStandard p => XStandardEligibleConeFactorKernel n (Orientation p)

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

-- XStandardEligibleConeCokernel -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeG Cone Dst Injective Diagram (Parallel RightToLeft) N2 n x
  => XStandardEligibleConeCokernel n x

instance XStandard p => XStandardEligibleConeCokernel n (Orientation p)

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

-- XStandardEligibleConeFactorCokernel -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeFactorG Cone Dst Injective Diagram (Parallel RightToLeft) N2 n x
  => XStandardEligibleConeFactorCokernel n x

instance XStandard p => XStandardEligibleConeFactorCokernel n (Orientation p)

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

-- XStandardEligibleConeKernel1 -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeKernel N1 c => XStandardEligibleConeKernel1 c

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

-- XStandardEligibleConeFactorKernel1 -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeFactorKernel N1 c => XStandardEligibleConeFactorKernel1 c

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

-- XStandardEligibleConeCokernel1 -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeCokernel N1 c => XStandardEligibleConeCokernel1 c

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

-- XStandardEligibleConeFactorCokernel1 -


-- | helper class to avoid undecidable instances.

class XStandardEligibleConeFactorCokernel N1 c => XStandardEligibleConeFactorCokernel1 c