{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}

-- |

-- Module      : OAlg.Limes.Cone.ZeroHead

-- Description : cones with a zero arrow. 

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- cones having a zero for its first arrow.

module OAlg.Limes.Cone.ZeroHead
  (
    ConeZeroHead(..)
  , cnZeroHead
  , cnKernel, cnCokernel
  , cnDiffHead

    -- * Duality

  , module Dl
    
  ) where

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Either

import OAlg.Entity.Natural
import OAlg.Entity.FinList
import OAlg.Entity.Diagram

import OAlg.Structure.Fibred
import OAlg.Structure.Multiplicative
import OAlg.Structure.Additive
import OAlg.Structure.Distributive

import OAlg.Hom.Oriented
import OAlg.Hom.Distributive

import OAlg.Limes.Perspective

import OAlg.Limes.Cone.Definition

import OAlg.Limes.Cone.ZeroHead.Core
import OAlg.Limes.Cone.ZeroHead.Duality as Dl

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

-- cnDiffHead -


-- | subtracts to every arrow of the underlying parallel diagram the first arrow and

-- adapts the shell accordingly.

cnDiffHead :: (Distributive a, Abelian a)
  => Cone Mlt p Diagram (Parallel d) n (m+1) a -> ConeZeroHead Mlt p Diagram (Parallel d) n (m+1) a
cnDiffHead :: forall a (p :: Perspective) (d :: Direction) (n :: N') (m :: N').
(Distributive a, Abelian a) =>
Cone Mlt p Diagram ('Parallel d) n (m + 1) a
-> ConeZeroHead Mlt p Diagram ('Parallel d) n (m + 1) a
cnDiffHead (ConeProjective Diagram ('Parallel d) n (m + 1) a
d Point a
t FinList n a
s) = Cone Mlt 'Projective Diagram ('Parallel d) n (m + 1) a
-> ConeZeroHead Mlt 'Projective Diagram ('Parallel d) n (m + 1) a
Cone Mlt 'Projective Diagram ('Parallel d) n ('S m) a
-> ConeZeroHead Mlt 'Projective Diagram ('Parallel d) n ('S m) a
forall x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m1 :: N').
Distributive x =>
Cone s p d t n (m1 + 1) x -> ConeZeroHead s p d t n (m1 + 1) x
ConeZeroHead (Cone Mlt 'Projective Diagram ('Parallel d) n ('S m) a
 -> ConeZeroHead Mlt 'Projective Diagram ('Parallel d) n ('S m) a)
-> Cone Mlt 'Projective Diagram ('Parallel d) n ('S m) a
-> ConeZeroHead Mlt 'Projective Diagram ('Parallel d) n ('S m) a
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ case Diagram ('Parallel d) n (m + 1) a
d of
  DiagramParallelLR Point a
_ Point a
_ FinList (m + 1) a
_ -> Diagram ('Parallel d) n ('S m) a
-> Point a
-> FinList n a
-> Cone Mlt 'Projective Diagram ('Parallel d) n ('S m) a
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective (Diagram ('Parallel d) n (m + 1) a
-> Diagram ('Parallel d) n (m + 1) a
forall a (d :: Direction) (n :: N') (m :: N').
Abelian a =>
Diagram ('Parallel d) n (m + 1) a
-> Diagram ('Parallel d) n (m + 1) a
dgPrlDiffHead Diagram ('Parallel d) n (m + 1) a
d) Point a
t (a
aa -> FinList N1 a -> FinList (N1 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|(a -> a) -> FinList N1 a -> FinList N1 a
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a -> a
forall {f} {a}. (Root f ~ Root a, Additive a, Fibred f) => f -> a
toZero FinList N1 a
as) where a
a:|FinList n1 a
FinList N1 a
as = FinList n a
s
  DiagramParallelRL Point a
_ Point a
_ FinList (m + 1) a
_ -> Diagram ('Parallel d) n ('S m) a
-> Point a
-> FinList n a
-> Cone Mlt 'Projective Diagram ('Parallel d) n ('S m) a
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective (Diagram ('Parallel d) n (m + 1) a
-> Diagram ('Parallel d) n (m + 1) a
forall a (d :: Direction) (n :: N') (m :: N').
Abelian a =>
Diagram ('Parallel d) n (m + 1) a
-> Diagram ('Parallel d) n (m + 1) a
dgPrlDiffHead Diagram ('Parallel d) n (m + 1) a
d) Point a
t (a -> a
forall {f} {a}. (Root f ~ Root a, Additive a, Fibred f) => f -> a
toZero a
aa -> FinList N1 a -> FinList (N1 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList N1 a
as) where a
a:|FinList n1 a
FinList N1 a
as = FinList n a
s
  
  where toZero :: f -> a
toZero f
a = Root a -> a
forall a. Additive a => Root a -> a
zero (f -> Root f
forall f. Fibred f => f -> Root f
root f
a)

cnDiffHead c :: Cone Mlt p Diagram ('Parallel d) n (m + 1) a
c@(ConeInjective (DiagramParallelLR Point a
_ Point a
_ FinList (m + 1) a
_) Point a
_ FinList n a
_) = ConeZeroHead Mlt p Diagram ('Parallel d) n (m + 1) a
ConeZeroHead
  Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m) a
cz where
  Contravariant2 (Inv2 HomDisjEmpty Dst Op a (Op a)
t HomDisjEmpty Dst Op (Op a) a
f) = Variant2 'Contravariant (IsoO Dst Op) a (Op a)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst
  SDualBi (Left1 Dual1
  (Cone
     Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
  (Op a)
c')  = HomDisjEmpty Dst Op a (Op a)
-> SDualBi
     (Cone
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
     a
-> SDualBi
     (Cone
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
     (Op a)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF HomDisjEmpty Dst Op a (Op a)
t (Either1
  (Dual1
     (Cone
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m)))
  (Cone
     Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
  a
-> SDualBi
     (Cone
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
     a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Cone
  Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m) a
-> Either1
     (Dual1
        (Cone
           Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m)))
     (Cone
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
     a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Cone Mlt p Diagram ('Parallel d) n (m + 1) a
Cone
  Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m) a
c))
  cz' :: ConeZeroHead
  Mlt
  'Projective
  Diagram
  ('Parallel 'RightToLeft)
  ('S N1)
  (m + 1)
  (Op a)
cz'                 = Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'RightToLeft)
  ('S N1)
  (m + 1)
  (Op a)
-> ConeZeroHead
     Mlt
     'Projective
     Diagram
     ('Parallel 'RightToLeft)
     ('S N1)
     (m + 1)
     (Op a)
forall a (p :: Perspective) (d :: Direction) (n :: N') (m :: N').
(Distributive a, Abelian a) =>
Cone Mlt p Diagram ('Parallel d) n (m + 1) a
-> ConeZeroHead Mlt p Diagram ('Parallel d) n (m + 1) a
cnDiffHead Dual1
  (Cone
     Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
  (Op a)
Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'RightToLeft)
  ('S N1)
  (m + 1)
  (Op a)
c'
  SDualBi (Right1 ConeZeroHead
  Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m) a
cz) = HomDisjEmpty Dst Op (Op a) a
-> SDualBi
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
     (Op a)
-> SDualBi
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
     a
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF HomDisjEmpty Dst Op (Op a) a
f (Either1
  (Dual1
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m)))
  (ConeZeroHead
     Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
  (Op a)
-> SDualBi
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
     (Op a)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Dual1
  (ConeZeroHead
     Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
  (Op a)
-> Either1
     (Dual1
        (ConeZeroHead
           Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m)))
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
     (Op a)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Dual1
  (ConeZeroHead
     Mlt 'Injective Diagram ('Parallel 'LeftToRight) ('S N1) ('S m))
  (Op a)
ConeZeroHead
  Mlt
  'Projective
  Diagram
  ('Parallel 'RightToLeft)
  ('S N1)
  (m + 1)
  (Op a)
cz'))
cnDiffHead c :: Cone Mlt p Diagram ('Parallel d) n (m + 1) a
c@(ConeInjective (DiagramParallelRL Point a
_ Point a
_ FinList (m + 1) a
_) Point a
_ FinList n a
_) = ConeZeroHead Mlt p Diagram ('Parallel d) n (m + 1) a
ConeZeroHead
  Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m) a
cz where
  Contravariant2 (Inv2 HomDisjEmpty Dst Op a (Op a)
t HomDisjEmpty Dst Op (Op a) a
f) = Variant2 'Contravariant (IsoO Dst Op) a (Op a)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst
  SDualBi (Left1 Dual1
  (Cone
     Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
  (Op a)
c')  = HomDisjEmpty Dst Op a (Op a)
-> SDualBi
     (Cone
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     a
-> SDualBi
     (Cone
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     (Op a)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF HomDisjEmpty Dst Op a (Op a)
t (Either1
  (Dual1
     (Cone
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m)))
  (Cone
     Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
  a
-> SDualBi
     (Cone
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Cone
  Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m) a
-> Either1
     (Dual1
        (Cone
           Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m)))
     (Cone
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Cone Mlt p Diagram ('Parallel d) n (m + 1) a
Cone
  Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m) a
c))
  cz' :: ConeZeroHead
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S N1)
  (m + 1)
  (Op a)
cz'                 = Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S N1)
  (m + 1)
  (Op a)
-> ConeZeroHead
     Mlt
     'Projective
     Diagram
     ('Parallel 'LeftToRight)
     ('S N1)
     (m + 1)
     (Op a)
forall a (p :: Perspective) (d :: Direction) (n :: N') (m :: N').
(Distributive a, Abelian a) =>
Cone Mlt p Diagram ('Parallel d) n (m + 1) a
-> ConeZeroHead Mlt p Diagram ('Parallel d) n (m + 1) a
cnDiffHead Dual1
  (Cone
     Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
  (Op a)
Cone
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S N1)
  (m + 1)
  (Op a)
c'
  SDualBi (Right1 ConeZeroHead
  Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m) a
cz) = HomDisjEmpty Dst Op (Op a) a
-> SDualBi
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     (Op a)
-> SDualBi
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     a
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF HomDisjEmpty Dst Op (Op a) a
f (Either1
  (Dual1
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m)))
  (ConeZeroHead
     Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
  (Op a)
-> SDualBi
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     (Op a)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Dual1
  (ConeZeroHead
     Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
  (Op a)
-> Either1
     (Dual1
        (ConeZeroHead
           Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m)))
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     (Op a)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Dual1
  (ConeZeroHead
     Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
  (Op a)
ConeZeroHead
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S N1)
  (m + 1)
  (Op a)
cz'))

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

-- cnZeroHead -


-- | embedding of a cone in a distributive structure to its multiplicative cone.

cnZeroHead :: Cone Dst p Diagram t n m a -> ConeZeroHead Mlt p Diagram t n (m+1) a
cnZeroHead :: forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p Diagram t n m a
-> ConeZeroHead Mlt p Diagram t n (m + 1) a
cnZeroHead c :: Cone Dst p Diagram t n m a
c@(ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
_ a
_)   = Cone Mlt p Diagram t n (m + 1) a
-> ConeZeroHead Mlt p Diagram t n (m + 1) a
forall x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m1 :: N').
Distributive x =>
Cone s p d t n (m1 + 1) x -> ConeZeroHead s p d t n (m1 + 1) x
ConeZeroHead (Cone Dst p Diagram t n m a -> Cone Mlt p Diagram t n (m + 1) a
forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p Diagram t n m a -> Cone Mlt p Diagram t n (m + 1) a
cnDstAdjZero Cone Dst p Diagram t n m a
c)
cnZeroHead c :: Cone Dst p Diagram t n m a
c@(ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m a
_ a
_) = Cone Mlt p Diagram t n (m + 1) a
-> ConeZeroHead Mlt p Diagram t n (m + 1) a
forall x s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m1 :: N').
Distributive x =>
Cone s p d t n (m1 + 1) x -> ConeZeroHead s p d t n (m1 + 1) x
ConeZeroHead (Cone Dst p Diagram t n m a -> Cone Mlt p Diagram t n (m + 1) a
forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p Diagram t n m a -> Cone Mlt p Diagram t n (m + 1) a
cnDstAdjZero Cone Dst p Diagram t n m a
c)

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

-- cnKernel -


-- | the kernel cone of a zero headed parallel cone, i.e. the inverse of 'cnZeroHead'.

cnKernel :: (p ~ Projective, t ~ Parallel LeftToRight)
  => ConeZeroHead Mlt p Diagram t n (m+1) a -> Cone Dst p Diagram t n m a
cnKernel :: forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
(p ~ 'Projective, t ~ 'Parallel 'LeftToRight) =>
ConeZeroHead Mlt p Diagram t n (m + 1) a
-> Cone Dst p Diagram t n m a
cnKernel (ConeZeroHead (ConeProjective Diagram t n (m1 + 1) a
d Point a
_ FinList n a
cs)) = case Diagram t n (m1 + 1) a
d of
  DiagramParallelLR Point a
l Point a
r FinList (m1 + 1) a
as -> Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> a
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) m a
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 (Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
forall a (m :: N').
Point a
-> Point a
-> FinList m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) m a
DiagramParallelLR Point a
l Point a
r (FinList (m + 1) a -> FinList m a
forall (n :: N') a. FinList (n + 1) a -> FinList n a
tail FinList (m + 1) a
FinList (m1 + 1) a
as)) (FinList (N1 + 1) a -> a
forall (n :: N') a. FinList (n + 1) a -> a
head FinList n a
FinList (N1 + 1) a
cs)

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

-- cnCokernel


-- | the cokernel cone of a zero headed parallel cone, i.e. the inverse of 'cnZeroHead'.

cnCokernel :: (p ~ Injective, t ~ Parallel RightToLeft, n ~ N2)
  => ConeZeroHead Mlt p Diagram t n (m+1) a -> Cone Dst p Diagram t n m a
cnCokernel :: forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
(p ~ 'Injective, t ~ 'Parallel 'RightToLeft, n ~ 'S N1) =>
ConeZeroHead Mlt p Diagram t n (m + 1) a
-> Cone Dst p Diagram t n m a
cnCokernel cz :: ConeZeroHead Mlt p Diagram t n (m + 1) a
cz@(ConeZeroHead Cone Mlt p Diagram t n (m1 + 1) a
_) = Cone Dst p Diagram t n m a
c where
  Contravariant2 (Inv2 HomDisjEmpty Dst Op a (Op a)
t HomDisjEmpty Dst Op (Op a) a
f) = Variant2 'Contravariant (IsoO Dst Op) a (Op a)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst

  SDualBi (Left1 Dual1
  (ConeZeroHead
     Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
  (Op a)
cz') = HomDisjEmpty Dst Op a (Op a)
-> SDualBi
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     a
-> SDualBi
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     (Op a)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF HomDisjEmpty Dst Op a (Op a)
t (Either1
  (Dual1
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m)))
  (ConeZeroHead
     Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
  a
-> SDualBi
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeZeroHead
  Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m) a
-> Either1
     (Dual1
        (ConeZeroHead
           Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m)))
     (ConeZeroHead
        Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
     a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 ConeZeroHead Mlt p Diagram t n (m + 1) a
ConeZeroHead
  Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m) a
cz))
  c' :: Cone
  Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) m (Op a)
c'                  = ConeZeroHead
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S N1)
  (m + 1)
  (Op a)
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) m (Op a)
forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
(p ~ 'Projective, t ~ 'Parallel 'LeftToRight) =>
ConeZeroHead Mlt p Diagram t n (m + 1) a
-> Cone Dst p Diagram t n m a
cnKernel Dual1
  (ConeZeroHead
     Mlt 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) ('S m))
  (Op a)
ConeZeroHead
  Mlt
  'Projective
  Diagram
  ('Parallel 'LeftToRight)
  ('S N1)
  (m + 1)
  (Op a)
cz'
  SDualBi (Right1 Cone Dst p Diagram t n m a
c)  = HomDisjEmpty Dst Op (Op a) a
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) m)
     (Op a)
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) m) a
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF HomDisjEmpty Dst Op (Op a) a
f (Either1
  (Dual1
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) m))
  (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) m)
  (Op a)
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) m)
     (Op a)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Cone
  Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) m (Op a)
-> Either1
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) m)
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) m)
     (Op a)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Cone
  Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) m (Op a)
c'))