{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE NoImplicitPrelude #-}

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

{-# LANGUAGE UndecidableInstances #-}
-- see comment for UndecidableInstances in OAlg.Limes.Cone.Duality


-- |

-- Module      : OAlg.Limes.Cone.ZeroHead.Duality

-- Description : duality for zero head cones.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- duality for 'ConeZeroHead'. 

module OAlg.Limes.Cone.ZeroHead.Duality
  (
    -- * Mapp

    czMapS, czMapCov, czMapCnt
  ) where

import OAlg.Prelude

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

import OAlg.Entity.Diagram

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

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

import OAlg.Limes.Cone.Definition
import OAlg.Limes.Cone.Conic

import OAlg.Limes.Cone.ZeroHead.Core

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

-- ConeZeroHead - Dual -


type instance Dual1 (ConeZeroHead s p d t n m)  = ConeZeroHead s (Dual p) d (Dual t) n m 

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

-- czMapS -


czMapMltCovStruct ::
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Struct Dst y
  -> Variant2 Covariant h x y -> ConeZeroHead Mlt p d t n m x -> ConeZeroHead Mlt p d t n m y
czMapMltCovStruct :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') y x (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Struct Dst y
-> Variant2 'Covariant h x y
-> ConeZeroHead Mlt p d t n m x
-> ConeZeroHead Mlt p d t n m y
czMapMltCovStruct Struct Dst y
Struct Variant2 'Covariant h x y
h (ConeZeroHead Cone Mlt p d t n (m1 + 1) x
c) = Cone Mlt p d t n (m1 + 1) y -> ConeZeroHead Mlt p d t n (m1 + 1) y
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 (Variant2 'Covariant h x y
-> Cone Mlt p d t n ('S m1) x -> Cone Mlt p d t n ('S m1) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomMultiplicativeDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> Cone Mlt p d t n m x -> Cone Mlt p d t n m y
cnMapMltCov Variant2 'Covariant h x y
h Cone Mlt p d t n (m1 + 1) x
Cone Mlt p d t n ('S m1) x
c)

czMapMltCov :: 
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Variant2 Covariant h x y -> ConeZeroHead Mlt p d t n m x -> ConeZeroHead Mlt p d t n m y
czMapMltCov :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> ConeZeroHead Mlt p d t n m x -> ConeZeroHead Mlt p d t n m y
czMapMltCov Variant2 'Covariant h x y
h = Struct Dst y
-> Variant2 'Covariant h x y
-> ConeZeroHead Mlt p d t n m x
-> ConeZeroHead Mlt p d t n m y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') y x (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Struct Dst y
-> Variant2 'Covariant h x y
-> ConeZeroHead Mlt p d t n m x
-> ConeZeroHead Mlt p d t n m y
czMapMltCovStruct (Struct (ObjectClass h) y -> Struct Dst y
forall x. Struct (ObjectClass h) x -> Struct Dst 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

czMapDstCovStruct :: 
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Struct Dst y
  -> Variant2 Covariant h x y -> ConeZeroHead Dst p d t n m x -> ConeZeroHead Dst p d t n m y
czMapDstCovStruct :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') y x (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Struct Dst y
-> Variant2 'Covariant h x y
-> ConeZeroHead Dst p d t n m x
-> ConeZeroHead Dst p d t n m y
czMapDstCovStruct Struct Dst y
Struct Variant2 'Covariant h x y
h (ConeZeroHead Cone Dst p d t n (m1 + 1) x
c) = Cone Dst p d t n (m1 + 1) y -> ConeZeroHead Dst p d t n (m1 + 1) y
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 (Variant2 'Covariant h x y
-> Cone Dst p d t n ('S m1) x -> Cone Dst p d t n ('S m1) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> Cone Dst p d t n m x -> Cone Dst p d t n m y
cnMapDstCov Variant2 'Covariant h x y
h Cone Dst p d t n (m1 + 1) x
Cone Dst p d t n ('S m1) x
c)

czMapDstCov ::
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Variant2 Covariant h x y -> ConeZeroHead Dst p d t n m x -> ConeZeroHead Dst p d t n m y
czMapDstCov :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> ConeZeroHead Dst p d t n m x -> ConeZeroHead Dst p d t n m y
czMapDstCov Variant2 'Covariant h x y
h = Struct Dst y
-> Variant2 'Covariant h x y
-> ConeZeroHead Dst p d t n m x
-> ConeZeroHead Dst p d t n m y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') y x (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Struct Dst y
-> Variant2 'Covariant h x y
-> ConeZeroHead Dst p d t n m x
-> ConeZeroHead Dst p d t n m y
czMapDstCovStruct (Struct (ObjectClass h) y -> Struct Dst y
forall x. Struct (ObjectClass h) x -> Struct Dst 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

-- | covariant mapping of 'ConeZeroHead'

czMapCov ::
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Variant2 Covariant h x y -> ConeZeroHead s p d t n m x -> ConeZeroHead s p d t n m y
czMapCov :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y s (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> ConeZeroHead s p d t n m x -> ConeZeroHead s p d t n m y
czMapCov Variant2 'Covariant h x y
h cz :: ConeZeroHead s p d t n m x
cz@(ConeZeroHead Cone s p d t n (m1 + 1) x
c) = case Cone s p d t n (m1 + 1) x
c of
  ConeProjective d t n (m1 + 1) x
_ Point x
_ FinList n x
_        -> Variant2 'Covariant h x y
-> ConeZeroHead Mlt p d t n m x -> ConeZeroHead Mlt p d t n m y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> ConeZeroHead Mlt p d t n m x -> ConeZeroHead Mlt p d t n m y
czMapMltCov Variant2 'Covariant h x y
h ConeZeroHead s p d t n m x
ConeZeroHead Mlt p d t n m x
cz
  ConeInjective d t n (m1 + 1) x
_ Point x
_ FinList n x
_         -> Variant2 'Covariant h x y
-> ConeZeroHead Mlt p d t n m x -> ConeZeroHead Mlt p d t n m y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> ConeZeroHead Mlt p d t n m x -> ConeZeroHead Mlt p d t n m y
czMapMltCov Variant2 'Covariant h x y
h ConeZeroHead s p d t n m x
ConeZeroHead Mlt p d t n m x
cz
  ConeKernel d ('Parallel 'LeftToRight) ('S N1) (m1 + 1) x
_ x
_              -> Variant2 'Covariant h x y
-> ConeZeroHead Dst p d t n m x -> ConeZeroHead Dst p d t n m y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> ConeZeroHead Dst p d t n m x -> ConeZeroHead Dst p d t n m y
czMapDstCov Variant2 'Covariant h x y
h ConeZeroHead s p d t n m x
ConeZeroHead Dst p d t n m x
cz
  ConeCokernel d ('Parallel 'RightToLeft) ('S N1) (m1 + 1) x
_ x
_            -> Variant2 'Covariant h x y
-> ConeZeroHead Dst p d t n m x -> ConeZeroHead Dst p d t n m y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> ConeZeroHead Dst p d t n m x -> ConeZeroHead Dst p d t n m y
czMapDstCov Variant2 'Covariant h x y
h ConeZeroHead s p d t n m x
ConeZeroHead Dst p d t n m x
cz
  
czMapMltCntStruct ::
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Struct Dst y
  -> Variant2 Contravariant h x y
  -> ConeZeroHead Mlt p d t n m x -> Dual1 (ConeZeroHead Mlt p d t n m) y
czMapMltCntStruct :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') y x (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Struct Dst y
-> Variant2 'Contravariant h x y
-> ConeZeroHead Mlt p d t n m x
-> Dual1 (ConeZeroHead Mlt p d t n m) y
czMapMltCntStruct Struct Dst y
Struct Variant2 'Contravariant h x y
h (ConeZeroHead Cone Mlt p d t n (m1 + 1) x
c) = Cone Mlt (Dual p) d (Dual t) n (m1 + 1) y
-> ConeZeroHead Mlt (Dual p) d (Dual t) n (m1 + 1) y
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 (Variant2 'Contravariant h x y
-> Cone Mlt p d t n ('S m1) x -> Dual1 (Cone Mlt p d t n ('S m1)) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomMultiplicativeDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> Cone Mlt p d t n m x -> Dual1 (Cone Mlt p d t n m) y
cnMapMltCnt Variant2 'Contravariant h x y
h Cone Mlt p d t n (m1 + 1) x
Cone Mlt p d t n ('S m1) x
c)

czMapMltCnt ::
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Variant2 Contravariant h x y
  -> ConeZeroHead Mlt p d t n m x -> Dual1 (ConeZeroHead Mlt p d t n m) y  
czMapMltCnt :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> ConeZeroHead Mlt p d t n m x
-> Dual1 (ConeZeroHead Mlt p d t n m) y
czMapMltCnt Variant2 'Contravariant h x y
h = Struct Dst y
-> Variant2 'Contravariant h x y
-> ConeZeroHead Mlt p d t n m x
-> Dual1 (ConeZeroHead Mlt p d t n m) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') y x (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Struct Dst y
-> Variant2 'Contravariant h x y
-> ConeZeroHead Mlt p d t n m x
-> Dual1 (ConeZeroHead Mlt p d t n m) y
czMapMltCntStruct (Struct (ObjectClass h) y -> Struct Dst y
forall x. Struct (ObjectClass h) x -> Struct Dst 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

czMapDstCntStruct ::
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Struct Dst y
  -> Variant2 Contravariant h x y
  -> ConeZeroHead Dst p d t n m x -> Dual1 (ConeZeroHead Dst p d t n m) y
czMapDstCntStruct :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') y x (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Struct Dst y
-> Variant2 'Contravariant h x y
-> ConeZeroHead Dst p d t n m x
-> Dual1 (ConeZeroHead Dst p d t n m) y
czMapDstCntStruct Struct Dst y
Struct Variant2 'Contravariant h x y
h (ConeZeroHead Cone Dst p d t n (m1 + 1) x
c) = Cone Dst (Dual p) d (Dual t) n (m1 + 1) y
-> ConeZeroHead Dst (Dual p) d (Dual t) n (m1 + 1) y
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 (Variant2 'Contravariant h x y
-> Cone Dst p d t n ('S m1) x -> Dual1 (Cone Dst p d t n ('S m1)) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> Cone Dst p d t n m x -> Dual1 (Cone Dst p d t n m) y
cnMapDstCnt Variant2 'Contravariant h x y
h Cone Dst p d t n (m1 + 1) x
Cone Dst p d t n ('S m1) x
c)

czMapDstCnt ::
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Variant2 Contravariant h x y
  -> ConeZeroHead Dst p d t n m x -> Dual1 (ConeZeroHead Dst p d t n m) y  
czMapDstCnt :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> ConeZeroHead Dst p d t n m x
-> Dual1 (ConeZeroHead Dst p d t n m) y
czMapDstCnt Variant2 'Contravariant h x y
h = Struct Dst y
-> Variant2 'Contravariant h x y
-> ConeZeroHead Dst p d t n m x
-> Dual1 (ConeZeroHead Dst p d t n m) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') y x (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Struct Dst y
-> Variant2 'Contravariant h x y
-> ConeZeroHead Dst p d t n m x
-> Dual1 (ConeZeroHead Dst p d t n m) y
czMapDstCntStruct (Struct (ObjectClass h) y -> Struct Dst y
forall x. Struct (ObjectClass h) x -> Struct Dst 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

-- | contravariant mapping of 'ConeZeroHead'

czMapCnt ::
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  )
  => Variant2 Contravariant h x y
  -> ConeZeroHead s p d t n m x -> Dual1 (ConeZeroHead s p d t n m) y
czMapCnt :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y s (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> ConeZeroHead s p d t n m x -> Dual1 (ConeZeroHead s p d t n m) y
czMapCnt Variant2 'Contravariant h x y
h cz :: ConeZeroHead s p d t n m x
cz@(ConeZeroHead Cone s p d t n (m1 + 1) x
c) = case Cone s p d t n (m1 + 1) x
c of
  ConeProjective d t n (m1 + 1) x
_ Point x
_ FinList n x
_        -> Variant2 'Contravariant h x y
-> ConeZeroHead Mlt p d t n m x
-> Dual1 (ConeZeroHead Mlt p d t n m) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> ConeZeroHead Mlt p d t n m x
-> Dual1 (ConeZeroHead Mlt p d t n m) y
czMapMltCnt Variant2 'Contravariant h x y
h ConeZeroHead s p d t n m x
ConeZeroHead Mlt p d t n m x
cz
  ConeInjective d t n (m1 + 1) x
_ Point x
_ FinList n x
_         -> Variant2 'Contravariant h x y
-> ConeZeroHead Mlt p d t n m x
-> Dual1 (ConeZeroHead Mlt p d t n m) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> ConeZeroHead Mlt p d t n m x
-> Dual1 (ConeZeroHead Mlt p d t n m) y
czMapMltCnt Variant2 'Contravariant h x y
h ConeZeroHead s p d t n m x
ConeZeroHead Mlt p d t n m x
cz
  ConeKernel d ('Parallel 'LeftToRight) ('S N1) (m1 + 1) x
_ x
_              -> Variant2 'Contravariant h x y
-> ConeZeroHead Dst p d t n m x
-> Dual1 (ConeZeroHead Dst p d t n m) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> ConeZeroHead Dst p d t n m x
-> Dual1 (ConeZeroHead Dst p d t n m) y
czMapDstCnt Variant2 'Contravariant h x y
h ConeZeroHead s p d t n m x
ConeZeroHead Dst p d t n m x
cz
  ConeCokernel d ('Parallel 'RightToLeft) ('S N1) (m1 + 1) x
_ x
_            -> Variant2 'Contravariant h x y
-> ConeZeroHead Dst p d t n m x
-> Dual1 (ConeZeroHead Dst p d t n m) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> ConeZeroHead Dst p d t n m x
-> Dual1 (ConeZeroHead Dst p d t n m) y
czMapDstCnt Variant2 'Contravariant h x y
h ConeZeroHead s p d t n m x
ConeZeroHead Dst p d t n m x
cz

-- | mapping of 'ConeZeroHead'  

czMapS ::
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammatic h d t n m
  , NaturalDiagrammatic h d (Dual t) n m
  , p ~ Dual (Dual p)
  )
  => h x y -> SDualBi (ConeZeroHead s p d t n m) x -> SDualBi (ConeZeroHead s p d t n m) y
czMapS :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') (p :: Perspective) x y s.
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m,
 NaturalDiagrammatic h d (Dual t) n m, p ~ Dual (Dual p)) =>
h x y
-> SDualBi (ConeZeroHead s p d t n m) x
-> SDualBi (ConeZeroHead s p d t n m) y
czMapS = (Variant2 'Covariant h x y
 -> ConeZeroHead s p d t n m x -> ConeZeroHead s p d t n m y)
-> (Variant2 'Covariant h x y
    -> Dual1 (ConeZeroHead s p d t n m) x
    -> Dual1 (ConeZeroHead s p d t n m) y)
-> (Variant2 'Contravariant h x y
    -> ConeZeroHead s p d t n m x
    -> Dual1 (ConeZeroHead s p d t n m) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (ConeZeroHead s p d t n m) x
    -> ConeZeroHead s p d t n m y)
-> h x y
-> SDualBi (ConeZeroHead s p d t n m) x
-> SDualBi (ConeZeroHead s p d 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
-> ConeZeroHead s p d t n m x -> ConeZeroHead s p d t n m y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y s (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> ConeZeroHead s p d t n m x -> ConeZeroHead s p d t n m y
czMapCov Variant2 'Covariant h x y
-> Dual1 (ConeZeroHead s p d t n m) x
-> Dual1 (ConeZeroHead s p d t n m) y
Variant2 'Covariant h x y
-> ConeZeroHead s (Dual p) d (Dual t) n m x
-> ConeZeroHead s (Dual p) d (Dual t) n m y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y s (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> ConeZeroHead s p d t n m x -> ConeZeroHead s p d t n m y
czMapCov Variant2 'Contravariant h x y
-> ConeZeroHead s p d t n m x -> Dual1 (ConeZeroHead s p d t n m) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y s (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> ConeZeroHead s p d t n m x -> Dual1 (ConeZeroHead s p d t n m) y
czMapCnt Variant2 'Contravariant h x y
-> Dual1 (ConeZeroHead s p d t n m) x -> ConeZeroHead s p d t n m y
Variant2 'Contravariant h x y
-> ConeZeroHead s (Dual p) d (Dual t) n m x
-> Dual1 (ConeZeroHead s (Dual p) d (Dual t) n m) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y s (p :: Perspective).
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> ConeZeroHead s p d t n m x -> Dual1 (ConeZeroHead s p d t n m) y
czMapCnt

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

-- FunctorialG -


instance
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => ApplicativeG (SDualBi (ConeZeroHead s p d t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (ConeZeroHead s p d t n m) x
   -> SDualBi (ConeZeroHead s p d t n m) y
amapG = h x y
-> SDualBi (ConeZeroHead s p d t n m) x
-> SDualBi (ConeZeroHead s p d t n m) y
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') (p :: Perspective) x y s.
(HomDistributiveDisjunctive h, NaturalDiagrammatic h d t n m,
 NaturalDiagrammatic h d (Dual t) n m, p ~ Dual (Dual p)) =>
h x y
-> SDualBi (ConeZeroHead s p d t n m) x
-> SDualBi (ConeZeroHead s p d t n m) y
czMapS

instance
  ( HomDistributiveDisjunctive h
  , FunctorialOriented h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => FunctorialG (SDualBi (ConeZeroHead s p d t n m)) h (->)

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

-- NaturalConic -


instance
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => ApplicativeG (SDualBi (ConeG ConeZeroHead s p d t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (ConeG ConeZeroHead s p d t n m) x
   -> SDualBi (ConeG ConeZeroHead s p d t n m) y
amapG h x y
h = SDualBi (ConeZeroHead s p d t n m) y
-> SDualBi (ConeG ConeZeroHead s p d t n m) y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Dual1 (c s p d t n m) ~ c s (Dual p) d (Dual t) n m) =>
SDualBi (c s p d t n m) x -> SDualBi (ConeG c s p d t n m) x
sdbFromCncObj (SDualBi (ConeZeroHead s p d t n m) y
 -> SDualBi (ConeG ConeZeroHead s p d t n m) y)
-> (SDualBi (ConeG ConeZeroHead s p d t n m) x
    -> SDualBi (ConeZeroHead s p d t n m) y)
-> SDualBi (ConeG ConeZeroHead s p d t n m) x
-> SDualBi (ConeG ConeZeroHead s p d 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 (ConeZeroHead s p d t n m) x
-> SDualBi (ConeZeroHead s p d t n m) y
forall x y.
h x y
-> SDualBi (ConeZeroHead s p d t n m) x
-> SDualBi (ConeZeroHead s p d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h (SDualBi (ConeZeroHead s p d t n m) x
 -> SDualBi (ConeZeroHead s p d t n m) y)
-> (SDualBi (ConeG ConeZeroHead s p d t n m) x
    -> SDualBi (ConeZeroHead s p d t n m) x)
-> SDualBi (ConeG ConeZeroHead s p d t n m) x
-> SDualBi (ConeZeroHead s p d 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 (ConeG ConeZeroHead s p d t n m) x
-> SDualBi (ConeZeroHead 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.
(Dual1 (c s p d t n m) ~ c s (Dual p) d (Dual t) n m) =>
SDualBi (ConeG c s p d t n m) x -> SDualBi (c s p d t n m) x
sdbToCncObj

instance
  ( HomDistributiveDisjunctive h
  , FunctorialOriented h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => FunctorialG (SDualBi (ConeG ConeZeroHead s p d t n m)) h (->) 

instance
  ( HomDistributiveDisjunctive h
  , FunctorialOriented h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => NaturalTransformable h (->)
       (SDualBi (ConeG ConeZeroHead Mlt p d t n m))
       (SDualBi (ConeG Cone Mlt p d t n m))

instance
  ( HomDistributiveDisjunctive h
  , FunctorialOriented h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => NaturalConic h ConeZeroHead Mlt p d t n m