{-# 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
    slcAdjunction

    -- ** Homomorphism
  , SliceCokernelKernel(..)
  , SliceCokernelTo(..)
  , SliceKernelFrom(..)

    -- ** Unit
  , slcCokerKer, slcKerCoker
  
    -- * X
  , xSliceFactorTo, xSliceFactorFrom
  
    -- * Proposition
  , prpHomMltSliceCokernelKernel
  ) where

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

import Data.Typeable

import OAlg.Prelude

import OAlg.Category.Unify

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

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

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

import OAlg.Adjunction

import OAlg.Entity.Natural
import OAlg.Entity.Slice.Definition

--------------------------------------------------------------------------------
-- SliceCokernelKernel -

-- | the left and right homomorphisms for the cokernel-kernel adjunction 'slcAdjunction'.
data SliceCokernelKernel i c x y where  
  SliceCokernel :: SliceCokernelKernel i c (SliceFactor To i c) (SliceFactor From i c)
  SliceKernel   :: SliceCokernelKernel i c (SliceFactor From i c) (SliceFactor To i c) 

--------------------------------------------------------------------------------
-- SliceCokernelKernel - Entity -

deriving instance Show (SliceCokernelKernel i c x y)
instance Show2 (SliceCokernelKernel i c)

deriving instance Eq (SliceCokernelKernel i c x y)
instance Eq2 (SliceCokernelKernel i c)

instance Validable (SliceCokernelKernel i c x y) where
  valid :: SliceCokernelKernel i c x y -> Statement
valid SliceCokernelKernel i c x y
SliceCokernel = Statement
SValid
  valid SliceCokernelKernel i c x y
SliceKernel   = Statement
SValid
instance Validable2 (SliceCokernelKernel i c)


instance (Typeable i, Typeable c, Typeable x, Typeable y)
  => Entity (SliceCokernelKernel i c x y)
instance (Typeable i, Typeable c) => Entity2 (SliceCokernelKernel i c)

--------------------------------------------------------------------------------
-- SliceCokernelTo -

-- | 'Distributive' structures @__c__@ having to each @'Slice' 'To' __i__ __c__@ a
--   'Cokernel'.
--
--  __Property__ Let @h = 'SliceTo' _ h'@ be in @'Slice' 'To' __i__ __c__@ for a
--  @__i__@ sliced, 'Distributive' structure @__c__@, then holds:
--
--  @'diagram' ('universalCone' coker) '==' 'cokernelDiagram' h'@ where
--  @coker = 'sliceCokernelTo' h@.
class (Distributive c, Sliced i c) => SliceCokernelTo i c where
  sliceCokernelTo :: Slice To i c -> Cokernel N1 c

--------------------------------------------------------------------------------
-- SliceKernelFrom -

-- | 'Distributive' structures @__c__@ having to each @'Slice' 'From' __i__ __c__@ a
--   'Kernel'.
--
--  __Property__ Let @h = 'SliceFrom' _ h'@ be in @'Slice' 'From' __i__ __c__@ for a
--  @__i__@ sliced, 'Distributive' structure @__c__@, then holds:
--
--  @'diagram' ('universalCone' ker) '==' 'kernelDiagram' h'@ where
--  @coker = 'sliceKernelFrom' h@.
class (Distributive c, Sliced i c) => SliceKernelFrom i c where
  sliceKernelFrom :: Slice From i c -> Kernel N1 c

--------------------------------------------------------------------------------
-- SliceCokernelKernel - Morphism -

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

instance (Multiplicative c, Sliced i c) => EmbeddableMorphism (SliceCokernelKernel i c) Typ
instance (Multiplicative c, Sliced i c) => EmbeddableMorphismTyp (SliceCokernelKernel i c)
instance (Multiplicative c, Sliced i c) => EmbeddableMorphism (SliceCokernelKernel i c) Ort
instance (Multiplicative c, Sliced i c) => EmbeddableMorphism (SliceCokernelKernel i c) Mlt


--------------------------------------------------------------------------------
-- SliceCokernelKernel - HomMultiplicative -

instance (Distributive c, SliceCokernelTo i c, SliceKernelFrom i c)
  => Applicative (SliceCokernelKernel i c) where
  
  amap :: forall a b. SliceCokernelKernel i c a b -> a -> b
amap SliceCokernelKernel i c a b
SliceCokernel (SliceFactor a :: Slice 'To i c
a@(SliceTo i c
k c
_) Slice 'To i c
b c
_)
    = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor (forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom i c
k c
a') (forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom i c
k c
b') c
f' where
    aCoker :: Cokernel N1 c
aCoker = forall (i :: * -> *) c.
SliceCokernelTo i c =>
Slice 'To i c -> Cokernel N1 c
sliceCokernelTo Slice 'To i c
a
    a' :: c
a' = forall c. CokernelCone N1 c -> c
cokernelFactor forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Cokernel N1 c
aCoker
    b' :: c
b' = forall c. CokernelCone N1 c -> c
cokernelFactor forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (i :: * -> *) c.
SliceCokernelTo i c =>
Slice 'To i c -> Cokernel N1 c
sliceCokernelTo Slice 'To i c
b
    f' :: c
f' = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Cokernel N1 c
aCoker (forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Cokernel N1 c
aCoker) c
b')
    -- from SliceFactor a b f valid follwos that
    -- ConeCokernel (diagram aCoker) b' is eligible

  amap SliceCokernelKernel i c a b
SliceKernel (SliceFactor a :: Slice 'From i c
a@(SliceFrom i c
k c
_) Slice 'From i c
b c
_)
    = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor (forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
k c
a') (forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
k c
b') c
f' where
    bKer :: Kernel N1 c
bKer = forall (i :: * -> *) c.
SliceKernelFrom i c =>
Slice 'From i c -> Kernel N1 c
sliceKernelFrom Slice 'From i c
b
    a' :: c
a' = forall c. KernelCone N1 c -> c
kernelFactor forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (i :: * -> *) c.
SliceKernelFrom i c =>
Slice 'From i c -> Kernel N1 c
sliceKernelFrom Slice 'From i c
a
    b' :: c
b' = forall c. KernelCone N1 c -> c
kernelFactor forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ Kernel N1 c
bKer
    f' :: c
f' = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Kernel N1 c
bKer (forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Kernel N1 c
bKer) c
a')
    -- from SliceFactor a b f valid follows that ConeKernel (diagram bKer) a' is eligible

instance (Distributive c, SliceCokernelTo i c, SliceKernelFrom i c)
  => HomOriented (SliceCokernelKernel i c) where
  pmap :: forall a b. SliceCokernelKernel i c a b -> Point a -> Point b
pmap SliceCokernelKernel i c a b
SliceCokernel a :: Point a
a@(SliceTo i c
k c
_) = forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom i c
k c
a' where
    a' :: c
a' = forall c. CokernelCone N1 c -> c
cokernelFactor forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (i :: * -> *) c.
SliceCokernelTo i c =>
Slice 'To i c -> Cokernel N1 c
sliceCokernelTo Point a
a
  pmap SliceCokernelKernel i c a b
SliceKernel a :: Point a
a@(SliceFrom i c
k c
_) = forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
k c
a' where
    a' :: c
a' = forall c. KernelCone N1 c -> c
kernelFactor forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (i :: * -> *) c.
SliceKernelFrom i c =>
Slice 'From i c -> Kernel N1 c
sliceKernelFrom Point a
a

instance (Distributive c, SliceCokernelTo i c, SliceKernelFrom i c)
  => HomMultiplicative (SliceCokernelKernel i c)

--------------------------------------------------------------------------------
-- xSliceFactorTo -

-- | random variable for @'SliceFactor' 'To' __i__ __c__@.
xSliceFactorTo :: (Multiplicative c, Sliced i c)
  => XOrtSite To c -> i c -> X (SliceFactor To i c)
xSliceFactorTo :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c -> i c -> X (SliceFactor 'To i c)
xSliceFactorTo (XEnd X (Point c)
_ Point c -> X c
xTo) i c
i = do
  c
a <- Point c -> X c
xTo Point c
p
  c
f <- Point c -> X c
xTo (forall q. Oriented q => q -> Point q
start c
a)
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor (forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
i (c
aforall c. Multiplicative c => c -> c -> c
*c
f)) (forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
i c
a) c
f)
  
  where p :: Point c
p = forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i

--------------------------------------------------------------------------------
-- xSliceFactorFrom -

-- | random variable for @'SliceFactor' 'From' __i__ __c__@.
xSliceFactorFrom :: (Multiplicative c, Sliced i c)
  => XOrtSite From c -> i c -> X (SliceFactor From i c)
xSliceFactorFrom :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'From c -> i c -> X (SliceFactor 'From i c)
xSliceFactorFrom (XStart X (Point c)
_ Point c -> X c
xFrom) i c
i = do
  c
a <- Point c -> X c
xFrom Point c
p
  c
f <- Point c -> X c
xFrom (forall q. Oriented q => q -> Point q
end c
a)
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor (forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom i c
i c
a) (forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom i c
i (c
fforall c. Multiplicative c => c -> c -> c
*c
a)) c
f)
  
  where p :: Point c
p = forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i

--------------------------------------------------------------------------------
-- prpHomOrtSliceCokernelKernel -

-- | validity for the values of 'SliceCokernelKernel' to be 'HomOriented'.
prpHomOrtSliceCokernelKernel
  :: (SliceCokernelTo i c, SliceKernelFrom i c)
  => XOrtSite To c
  -> XOrtSite From c
  -> i c
  -> Statement
prpHomOrtSliceCokernelKernel :: forall (i :: * -> *) c.
(SliceCokernelTo i c, SliceKernelFrom i c) =>
XOrtSite 'To c -> XOrtSite 'From c -> i c -> Statement
prpHomOrtSliceCokernelKernel XOrtSite 'To c
xTo XOrtSite 'From c
xFrom i c
i = String -> Label
Prp String
"HomOrtSliceCokernelKernel"
  Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *). Hom Ort h => XHomOrt h -> Statement
prpHomOrt (forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c -> i c -> XHomOrt (SliceCokernelKernel i c)
xSliceCokernel XOrtSite 'To c
xTo i c
i forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'From c -> i c -> XHomOrt (SliceCokernelKernel i c)
xSliceKernel XOrtSite 'From c
xFrom i c
i) where
  
  xSliceCokernel :: (Multiplicative c, Sliced i c)
    => XOrtSite To c -> i c -> XHomOrt (SliceCokernelKernel i c)
  xSliceCokernel :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c -> i c -> XHomOrt (SliceCokernelKernel i c)
xSliceCokernel XOrtSite 'To c
xTo i c
i = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall (h :: * -> * -> *) a b. h a b -> a -> SomeApplication h
SomeApplication forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'To i c) (SliceFactor 'From i c)
SliceCokernel) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c -> i c -> X (SliceFactor 'To i c)
xSliceFactorTo XOrtSite 'To c
xTo i c
i

  xSliceKernel :: (Multiplicative c, Sliced i c)
    => XOrtSite From c -> i c -> XHomOrt (SliceCokernelKernel i c)
  xSliceKernel :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'From c -> i c -> XHomOrt (SliceCokernelKernel i c)
xSliceKernel XOrtSite 'From c
xFrom i c
i = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall (h :: * -> * -> *) a b. h a b -> a -> SomeApplication h
SomeApplication forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'From i c) (SliceFactor 'To i c)
SliceKernel) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'From c -> i c -> X (SliceFactor 'From i c)
xSliceFactorFrom XOrtSite 'From c
xFrom i c
i

--------------------------------------------------------------------------------
-- prpHomMltSliceCokernelKernel -

-- | validity for the values of 'SliceCokernelKernel' to be 'HomMultiplicative'.
prpHomMltSliceCokernelKernel
  :: (SliceCokernelTo i c, SliceKernelFrom i c)
  => XOrtSite To c
  -> XOrtSite From c
  -> i c
  -> Statement
prpHomMltSliceCokernelKernel :: forall (i :: * -> *) c.
(SliceCokernelTo i c, SliceKernelFrom i c) =>
XOrtSite 'To c -> XOrtSite 'From c -> i c -> Statement
prpHomMltSliceCokernelKernel XOrtSite 'To c
xTo XOrtSite 'From c
xFrom i c
i = String -> Label
Prp String
"HomMltSliceCokernelKernel"
  Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *). Hom Mlt h => XHomMlt h -> Statement
prpHomMlt (forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c
-> XOrtSite 'From c -> i c -> XHomMlt (SliceCokernelKernel i c)
xHomMltKernelCokernel XOrtSite 'To c
xTo XOrtSite 'From c
xFrom i c
i) where

  xHomMltKernelCokernel :: (Multiplicative c, Sliced i c)
    => XOrtSite To c -> XOrtSite From c -> i c -> XHomMlt (SliceCokernelKernel i c)
  xHomMltKernelCokernel :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c
-> XOrtSite 'From c -> i c -> XHomMlt (SliceCokernelKernel i c)
xHomMltKernelCokernel XOrtSite 'To c
xTo XOrtSite 'From c
xFrom i c
i
    = forall (h :: * -> * -> *).
X (SomeApplPnt h) -> X (SomeApplMltp2 h) -> XHomMlt h
XHomMlt (X (SomeApplPnt (SliceCokernelKernel i c))
xpCoker forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> X (SomeApplPnt (SliceCokernelKernel i c))
xpKer) (X (SomeApplMltp2 (SliceCokernelKernel i c))
xm2Coker forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> X (SomeApplMltp2 (SliceCokernelKernel i c))
xm2Ker) where
    XHomMlt X (SomeApplPnt (SliceCokernelKernel i c))
xpCoker X (SomeApplMltp2 (SliceCokernelKernel i c))
xm2Coker = forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c -> i c -> XHomMlt (SliceCokernelKernel i c)
xHomMltCokernel XOrtSite 'To c
xTo i c
i
    XHomMlt X (SomeApplPnt (SliceCokernelKernel i c))
xpKer X (SomeApplMltp2 (SliceCokernelKernel i c))
xm2Ker = forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'From c -> i c -> XHomMlt (SliceCokernelKernel i c)
xHomMltKernel XOrtSite 'From c
xFrom i c
i
  
  xHomMltCokernel :: (Multiplicative c, Sliced i c)
    => XOrtSite To c -> i c -> XHomMlt (SliceCokernelKernel i c)
  xHomMltCokernel :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c -> i c -> XHomMlt (SliceCokernelKernel i c)
xHomMltCokernel XOrtSite 'To c
xTo i c
i = forall (h :: * -> * -> *).
X (SomeApplPnt h) -> X (SomeApplMltp2 h) -> XHomMlt h
XHomMlt X (SomeApplPnt (SliceCokernelKernel i c))
xApplPnt X (SomeApplMltp2 (SliceCokernelKernel i c))
xApplMltp2 where
    xApplPnt :: X (SomeApplPnt (SliceCokernelKernel i c))
xApplPnt = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall (h :: * -> * -> *) a b. h a b -> Point a -> SomeApplPnt h
SomeApplPnt forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'To i c) (SliceFactor 'From i c)
SliceCokernel) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (i :: * -> *) c.
Sliced i c =>
XOrtSite 'To c -> i c -> X (Slice 'To i c)
xSliceTo XOrtSite 'To c
xTo i c
i
    xApplMltp2 :: X (SomeApplMltp2 (SliceCokernelKernel i c))
xApplMltp2 = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall (h :: * -> * -> *) a b. h a b -> Mltp2 a -> SomeApplMltp2 h
SomeApplMltp2 forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'To i c) (SliceFactor 'From i c)
SliceCokernel)
               forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp2 c)
xMltp2
               forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c -> i c -> XOrtSite 'To (SliceFactor 'To i c)
xosXOrtSiteToSliceFactorTo XOrtSite 'To c
xTo i c
i

  xHomMltKernel :: (Multiplicative c, Sliced i c)
    => XOrtSite From c -> i c -> XHomMlt (SliceCokernelKernel i c)
  xHomMltKernel :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'From c -> i c -> XHomMlt (SliceCokernelKernel i c)
xHomMltKernel XOrtSite 'From c
xFrom i c
i = forall (h :: * -> * -> *).
X (SomeApplPnt h) -> X (SomeApplMltp2 h) -> XHomMlt h
XHomMlt X (SomeApplPnt (SliceCokernelKernel i c))
xApplPnt X (SomeApplMltp2 (SliceCokernelKernel i c))
xApplMltp2 where
    xApplPnt :: X (SomeApplPnt (SliceCokernelKernel i c))
xApplPnt = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall (h :: * -> * -> *) a b. h a b -> Point a -> SomeApplPnt h
SomeApplPnt forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'From i c) (SliceFactor 'To i c)
SliceKernel) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (i :: * -> *) c.
Sliced i c =>
XOrtSite 'From c -> i c -> X (Slice 'From i c)
xSliceFrom XOrtSite 'From c
xFrom i c
i
    xApplMltp2 :: X (SomeApplMltp2 (SliceCokernelKernel i c))
xApplMltp2 = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall (h :: * -> * -> *) a b. h a b -> Mltp2 a -> SomeApplMltp2 h
SomeApplMltp2 forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'From i c) (SliceFactor 'To i c)
SliceKernel)
               forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp2 c)
xMltp2
               forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'From c -> i c -> XOrtSite 'From (SliceFactor 'From i c)
xosXOrtSiteFromSliceFactorFrom XOrtSite 'From c
xFrom i c
i
  
--------------------------------------------------------------------------------
-- slcCokerKer -

-- | the right unit of the cokernel-kernel adjunction 'slcAdjunction'.
slcCokerKer :: (SliceCokernelTo i c, SliceKernelFrom i c)
    => Slice To i c -> SliceFactor To i c 
slcCokerKer :: forall (i :: * -> *) c.
(SliceCokernelTo i c, SliceKernelFrom i c) =>
Slice 'To i c -> SliceFactor 'To i c
slcCokerKer a :: Slice 'To i c
a@(SliceTo i c
i c
a') = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Slice 'To i c
a (forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
i c
k) c
u where
  aCokerKer :: Kernel N1 c
aCokerKer = forall (i :: * -> *) c.
SliceKernelFrom i c =>
Slice 'From i c -> Kernel N1 c
sliceKernelFrom (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'To i c) (SliceFactor 'From i c)
SliceCokernel Slice 'To i c
a)
  k :: c
k = forall c. KernelCone N1 c -> c
kernelFactor forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Kernel N1 c
aCokerKer
  u :: c
u = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Kernel N1 c
aCokerKer (forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) N2 m a
ConeKernel (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Kernel N1 c
aCokerKer) c
a') 

--------------------------------------------------------------------------------
-- slcKerCoker -

-- | the left unit of the cokernel-kenrel adjunction 'slcAdjunction'.
slcKerCoker :: (SliceCokernelTo i c, SliceKernelFrom i c)
  => Slice From i c -> SliceFactor From i c
slcKerCoker :: forall (i :: * -> *) c.
(SliceCokernelTo i c, SliceKernelFrom i c) =>
Slice 'From i c -> SliceFactor 'From i c
slcKerCoker a :: Slice 'From i c
a@(SliceFrom i c
i c
a') = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor (forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom i c
i c
c) Slice 'From i c
a c
v where
  aKerCoker :: Cokernel N1 c
aKerCoker = forall (i :: * -> *) c.
SliceCokernelTo i c =>
Slice 'To i c -> Cokernel N1 c
sliceCokernelTo (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'From i c) (SliceFactor 'To i c)
SliceKernel Slice 'From i c
a)
  c :: c
c = forall c. CokernelCone N1 c -> c
cokernelFactor forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Cokernel N1 c
aKerCoker
  v :: c
v = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Cokernel N1 c
aKerCoker (forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective ('Parallel 'RightToLeft) N2 m a
ConeCokernel (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Diagram t n m a
diagram Cokernel N1 c
aKerCoker) c
a')

--------------------------------------------------------------------------------
-- slcAdjunction -

-- | the cokernel-kenrel adjunction.
slcAdjunction :: (SliceCokernelTo i c, SliceKernelFrom i c)
  => i c
  -> Adjunction (SliceCokernelKernel i c) (SliceFactor From i c) (SliceFactor To i c)
slcAdjunction :: forall (i :: * -> *) c.
(SliceCokernelTo i c, SliceKernelFrom i c) =>
i c
-> Adjunction
     (SliceCokernelKernel i c)
     (SliceFactor 'From i c)
     (SliceFactor 'To i c)
slcAdjunction i c
_ = forall (h :: * -> * -> *) c d.
h c d
-> h d c -> (Point c -> c) -> (Point d -> d) -> Adjunction h d c
Adjunction forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'To i c) (SliceFactor 'From i c)
l forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'From i c) (SliceFactor 'To i c)
r Slice 'To i c -> SliceFactor 'To i c
u Slice 'From i c -> SliceFactor 'From i c
v where
  l :: SliceCokernelKernel
  i c (SliceFactor 'To i c) (SliceFactor 'From i c)
l = forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'To i c) (SliceFactor 'From i c)
SliceCokernel
  r :: SliceCokernelKernel
  i c (SliceFactor 'From i c) (SliceFactor 'To i c)
r = forall (i :: * -> *) c.
SliceCokernelKernel
  i c (SliceFactor 'From i c) (SliceFactor 'To i c)
SliceKernel
  u :: Slice 'To i c -> SliceFactor 'To i c
u = forall (i :: * -> *) c.
(SliceCokernelTo i c, SliceKernelFrom i c) =>
Slice 'To i c -> SliceFactor 'To i c
slcCokerKer
  v :: Slice 'From i c -> SliceFactor 'From i c
v = forall (i :: * -> *) c.
(SliceCokernelTo i c, SliceKernelFrom i c) =>
Slice 'From i c -> SliceFactor 'From i c
slcKerCoker