{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Entity.Slice.Adjunction

-- Description : cokernel-kernel adjunction

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- 'Cokernel'-'Kernel' 'Adjunction' for 'Slice'd structures. 

module OAlg.Entity.Slice.Adjunction
  (

    -- * Adjunction

    SliceAdjunction(..), slcAdjunction
  , slcCokerKer, slcKerCoker

    -- * Diagram

  , SliceDiagram(..)
  , sdgMapS, sdgMapCov, sdgMapCnt

    -- * Limits

    
  , SliceCokernels, slcCokernelsCone
  , sliceCokernel
  
  , SliceKernels, slcKernelsCone
  , sliceKernel

    -- * X

  , xSliceFactorFrom

    -- * Proposition

  , prpHomOrtSliceAdjunction
  , prpHomMltSliceAdjunction
  ) where

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

import OAlg.Prelude

import OAlg.Category.SDuality
import OAlg.Category.NaturalTransformable
import OAlg.Category.Unify

import OAlg.Data.Either

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

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

import OAlg.Limes.Cone
import OAlg.Limes.Definition
import OAlg.Limes.Limits
import OAlg.Limes.KernelsAndCokernels

import OAlg.Adjunction

import OAlg.Entity.Diagram
import OAlg.Entity.Natural
import OAlg.Entity.FinList
import OAlg.Entity.Slice.Definition
import OAlg.Entity.Slice.Sliced
import OAlg.Entity.Slice.Free

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

-- SliceDiagram -


-- | slice as a kernel respectively cokernel diagram.

data SliceDiagram i t n m x where
  SliceDiagramKernel :: Sliced i x => Slice From i x -> SliceDiagram i (Parallel LeftToRight) N2 N1 x
  SliceDiagramCokernel :: Sliced i x => Slice To i x -> SliceDiagram i (Parallel RightToLeft) N2 N1 x

deriving instance Show (SliceDiagram i t n m x)
deriving instance Eq (SliceDiagram i t n m x)

instance Validable (SliceDiagram i t n m x) where
  valid :: SliceDiagram i t n m x -> Statement
valid (SliceDiagramKernel Slice 'From i x
f)  = Slice 'From i x -> Statement
forall a. Validable a => a -> Statement
valid Slice 'From i x
f
  valid (SliceDiagramCokernel Slice 'To i x
t) = Slice 'To i x -> Statement
forall a. Validable a => a -> Statement
valid Slice 'To i x
t

instance Attestable k => NaturalDiagrammaticFree Dst (SliceDiagram (Free k)) N2 N1

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

-- sdgMapCov -


-- | mapping a slice diagram according to a covariant homomorphism.

sdgMapCovStruct :: HomSlicedOriented i h
  => Struct (Sld i) y -> Variant2 Covariant h x y -> SliceDiagram i t n m x -> SliceDiagram i t n m y
sdgMapCovStruct :: forall (i :: * -> *) (h :: * -> * -> *) y x (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Struct (Sld i) y
-> Variant2 'Covariant h x y
-> SliceDiagram i t n m x
-> SliceDiagram i t n m y
sdgMapCovStruct Struct (Sld i) y
Struct Variant2 'Covariant h x y
h (SliceDiagramKernel Slice 'From i x
d)   = Slice 'From i y -> SliceDiagram i t n m y
Slice 'From i y
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 y
forall (i :: * -> *) x.
Sliced i x =>
Slice 'From i x
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
SliceDiagramKernel (Slice 'From i y -> SliceDiagram i t n m y)
-> Slice 'From i y -> SliceDiagram i t n m y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Variant2 'Covariant h x y -> Slice 'From i x -> Slice 'From i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov Variant2 'Covariant h x y
h Slice 'From i x
d
sdgMapCovStruct Struct (Sld i) y
Struct Variant2 'Covariant h x y
h (SliceDiagramCokernel Slice 'To i x
d) = Slice 'To i y -> SliceDiagram i t n m y
Slice 'To i y
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 y
forall (i :: * -> *) x.
Sliced i x =>
Slice 'To i x
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 x
SliceDiagramCokernel (Slice 'To i y -> SliceDiagram i t n m y)
-> Slice 'To i y -> SliceDiagram i t n m y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Variant2 'Covariant h x y -> Slice 'To i x -> Slice 'To i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov Variant2 'Covariant h x y
h Slice 'To i x
d

-- | mapping a slice diagram according to a covariant homomorphism.

sdgMapCov :: HomSlicedOriented i h
  => Variant2 Covariant h x y -> SliceDiagram i t n m x -> SliceDiagram i t n m y
sdgMapCov :: forall (i :: * -> *) (h :: * -> * -> *) x y (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Variant2 'Covariant h x y
-> SliceDiagram i t n m x -> SliceDiagram i t n m y
sdgMapCov Variant2 'Covariant h x y
h = Struct (Sld i) y
-> Variant2 'Covariant h x y
-> SliceDiagram i t n m x
-> SliceDiagram i t n m y
forall (i :: * -> *) (h :: * -> * -> *) y x (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Struct (Sld i) y
-> Variant2 'Covariant h x y
-> SliceDiagram i t n m x
-> SliceDiagram i t n m y
sdgMapCovStruct (Struct (ObjectClass h) y -> Struct (Sld i) y
forall x. Struct (ObjectClass h) x -> Struct (Sld i) x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Variant2 'Covariant h x y
-> Struct (ObjectClass (Variant2 'Covariant h)) y
forall x y.
Variant2 'Covariant h x y
-> Struct (ObjectClass (Variant2 'Covariant h)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Covariant h x y
h)) Variant2 'Covariant h x y
h

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

-- sdgMapCnt -


-- | mapping a slice diagram according to a contravariant homomorphism.

sdgMapCntStruct :: HomSlicedOriented i h
  => Struct (Sld i) y
  -> Variant2 Contravariant h x y -> SliceDiagram i t n m x -> SliceDiagram i (Dual t) n m y
sdgMapCntStruct :: forall (i :: * -> *) (h :: * -> * -> *) y x (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Struct (Sld i) y
-> Variant2 'Contravariant h x y
-> SliceDiagram i t n m x
-> SliceDiagram i (Dual t) n m y
sdgMapCntStruct Struct (Sld i) y
Struct Variant2 'Contravariant h x y
h (SliceDiagramKernel Slice 'From i x
d)   = Slice 'To i y
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 y
forall (i :: * -> *) x.
Sliced i x =>
Slice 'To i x
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 x
SliceDiagramCokernel (Slice 'To i y
 -> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 y)
-> Slice 'To i y
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Variant2 'Contravariant h x y
-> Slice 'From i x -> Slice (Dual 'From) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt Variant2 'Contravariant h x y
h Slice 'From i x
d
sdgMapCntStruct Struct (Sld i) y
Struct Variant2 'Contravariant h x y
h (SliceDiagramCokernel Slice 'To i x
d) = Slice 'From i y
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 y
forall (i :: * -> *) x.
Sliced i x =>
Slice 'From i x
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
SliceDiagramKernel (Slice 'From i y
 -> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 y)
-> Slice 'From i y
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Variant2 'Contravariant h x y
-> Slice 'To i x -> Slice (Dual 'To) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt Variant2 'Contravariant h x y
h Slice 'To i x
d

-- | mapping a slice diagram according to a contravariant homomorphism.

sdgMapCnt :: HomSlicedOriented i h
  => Variant2 Contravariant h x y -> SliceDiagram i t n m x -> SliceDiagram i (Dual t) n m y
sdgMapCnt :: forall (i :: * -> *) (h :: * -> * -> *) x y (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Variant2 'Contravariant h x y
-> SliceDiagram i t n m x -> SliceDiagram i (Dual t) n m y
sdgMapCnt Variant2 'Contravariant h x y
h = Struct (Sld i) y
-> Variant2 'Contravariant h x y
-> SliceDiagram i t n m x
-> SliceDiagram i (Dual t) n m y
forall (i :: * -> *) (h :: * -> * -> *) y x (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Struct (Sld i) y
-> Variant2 'Contravariant h x y
-> SliceDiagram i t n m x
-> SliceDiagram i (Dual t) n m y
sdgMapCntStruct (Struct (ObjectClass h) y -> Struct (Sld i) y
forall x. Struct (ObjectClass h) x -> Struct (Sld i) x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Variant2 'Contravariant h x y
-> Struct (ObjectClass (Variant2 'Contravariant h)) y
forall x y.
Variant2 'Contravariant h x y
-> Struct (ObjectClass (Variant2 'Contravariant h)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range Variant2 'Contravariant h x y
h)) Variant2 'Contravariant h x y
h

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

-- Duality -


type instance Dual1 (SliceDiagram i t n m) = SliceDiagram i (Dual t) n m

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

-- sdgMapS -


-- | mapping a slice diagram.

sdgMapS :: (HomSlicedOriented i h, t ~ Dual (Dual t))
  => h x y -> SDualBi (SliceDiagram i t n m) x -> SDualBi (SliceDiagram i t n m) y
sdgMapS :: forall (i :: * -> *) (h :: * -> * -> *) (t :: DiagramType) x y
       (n :: N') (m :: N').
(HomSlicedOriented i h, t ~ Dual (Dual t)) =>
h x y
-> SDualBi (SliceDiagram i t n m) x
-> SDualBi (SliceDiagram i t n m) y
sdgMapS = (Variant2 'Covariant h x y
 -> SliceDiagram i t n m x -> SliceDiagram i t n m y)
-> (Variant2 'Covariant h x y
    -> Dual1 (SliceDiagram i t n m) x
    -> Dual1 (SliceDiagram i t n m) y)
-> (Variant2 'Contravariant h x y
    -> SliceDiagram i t n m x -> Dual1 (SliceDiagram i t n m) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (SliceDiagram i t n m) x -> SliceDiagram i t n m y)
-> h x y
-> SDualBi (SliceDiagram i t n m) x
-> SDualBi (SliceDiagram i t n m) y
forall (h :: * -> * -> *) x y (d :: * -> *).
Disjunctive2 h =>
(Variant2 'Covariant h x y -> d x -> d y)
-> (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> Dual1 d x -> d y)
-> h x y
-> SDualBi d x
-> SDualBi d y
vmapBi Variant2 'Covariant h x y
-> SliceDiagram i t n m x -> SliceDiagram i t n m y
forall (i :: * -> *) (h :: * -> * -> *) x y (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Variant2 'Covariant h x y
-> SliceDiagram i t n m x -> SliceDiagram i t n m y
sdgMapCov Variant2 'Covariant h x y
-> Dual1 (SliceDiagram i t n m) x -> Dual1 (SliceDiagram i t n m) y
Variant2 'Covariant h x y
-> SliceDiagram i (Dual t) n m x -> SliceDiagram i (Dual t) n m y
forall (i :: * -> *) (h :: * -> * -> *) x y (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Variant2 'Covariant h x y
-> SliceDiagram i t n m x -> SliceDiagram i t n m y
sdgMapCov Variant2 'Contravariant h x y
-> SliceDiagram i t n m x -> Dual1 (SliceDiagram i t n m) y
Variant2 'Contravariant h x y
-> SliceDiagram i t n m x -> SliceDiagram i (Dual t) n m y
forall (i :: * -> *) (h :: * -> * -> *) x y (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Variant2 'Contravariant h x y
-> SliceDiagram i t n m x -> SliceDiagram i (Dual t) n m y
sdgMapCnt Variant2 'Contravariant h x y
-> Dual1 (SliceDiagram i t n m) x -> SliceDiagram i t n m y
Variant2 'Contravariant h x y
-> SliceDiagram i (Dual t) n m x
-> SliceDiagram i (Dual (Dual t)) n m y
forall (i :: * -> *) (h :: * -> * -> *) x y (t :: DiagramType)
       (n :: N') (m :: N').
HomSlicedOriented i h =>
Variant2 'Contravariant h x y
-> SliceDiagram i t n m x -> SliceDiagram i (Dual t) n m y
sdgMapCnt

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

-- Diagrammatic -


instance Diagrammatic (SliceDiagram i) where
  diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x.
SliceDiagram i t n m x -> Diagram t n m x
diagram (SliceDiagramKernel (SliceFrom i x
_ x
f)) = Point x
-> Point x
-> FinList m x
-> Diagram ('Parallel 'LeftToRight) ('S N1) m x
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR Point x
s Point x
e (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)
    where Point x
s:>Point x
e = x -> Orientation (Point x)
forall q. Oriented q => q -> Orientation (Point q)
orientation x
f
  diagram (SliceDiagramCokernel (SliceTo i x
_ x
t)) = Point x
-> Point x
-> FinList m x
-> Diagram ('Parallel 'RightToLeft) ('S N1) m x
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) m a
DiagramParallelRL Point x
e Point x
s (x
tx -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil)
    where Point x
s:>Point x
e = x -> Orientation (Point x)
forall q. Oriented q => q -> Orientation (Point q)
orientation x
t

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

-- SliceKernels -


-- | generalized kernels according to a slice diagram.

type SliceKernels i c = KernelsG c (SliceDiagram i) N1

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

-- slcKernelsCone -


-- | the induced slice kernels for 'Cone's.

slcKernelsCone :: Distributive x => Kernels N1 x -> SliceKernels i Cone x
slcKernelsCone :: forall x (i :: * -> *).
Distributive x =>
Kernels N1 x -> SliceKernels i Cone x
slcKernelsCone Kernels N1 x
ks = (SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
 -> LimesG
      Cone
      Dst
      'Projective
      (SliceDiagram i)
      ('Parallel 'LeftToRight)
      ('S N1)
      N1
      x)
-> LimitsG
     Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     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.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
-> LimesG
     Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     x
sks where
  sks :: SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
-> LimesG
     Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     x
sks SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
sd = Cone
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  x
-> (Cone
      Dst
      'Projective
      (SliceDiagram i)
      ('Parallel 'LeftToRight)
      ('S N1)
      N1
      x
    -> x)
-> LimesG
     Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     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
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  x
sl Cone
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  x
-> x
su where
    d :: Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
d = SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
-> Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
forall (t :: DiagramType) (n :: N') (m :: N') x.
SliceDiagram i 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 SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
sd
    l :: LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
l = Kernels N1 x
-> Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
-> LimesG
     Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) 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
ks Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
d
    
    sl :: Cone
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  x
sl = SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
-> x
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
sd (KernelConic Cone Diagram 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 (KernelConic Cone Diagram N1 x -> x)
-> KernelConic Cone Diagram N1 x -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
-> KernelConic Cone Diagram N1 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
l) 
    su :: Cone
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  x
-> x
su (ConeKernel SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
_ x
x) = LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
-> KernelConic Cone Diagram N1 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalFactor LimesG
  Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
l (Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
-> x -> KernelConic Cone Diagram N1 x
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) N1 x
d x
x)

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

-- NaturalDiagrammatic -


instance (HomSlicedOriented i h, t ~ Dual (Dual t))
  => ApplicativeG (SDualBi (DiagramG (SliceDiagram i) t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (DiagramG (SliceDiagram i) t n m) x
   -> SDualBi (DiagramG (SliceDiagram i) t n m) y
amapG h x y
h = SDualBi (SliceDiagram i t n m) y
-> SDualBi (DiagramG (SliceDiagram i) t n m) y
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
(Dual1 (d t n m) ~ d (Dual t) n m) =>
SDualBi (d t n m) x -> SDualBi (DiagramG d t n m) x
sdbFromDgmObj (SDualBi (SliceDiagram i t n m) y
 -> SDualBi (DiagramG (SliceDiagram i) t n m) y)
-> (SDualBi (DiagramG (SliceDiagram i) t n m) x
    -> SDualBi (SliceDiagram i t n m) y)
-> SDualBi (DiagramG (SliceDiagram i) t n m) x
-> SDualBi (DiagramG (SliceDiagram i) t n m) y
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
. h x y
-> SDualBi (SliceDiagram i t n m) x
-> SDualBi (SliceDiagram i t n m) y
forall (i :: * -> *) (h :: * -> * -> *) (t :: DiagramType) x y
       (n :: N') (m :: N').
(HomSlicedOriented i h, t ~ Dual (Dual t)) =>
h x y
-> SDualBi (SliceDiagram i t n m) x
-> SDualBi (SliceDiagram i t n m) y
sdgMapS h x y
h (SDualBi (SliceDiagram i t n m) x
 -> SDualBi (SliceDiagram i t n m) y)
-> (SDualBi (DiagramG (SliceDiagram i) t n m) x
    -> SDualBi (SliceDiagram i t n m) x)
-> SDualBi (DiagramG (SliceDiagram i) t n m) x
-> SDualBi (SliceDiagram i t n m) y
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
. SDualBi (DiagramG (SliceDiagram i) t n m) x
-> SDualBi (SliceDiagram i t n m) x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
(Dual1 (d t n m) ~ d (Dual t) n m) =>
SDualBi (DiagramG d t n m) x -> SDualBi (d t n m) x
sdbToDgmObj
  
instance
  ( CategoryDisjunctive h
  , HomSlicedOriented i h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (DiagramG (SliceDiagram i) t n m)) h (->)

instance
  ( CategoryDisjunctive h
  , HomSlicedOriented i h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => NaturalTransformable h (->)
       (SDualBi (DiagramG (SliceDiagram i) t n m)) (SDualBi (DiagramG Diagram t n m))

instance
  ( CategoryDisjunctive h
  , HomSlicedOriented i h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => NaturalDiagrammatic h (SliceDiagram i) t n m

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

-- SliceCokernels -


-- | generalized cokernels according to a slice diagram.

type SliceCokernels i c = CokernelsG c (SliceDiagram i) N1

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

-- slcCokernelsCone -


slcCokernelConeStruct :: Distributive x
  => Variant2 Contravariant (IsoO (Dst,Sld i) Op) x (Op x)
  -> Cokernels N1 x -> SliceCokernels i Cone x
slcCokernelConeStruct :: forall x (i :: * -> *).
Distributive x =>
Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
-> Cokernels N1 x -> SliceCokernels i Cone x
slcCokernelConeStruct (Contravariant2 IsoO (Dst, Sld i) Op x (Op x)
i) Cokernels N1 x
cs = LimitsG
  Cone
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  x
scs where
  
  SDualBi (Left1 Dual1
  (LimitsG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
  (Op x)
ks) = IsoO (Dst, Sld i) Op x (Op x)
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
     x
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
     (Op x)
forall x y.
Inv2 (HomDisj (Dst, Sld i) Op (HomEmpty (Dst, Sld i))) x y
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
     x
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
     y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG IsoO (Dst, Sld i) Op x (Op x)
i (Either1
  (Dual1
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1))
  (LimitsG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
  x
-> SDualBi
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) 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) ('S N1) N1)
     (LimitsG
        Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Cokernels N1 x
cs))
  sks :: SliceKernels i Cone (Op x)
sks = Kernels N1 (Op x) -> SliceKernels i Cone (Op x)
forall x (i :: * -> *).
Distributive x =>
Kernels N1 x -> SliceKernels i Cone x
slcKernelsCone Dual1
  (LimitsG
     Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) N1)
  (Op x)
Kernels N1 (Op x)
ks
  SDualBi (Right1 LimitsG
  Cone
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  x
scs) = Inv2 (HomDisj (Dst, Sld i) Op (HomEmpty (Dst, Sld i))) (Op x) x
-> SDualBi
     (LimitsG
        Cone
        Dst
        'Injective
        (SliceDiagram i)
        ('Parallel 'RightToLeft)
        ('S N1)
        N1)
     (Op x)
-> SDualBi
     (LimitsG
        Cone
        Dst
        'Injective
        (SliceDiagram i)
        ('Parallel 'RightToLeft)
        ('S N1)
        N1)
     x
forall x y.
Inv2 (HomDisj (Dst, Sld i) Op (HomEmpty (Dst, Sld i))) x y
-> SDualBi
     (LimitsG
        Cone
        Dst
        'Injective
        (SliceDiagram i)
        ('Parallel 'RightToLeft)
        ('S N1)
        N1)
     x
-> SDualBi
     (LimitsG
        Cone
        Dst
        'Injective
        (SliceDiagram i)
        ('Parallel 'RightToLeft)
        ('S N1)
        N1)
     y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (IsoO (Dst, Sld i) Op x (Op x)
-> Inv2 (HomDisj (Dst, Sld i) Op (HomEmpty (Dst, Sld i))) (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO (Dst, Sld i) Op x (Op x)
i) (Either1
  (Dual1
     (LimitsG
        Cone
        Dst
        'Injective
        (SliceDiagram i)
        ('Parallel 'RightToLeft)
        ('S N1)
        N1))
  (LimitsG
     Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1)
  (Op x)
-> SDualBi
     (LimitsG
        Cone
        Dst
        'Injective
        (SliceDiagram i)
        ('Parallel 'RightToLeft)
        ('S N1)
        N1)
     (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (SliceKernels i Cone (Op x)
-> Either1
     (LimitsG
        Cone
        Dst
        'Projective
        (SliceDiagram i)
        ('Parallel 'LeftToRight)
        ('S N1)
        N1)
     (LimitsG
        Cone
        Dst
        'Injective
        (SliceDiagram i)
        ('Parallel 'RightToLeft)
        ('S N1)
        N1)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 SliceKernels i Cone (Op x)
sks))

-- | the induced slice cokernels for 'Cone's.

slcCokernelsCone ::
  ( Distributive x
  , Sliced i x
  )
  => Cokernels N1 x -> SliceCokernels i Cone x
slcCokernelsCone :: forall x (i :: * -> *).
(Distributive x, Sliced i x) =>
Cokernels N1 x -> SliceCokernels i Cone x
slcCokernelsCone = Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
-> Cokernels N1 x -> SliceCokernels i Cone x
forall x (i :: * -> *).
Distributive x =>
Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
-> Cokernels N1 x -> SliceCokernels i Cone x
slcCokernelConeStruct Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
forall (i :: * -> *) x.
(Sliced i x, Distributive x) =>
Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
toDualOpDstSld

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

-- SliceAdjunction -


-- | the left and right homomorphisms for the cokernel-kernel adjunction 'slcAdjunction' within

-- a 'Distributive' structure @__d__@.

data SliceAdjunction i c d x y where  
  SliceCokernel :: SliceCokernels i c d
                -> SliceAdjunction i c d (SliceFactor To i d) (SliceFactor From i d)
  SliceKernel   :: SliceKernels i c d
                -> SliceAdjunction i c d (SliceFactor From i d) (SliceFactor To i d) 

instance Show2 (SliceAdjunction i c d) where
  show2 :: forall a b. SliceAdjunction i c d a b -> String
show2 (SliceCokernel SliceCokernels i c d
_) = String
"SliceCokernel"
  show2 (SliceKernel SliceKernels i c d
_)   = String
"SliceKernel"
  
--------------------------------------------------------------------------------

-- SliceAdjunction - Morphism -


instance (Multiplicative d, Sliced i d) => Morphism (SliceAdjunction i c d) where
  type ObjectClass (SliceAdjunction i c d) = Mlt
  homomorphous :: forall x y.
SliceAdjunction i c d x y
-> Homomorphous (ObjectClass (SliceAdjunction i c d)) x y
homomorphous (SliceCokernel SliceCokernels i c d
_) = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct Struct Mlt x -> Struct Mlt y -> Homomorphous Mlt x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Mlt y
forall s x. Structure s x => Struct s x
Struct
  homomorphous (SliceKernel SliceKernels i c d
_)   = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct Struct Mlt x -> Struct Mlt y -> Homomorphous Mlt x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Mlt y
forall s x. Structure s x => Struct s x
Struct

instance TransformableObjectClassTyp (SliceAdjunction i c d)

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

-- SliceAdjunction - Entity -


{-
deriving instance Show (SliceAdjunction i c d x y)

instance Show2 (SliceAdjunction c k i d)

deriving instance Eq (SliceAdjunction c k i d x y)
instance Eq2 (SliceAdjunction c k i d)

instance Validable (SliceAdjunction c k i d x y) where
  valid SliceCokernel = SValid
  valid SliceKernel   = SValid
instance Validable2 (SliceAdjunction c k i d)
-}

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

-- sliceKernel -


-- | the slice factor 'To' according to the given slice kernels and a slice 'From'. It is

-- the base for 'SliceKernel'.

sliceKernel ::
  ( Distributive d
  , Sliced i d
  , Conic c
  )
  => SliceKernels i c d -> SliceFactor From i d -> SliceFactor To i d
sliceKernel :: forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceKernels i c d -> SliceFactor 'From i d -> SliceFactor 'To i d
sliceKernel SliceKernels i c d
ks (SliceFactor a :: Slice 'From i d
a@(SliceFrom i d
k d
_) Slice 'From i d
b d
_)
    = Slice 'To i d -> Slice 'To i d -> d -> SliceFactor 'To i d
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor (i d -> d -> Slice 'To i d
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i d
k d
a') (i d -> d -> Slice 'To i d
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i d
k d
b') d
f' where
    bKer :: LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
bKer = SliceKernels i c d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
-> LimesG
     c
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
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 SliceKernels i c d
ks (Slice 'From i d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
forall (i :: * -> *) x.
Sliced i x =>
Slice 'From i x
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
SliceDiagramKernel Slice 'From i d
b)
    bDgm :: SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
bDgm = Cone
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
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 (Cone
   Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d)
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
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 (c Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> Cone
      Dst
      'Projective
      (SliceDiagram i)
      ('Parallel 'LeftToRight)
      ('S N1)
      N1
      d)
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
bKer
    aKer :: LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
aKer = SliceKernels i c d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
-> LimesG
     c
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
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 SliceKernels i c d
ks (Slice 'From i d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
forall (i :: * -> *) x.
Sliced i x =>
Slice 'From i x
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
SliceDiagramKernel Slice 'From i d
a)
    
    a' :: d
a' = c Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> d
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 (c Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> d)
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone (LimesG
   c
   Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> c Dst
      'Projective
      (SliceDiagram i)
      ('Parallel 'LeftToRight)
      ('S N1)
      N1
      d)
-> LimesG
     c
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
aKer
    b' :: d
b' = c Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> d
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 (c Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> d)
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone (LimesG
   c
   Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> c Dst
      'Projective
      (SliceDiagram i)
      ('Parallel 'LeftToRight)
      ('S N1)
      N1
      d)
-> LimesG
     c
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
bKer
    f' :: d
f' = LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalFactor LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
bKer (SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
-> d
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
bDgm d
a')
    -- from SliceFactor a b f valid follows that ConeKernel (diagram bKer) a' is eligible


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

-- sliceCokernel -


-- | the slice factor 'From' according to the given slice cokernels and a slice 'To'. It is

-- the base for 'SliceCokernel'.

sliceCokernel ::
  ( Distributive d
  , Sliced i d
  , Conic c
  )
  => SliceCokernels i c d -> SliceFactor To i d -> SliceFactor From i d
sliceCokernel :: forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceCokernels i c d
-> SliceFactor 'To i d -> SliceFactor 'From i d
sliceCokernel SliceCokernels i c d
cs (SliceFactor a :: Slice 'To i d
a@(SliceTo i d
k d
_) Slice 'To i d
b d
_)
    = Slice 'From i d -> Slice 'From i d -> d -> SliceFactor 'From i d
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor (i d -> d -> Slice 'From i d
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i d
k d
a') (i d -> d -> Slice 'From i d
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i d
k d
b') d
f' where
  
    aCoker :: LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
aCoker = SliceCokernels i c d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
-> LimesG
     c
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
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 SliceCokernels i c d
cs (Slice 'To i d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
forall (i :: * -> *) x.
Sliced i x =>
Slice 'To i x
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 x
SliceDiagramCokernel Slice 'To i d
a)
    aDgm :: SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
aDgm   = Cone
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
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 (Cone
   Dst
   'Injective
   (SliceDiagram i)
   ('Parallel 'RightToLeft)
   ('S N1)
   N1
   d
 -> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d)
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
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 (c Dst
   'Injective
   (SliceDiagram i)
   ('Parallel 'RightToLeft)
   ('S N1)
   N1
   d
 -> Cone
      Dst
      'Injective
      (SliceDiagram i)
      ('Parallel 'RightToLeft)
      ('S N1)
      N1
      d)
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
aCoker
    bCoker :: LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
bCoker = SliceCokernels i c d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
-> LimesG
     c
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
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 SliceCokernels i c d
cs (Slice 'To i d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
forall (i :: * -> *) x.
Sliced i x =>
Slice 'To i x
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 x
SliceDiagramCokernel Slice 'To i d
b)
    
    a' :: d
a' = c Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> d
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 (c Dst
   'Injective
   (SliceDiagram i)
   ('Parallel 'RightToLeft)
   ('S N1)
   N1
   d
 -> d)
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
aCoker
    b' :: d
b' = c Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> d
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 (c Dst
   'Injective
   (SliceDiagram i)
   ('Parallel 'RightToLeft)
   ('S N1)
   N1
   d
 -> d)
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone (LimesG
   c
   Dst
   'Injective
   (SliceDiagram i)
   ('Parallel 'RightToLeft)
   ('S N1)
   N1
   d
 -> c Dst
      'Injective
      (SliceDiagram i)
      ('Parallel 'RightToLeft)
      ('S N1)
      N1
      d)
-> LimesG
     c
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
bCoker
    f' :: d
f' = LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalFactor LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
aCoker (SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
-> d
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'RightToLeft) ('S N1) m a
-> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) m a
ConeCokernel SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
aDgm d
b')
    -- from SliceFactor a b f valid follwos that

    -- ConeCokernel (diagram aCoker) b' is eligible


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

-- SliceAdjunction - HomMultiplicative -


instance (Distributive d, Sliced i d, Conic c)
  => ApplicativeG Id (SliceAdjunction i c d) (->) where
  
  amapG :: forall x y. SliceAdjunction i c d x y -> Id x -> Id y
amapG (SliceCokernel SliceCokernels i c d
cs) = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG (SliceCokernels i c d
-> SliceFactor 'To i d -> SliceFactor 'From i d
forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceCokernels i c d
-> SliceFactor 'To i d -> SliceFactor 'From i d
sliceCokernel SliceCokernels i c d
cs)
  amapG (SliceKernel SliceKernels i c d
ks)   = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG (SliceKernels i c d -> SliceFactor 'From i d -> SliceFactor 'To i d
forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceKernels i c d -> SliceFactor 'From i d -> SliceFactor 'To i d
sliceKernel SliceKernels i c d
ks)

instance (Distributive d, Sliced i d, Conic c)
  => ApplicativeG Pnt (SliceAdjunction i c d) (->) where
  
  amapG :: forall x y. SliceAdjunction i c d x y -> Pnt x -> Pnt y
amapG (SliceCokernel SliceCokernels i c d
cs) (Pnt a :: Point x
a@(SliceTo i d
k d
_)) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt (i d -> d -> Slice 'From i d
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i d
k d
a') where
    a' :: d
a' = CokernelConic c (SliceDiagram i) N1 d -> d
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 (SliceDiagram i) N1 d -> d)
-> CokernelConic c (SliceDiagram i) N1 d -> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> CokernelConic c (SliceDiagram i) N1 d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone (LimesG
   c
   Dst
   'Injective
   (SliceDiagram i)
   ('Parallel 'RightToLeft)
   ('S N1)
   N1
   d
 -> CokernelConic c (SliceDiagram i) N1 d)
-> LimesG
     c
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> CokernelConic c (SliceDiagram i) N1 d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SliceCokernels i c d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
-> LimesG
     c
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
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 SliceCokernels i c d
cs (Slice 'To i d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
forall (i :: * -> *) x.
Sliced i x =>
Slice 'To i x
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 x
SliceDiagramCokernel Point x
Slice 'To i d
a)

  amapG (SliceKernel SliceKernels i c d
ks) (Pnt a :: Point x
a@(SliceFrom i d
k d
_)) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt (i d -> d -> Slice 'To i d
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i d
k d
a') where
    a' :: d
a' = KernelConic c (SliceDiagram i) N1 d -> d
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 (SliceDiagram i) N1 d -> d)
-> KernelConic c (SliceDiagram i) N1 d -> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> KernelConic c (SliceDiagram i) N1 d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone (LimesG
   c
   Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> KernelConic c (SliceDiagram i) N1 d)
-> LimesG
     c
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> KernelConic c (SliceDiagram i) N1 d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SliceKernels i c d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
-> LimesG
     c
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
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 SliceKernels i c d
ks (Slice 'From i d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
forall (i :: * -> *) x.
Sliced i x =>
Slice 'From i x
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
SliceDiagramKernel Point x
Slice 'From i d
a)


instance (Distributive d, Sliced i d, Conic c) => HomOriented (SliceAdjunction i c d)
instance (Distributive d, Sliced i d, Conic c) => HomMultiplicative (SliceAdjunction i c d)

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

-- xSliceFactorTo -


-- | random variable for @'SliceFactor' 'To' __i__ __d__@.

xSliceFactorTo :: (Multiplicative d, Sliced i d)
  => XOrtSite To d -> i d -> X (SliceFactor To i d)
xSliceFactorTo :: forall d (i :: * -> *).
(Multiplicative d, Sliced i d) =>
XOrtSite 'To d -> i d -> X (SliceFactor 'To i d)
xSliceFactorTo (XEnd X (Point d)
_ Point d -> X d
xTo) i d
i = do
  d
a <- Point d -> X d
xTo Point d
p
  d
f <- Point d -> X d
xTo (d -> Point d
forall q. Oriented q => q -> Point q
start d
a)
  SliceFactor 'To i d -> X (SliceFactor 'To i d)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Slice 'To i d -> Slice 'To i d -> d -> SliceFactor 'To i d
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor (i d -> d -> Slice 'To i d
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i d
i (d
ad -> d -> d
forall c. Multiplicative c => c -> c -> c
*d
f)) (i d -> d -> Slice 'To i d
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i d
i d
a) d
f)
  
  where p :: Point d
p = i d -> Point d
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i d
i

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

-- xSliceFactorFrom -


-- | random variable for @'SliceFactor' 'From' __i__ __d__@.

xSliceFactorFrom :: (Multiplicative d, Sliced i d)
  => XOrtSite From d -> i d -> X (SliceFactor From i d)
xSliceFactorFrom :: forall d (i :: * -> *).
(Multiplicative d, Sliced i d) =>
XOrtSite 'From d -> i d -> X (SliceFactor 'From i d)
xSliceFactorFrom (XStart X (Point d)
_ Point d -> X d
xFrom) i d
i = do
  d
a <- Point d -> X d
xFrom Point d
p
  d
f <- Point d -> X d
xFrom (d -> Point d
forall q. Oriented q => q -> Point q
end d
a)
  SliceFactor 'From i d -> X (SliceFactor 'From i d)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Slice 'From i d -> Slice 'From i d -> d -> SliceFactor 'From i d
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor (i d -> d -> Slice 'From i d
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i d
i d
a) (i d -> d -> Slice 'From i d
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i d
i (d
fd -> d -> d
forall c. Multiplicative c => c -> c -> c
*d
a)) d
f)
  
  where p :: Point d
p = i d -> Point d
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i d
i

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

-- prpHomOrtSliceAdjunction -


-- | validity for the values of 'SliceAdjunction' to be 'HomOriented'.

prpHomOrtSliceAdjunction
  :: (Distributive d, Sliced i d, Conic c)
  => SliceCokernels i c d
  -> SliceKernels i c d
  -> XOrtSite To d
  -> XOrtSite From d
  -> i d
  -> Statement
prpHomOrtSliceAdjunction :: forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceCokernels i c d
-> SliceKernels i c d
-> XOrtSite 'To d
-> XOrtSite 'From d
-> i d
-> Statement
prpHomOrtSliceAdjunction SliceCokernels i c d
cs SliceKernels i c d
ks XOrtSite 'To d
xTo XOrtSite 'From d
xFrom i d
i = String -> Label
Prp String
"HomOrtSliceAdjunction"
  Label -> Statement -> Statement
:<=>: X (SomeApplication (SliceAdjunction i c d)) -> Statement
forall (h :: * -> * -> *).
(HomOriented h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomOriented (SliceCokernels i c d
-> XOrtSite 'To d
-> i d
-> X (SomeApplication (SliceAdjunction i c d))
forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Multiplicative d, Sliced i d) =>
SliceCokernels i c d
-> XOrtSite 'To d
-> i d
-> X (SomeApplication (SliceAdjunction i c d))
xSliceCokernel SliceCokernels i c d
cs XOrtSite 'To d
xTo i d
i X (SomeApplication (SliceAdjunction i c d))
-> X (SomeApplication (SliceAdjunction i c d))
-> X (SomeApplication (SliceAdjunction i c d))
forall a. X a -> X a -> X a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SliceKernels i c d
-> XOrtSite 'From d
-> i d
-> X (SomeApplication (SliceAdjunction i c d))
forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Multiplicative d, Sliced i d) =>
SliceKernels i c d
-> XOrtSite 'From d
-> i d
-> X (SomeApplication (SliceAdjunction i c d))
xSliceKernel SliceKernels i c d
ks XOrtSite 'From d
xFrom i d
i) where
  
  xSliceCokernel :: (Multiplicative d, Sliced i d)
    => SliceCokernels i c d -> XOrtSite To d -> i d -> X (SomeApplication (SliceAdjunction i c d))
  xSliceCokernel :: forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Multiplicative d, Sliced i d) =>
SliceCokernels i c d
-> XOrtSite 'To d
-> i d
-> X (SomeApplication (SliceAdjunction i c d))
xSliceCokernel SliceCokernels i c d
cs XOrtSite 'To d
xTo i d
i = (SliceFactor 'To i d -> SomeApplication (SliceAdjunction i c d))
-> X (SliceFactor 'To i d)
-> X (SomeApplication (SliceAdjunction i c d))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (SliceAdjunction i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
-> SliceFactor 'To i d -> SomeApplication (SliceAdjunction i c d)
forall (h :: * -> * -> *) x y. h x y -> x -> SomeApplication h
SomeApplication (SliceCokernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
forall (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       d.
SliceCokernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
SliceCokernel SliceCokernels i c d
cs)) (X (SliceFactor 'To i d)
 -> X (SomeApplication (SliceAdjunction i c d)))
-> X (SliceFactor 'To i d)
-> X (SomeApplication (SliceAdjunction i c d))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'To d -> i d -> X (SliceFactor 'To i d)
forall d (i :: * -> *).
(Multiplicative d, Sliced i d) =>
XOrtSite 'To d -> i d -> X (SliceFactor 'To i d)
xSliceFactorTo XOrtSite 'To d
xTo i d
i

  xSliceKernel :: (Multiplicative d, Sliced i d)
    => SliceKernels i c d -> XOrtSite From d -> i d -> X (SomeApplication (SliceAdjunction i c d))
  xSliceKernel :: forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Multiplicative d, Sliced i d) =>
SliceKernels i c d
-> XOrtSite 'From d
-> i d
-> X (SomeApplication (SliceAdjunction i c d))
xSliceKernel SliceKernels i c d
ks XOrtSite 'From d
xFrom i d
i = (SliceFactor 'From i d -> SomeApplication (SliceAdjunction i c d))
-> X (SliceFactor 'From i d)
-> X (SomeApplication (SliceAdjunction i c d))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (SliceAdjunction i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
-> SliceFactor 'From i d -> SomeApplication (SliceAdjunction i c d)
forall (h :: * -> * -> *) x y. h x y -> x -> SomeApplication h
SomeApplication (SliceKernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
forall (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       d.
SliceKernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
SliceKernel SliceKernels i c d
ks)) (X (SliceFactor 'From i d)
 -> X (SomeApplication (SliceAdjunction i c d)))
-> X (SliceFactor 'From i d)
-> X (SomeApplication (SliceAdjunction i c d))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'From d -> i d -> X (SliceFactor 'From i d)
forall d (i :: * -> *).
(Multiplicative d, Sliced i d) =>
XOrtSite 'From d -> i d -> X (SliceFactor 'From i d)
xSliceFactorFrom XOrtSite 'From d
xFrom i d
i

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

-- prpHomMltSliceAdjunction -


-- | validity for the values of 'SliceAdjunction' being 'HomMultiplicative'.

prpHomMltSliceAdjunction
  :: (Distributive d, Sliced i d, Conic c)
  => SliceCokernels i c d
  -> SliceKernels i c d
  -> XOrtSite To d
  -> XOrtSite From d
  -> i d
  -> Statement
prpHomMltSliceAdjunction :: forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceCokernels i c d
-> SliceKernels i c d
-> XOrtSite 'To d
-> XOrtSite 'From d
-> i d
-> Statement
prpHomMltSliceAdjunction SliceCokernels i c d
cs SliceKernels i c d
ks XOrtSite 'To d
xTo XOrtSite 'From d
xFrom i d
i = String -> Label
Prp String
"HomMltSliceAdjunction" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ SliceAdjunction i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
-> XHomMlt (SliceFactor 'To i d) -> Statement
forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
h x y -> XHomMlt x -> Statement
prpHomMultiplicative (SliceCokernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
forall (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       d.
SliceCokernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
SliceCokernel SliceCokernels i c d
cs) XHomMlt (SliceFactor 'To i d)
xSlcTo
      , SliceAdjunction i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
-> XHomMlt (SliceFactor 'From i d) -> Statement
forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
h x y -> XHomMlt x -> Statement
prpHomMultiplicative (SliceKernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
forall (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       d.
SliceKernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
SliceKernel SliceKernels i c d
ks) XHomMlt (SliceFactor 'From i d)
xSlcFrom
      ] where

  xSlcTo :: XHomMlt (SliceFactor 'To i d)
xSlcTo   = XOrtSite 'To (SliceFactor 'To i d) -> XHomMlt (SliceFactor 'To i d)
forall x (d :: Site). Multiplicative x => XOrtSite d x -> XHomMlt x
xosHomMlt (XOrtSite 'To (SliceFactor 'To i d)
 -> XHomMlt (SliceFactor 'To i d))
-> XOrtSite 'To (SliceFactor 'To i d)
-> XHomMlt (SliceFactor 'To i d)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'To d -> i d -> XOrtSite 'To (SliceFactor 'To i d)
forall x (i :: * -> *).
(Multiplicative x, Sliced i x) =>
XOrtSite 'To x -> i x -> XOrtSite 'To (SliceFactor 'To i x)
xosXOrtSiteToSliceFactorTo XOrtSite 'To d
xTo i d
i
  xSlcFrom :: XHomMlt (SliceFactor 'From i d)
xSlcFrom = XOrtSite 'From (SliceFactor 'From i d)
-> XHomMlt (SliceFactor 'From i d)
forall x (d :: Site). Multiplicative x => XOrtSite d x -> XHomMlt x
xosHomMlt (XOrtSite 'From (SliceFactor 'From i d)
 -> XHomMlt (SliceFactor 'From i d))
-> XOrtSite 'From (SliceFactor 'From i d)
-> XHomMlt (SliceFactor 'From i d)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XOrtSite 'From d -> i d -> XOrtSite 'From (SliceFactor 'From i d)
forall x (i :: * -> *).
(Multiplicative x, Sliced i x) =>
XOrtSite 'From x -> i x -> XOrtSite 'From (SliceFactor 'From i x)
xosXOrtSiteFromSliceFactorFrom XOrtSite 'From d
xFrom i d
i

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

-- slcCokerKer -


-- | the right unit of the cokernel-kernel adjunction 'slcAdjunction'.

slcCokerKer :: (Distributive d, Sliced i d, Conic c)
  => SliceCokernels i c d
  -> SliceKernels i c d
  -> Slice To i d -> SliceFactor To i d 
slcCokerKer :: forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceCokernels i c d
-> SliceKernels i c d -> Slice 'To i d -> SliceFactor 'To i d
slcCokerKer SliceCokernels i c d
cs SliceKernels i c d
ks a :: Slice 'To i d
a@(SliceTo i d
i d
a') = Slice 'To i d -> Slice 'To i d -> d -> SliceFactor 'To i d
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor Slice 'To i d
a (i d -> d -> Slice 'To i d
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i d
i d
b') d
u where
  f :: Point (SliceFactor 'From i d)
f       = SliceAdjunction i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
-> Point (SliceFactor 'To i d) -> Point (SliceFactor 'From i d)
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap (SliceCokernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
forall (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       d.
SliceCokernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
SliceCokernel SliceCokernels i c d
cs) Point (SliceFactor 'To i d)
Slice 'To i d
a
  fKer :: LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
fKer    = SliceKernels i c d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
-> LimesG
     c
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
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 SliceKernels i c d
ks (Slice 'From i d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
forall (i :: * -> *) x.
Sliced i x =>
Slice 'From i x
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 x
SliceDiagramKernel Point (SliceFactor 'From i d)
Slice 'From i d
f)
  fKerDgm :: SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
fKerDgm = Cone
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
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 (Cone
   Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d)
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
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 (c Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> Cone
      Dst
      'Projective
      (SliceDiagram i)
      ('Parallel 'LeftToRight)
      ('S N1)
      N1
      d)
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
fKer
  b' :: d
b'      = c Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> d
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 (c Dst
   'Projective
   (SliceDiagram i)
   ('Parallel 'LeftToRight)
   ('S N1)
   N1
   d
 -> d)
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> c Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
fKer
  u :: d
u       = LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
-> d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalFactor LimesG
  c
  Dst
  'Projective
  (SliceDiagram i)
  ('Parallel 'LeftToRight)
  ('S N1)
  N1
  d
fKer (SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
-> d
-> Cone
     Dst
     'Projective
     (SliceDiagram i)
     ('Parallel 'LeftToRight)
     ('S N1)
     N1
     d
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel SliceDiagram i ('Parallel 'LeftToRight) ('S N1) N1 d
fKerDgm d
a')

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

-- slcKerCoker -


-- | the left unit of the cokernel-kenrel adjunction 'slcAdjunction'.

slcKerCoker :: (Distributive d, Sliced i d, Conic c)
  => SliceCokernels i c d
  -> SliceKernels i c d
  -> Slice From i d -> SliceFactor From i d
slcKerCoker :: forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceCokernels i c d
-> SliceKernels i c d -> Slice 'From i d -> SliceFactor 'From i d
slcKerCoker SliceCokernels i c d
cs SliceKernels i c d
ks a :: Slice 'From i d
a@(SliceFrom i d
i d
a') = Slice 'From i d -> Slice 'From i d -> d -> SliceFactor 'From i d
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor (i d -> d -> Slice 'From i d
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i d
i d
b') Slice 'From i d
a d
u where
  t :: Point (SliceFactor 'To i d)
t         = SliceAdjunction i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
-> Point (SliceFactor 'From i d) -> Point (SliceFactor 'To i d)
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap (SliceKernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
forall (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       d.
SliceKernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
SliceKernel SliceKernels i c d
ks) Point (SliceFactor 'From i d)
Slice 'From i d
a
  tCoker :: LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
tCoker    = SliceCokernels i c d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
-> LimesG
     c
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
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 SliceCokernels i c d
cs (Slice 'To i d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
forall (i :: * -> *) x.
Sliced i x =>
Slice 'To i x
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 x
SliceDiagramCokernel Point (SliceFactor 'To i d)
Slice 'To i d
t)
  tCokerDgm :: SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
tCokerDgm = Cone
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
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 (Cone
   Dst
   'Injective
   (SliceDiagram i)
   ('Parallel 'RightToLeft)
   ('S N1)
   N1
   d
 -> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d)
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
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 (c Dst
   'Injective
   (SliceDiagram i)
   ('Parallel 'RightToLeft)
   ('S N1)
   N1
   d
 -> Cone
      Dst
      'Injective
      (SliceDiagram i)
      ('Parallel 'RightToLeft)
      ('S N1)
      N1
      d)
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
tCoker
  b' :: d
b'        = c Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> d
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 (c Dst
   'Injective
   (SliceDiagram i)
   ('Parallel 'RightToLeft)
   ('S N1)
   N1
   d
 -> d)
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> d
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> c Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
tCoker
  u :: d
u         = LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
-> d
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalFactor LimesG
  c
  Dst
  'Injective
  (SliceDiagram i)
  ('Parallel 'RightToLeft)
  ('S N1)
  N1
  d
tCoker (SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
-> d
-> Cone
     Dst
     'Injective
     (SliceDiagram i)
     ('Parallel 'RightToLeft)
     ('S N1)
     N1
     d
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'RightToLeft) ('S N1) m a
-> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) m a
ConeCokernel SliceDiagram i ('Parallel 'RightToLeft) ('S N1) N1 d
tCokerDgm d
a')

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

-- slcAdjunction -


-- | the cokernel-kenrel adjunction.

slcAdjunction :: (Distributive d, Sliced i d, Conic c)
  => SliceCokernels i c d
  -> SliceKernels i c d
  -> i d
  -> Adjunction (SliceAdjunction i c d) (SliceFactor From i d) (SliceFactor To i d)
slcAdjunction :: forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceCokernels i c d
-> SliceKernels i c d
-> i d
-> Adjunction
     (SliceAdjunction i c d)
     (SliceFactor 'From i d)
     (SliceFactor 'To i d)
slcAdjunction SliceCokernels i c d
cs SliceKernels i c d
ks i d
_ = SliceAdjunction i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
-> SliceAdjunction
     i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
-> (Point (SliceFactor 'To i d) -> SliceFactor 'To i d)
-> (Point (SliceFactor 'From i d) -> SliceFactor 'From i d)
-> Adjunction
     (SliceAdjunction i c d)
     (SliceFactor 'From i d)
     (SliceFactor 'To i d)
forall (h :: * -> * -> *) c d.
h c d
-> h d c -> (Point c -> c) -> (Point d -> d) -> Adjunction h d c
Adjunction SliceAdjunction i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
l SliceAdjunction i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
r Point (SliceFactor 'To i d) -> SliceFactor 'To i d
Slice 'To i d -> SliceFactor 'To i d
u Point (SliceFactor 'From i d) -> SliceFactor 'From i d
Slice 'From i d -> SliceFactor 'From i d
v where
  l :: SliceAdjunction i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
l = SliceCokernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
forall (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       d.
SliceCokernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'To i d) (SliceFactor 'From i d)
SliceCokernel SliceCokernels i c d
cs
  r :: SliceAdjunction i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
r = SliceKernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
forall (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       d.
SliceKernels i c d
-> SliceAdjunction
     i c d (SliceFactor 'From i d) (SliceFactor 'To i d)
SliceKernel SliceKernels i c d
ks
  u :: Slice 'To i d -> SliceFactor 'To i d
u = SliceCokernels i c d
-> SliceKernels i c d -> Slice 'To i d -> SliceFactor 'To i d
forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceCokernels i c d
-> SliceKernels i c d -> Slice 'To i d -> SliceFactor 'To i d
slcCokerKer SliceCokernels i c d
cs SliceKernels i c d
ks
  v :: Slice 'From i d -> SliceFactor 'From i d
v = SliceCokernels i c d
-> SliceKernels i c d -> Slice 'From i d -> SliceFactor 'From i d
forall d (i :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *).
(Distributive d, Sliced i d, Conic c) =>
SliceCokernels i c d
-> SliceKernels i c d -> Slice 'From i d -> SliceFactor 'From i d
slcKerCoker SliceCokernels i c d
cs SliceKernels i c d
ks