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

{-# LANGUAGE NoImplicitPrelude #-}

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

{-# LANGUAGE UndecidableInstances #-}
-- we allow undecidable instances to use NaturalConicBi as constraint for

-- the functorial property for cones! As such we separated this

-- declaration.

--

-- the problem in the declaration for NaturalConicBi is the constraint

-- NaturalDiagrammatic h d (Dual t) n m, which forces undecidable instances,

-- but as we demand t ~ Dual (Dual t) in being

-- NaturalDiagrammatic this should prevent the type checker from indefinite loops...hopfully!


-- |

-- Module      : OAlg.Limes.Cone.Duality

-- Description : definition of duality of cones.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- definition of duality for 'Cone's over 'Diagrammatic' objects.

module OAlg.Limes.Cone.Duality
  (
    -- * Map

    cnMapS  
    -- ** Covariant

  , cnMapCov, cnMapMltCov, cnMapDstCov
  , cnMap, cnMapMlt, cnMapDst

    -- ** Contravariant

  , cnMapCnt, cnMapMltCnt, cnMapDstCnt
  ) where

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Either

import OAlg.Entity.Diagram

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

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

import OAlg.Limes.Cone.Core

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

-- Cone - Duality -


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

instance (Show x, ShowPoint x) => ShowDual1 (Cone s p Diagram t n m) x
instance (Eq x, EqPoint x) => EqDual1 (Cone s p Diagram t n m) x

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

-- cnMapCov -


-- | mapping of a cone under a 'Multiplicative' covariant homomorphism.

cnMapMltCov ::
  ( 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 :: 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 (Covariant2 h x y
h) Cone Mlt p d t n m x
c            = case Struct (ObjectClass h) y -> Struct Mlt y
forall s x. Transformable s Mlt => Struct s x -> Struct Mlt x
tauMlt (h x y -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h x y
h) of
  Struct Mlt y
Struct                  -> case Cone Mlt p d t n m x
c of
    ConeProjective d t n m x
d Point x
t FinList n x
as -> d t n m y
-> Point y -> FinList n y -> Cone Mlt 'Projective d t n m y
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 d t n m y
d' (h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h Point x
t) ((x -> y) -> FinList n x -> FinList n y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h) FinList n x
as) where
      SDualBi (Right1 (DiagramG d t n m y
d')) = h x y
-> SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
h (Either1 (Dual1 (DiagramG d t n m)) (DiagramG d t n m) x
-> SDualBi (DiagramG d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d t n m x
-> Either1 (DiagramG d (Dual t) n m) (DiagramG d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d t n m x -> DiagramG d t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d t n m x
d)))
    ConeInjective d t n m x
d Point x
t FinList n x
as  -> d t n m y
-> Point y -> FinList n y -> Cone Mlt 'Injective d t n m y
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 'Injective d t n m a
ConeInjective d t n m y
d' (h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h Point x
t) ((x -> y) -> FinList n x -> FinList n y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h) FinList n x
as) where
      SDualBi (Right1 (DiagramG d t n m y
d')) = h x y
-> SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
h (Either1 (Dual1 (DiagramG d t n m)) (DiagramG d t n m) x
-> SDualBi (DiagramG d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d t n m x
-> Either1 (DiagramG d (Dual t) n m) (DiagramG d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d t n m x -> DiagramG d t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d t n m x
d)))

-- | mapping of a cone under a 'Distributive' covariant homomorphism.

cnMapDstCov ::
  ( 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 :: 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 (Covariant2 h x y
h) Cone Dst p d t n m x
c = case Struct (ObjectClass h) y -> Struct Dst y
forall s x. Transformable s Dst => Struct s x -> Struct Dst x
tauDst (h x y -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h x y
h) of
  Struct Dst y
Struct                    -> case Cone Dst p d t n m x
c of
    ConeKernel d ('Parallel 'LeftToRight) ('S N1) m x
d x
a          -> d ('Parallel 'LeftToRight) ('S N1) m y
-> y -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m y
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 d ('Parallel 'LeftToRight) ('S N1) m y
d' (h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf h x y
h x
a) where
      SDualBi (Right1 (DiagramG d ('Parallel 'LeftToRight) ('S N1) m y
d')) = h x y
-> SDualBi (DiagramG d ('Parallel 'LeftToRight) ('S N1) m) x
-> SDualBi (DiagramG d ('Parallel 'LeftToRight) ('S N1) m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
h (Either1
  (Dual1 (DiagramG d ('Parallel 'LeftToRight) ('S N1) m))
  (DiagramG d ('Parallel 'LeftToRight) ('S N1) m)
  x
-> SDualBi (DiagramG d ('Parallel 'LeftToRight) ('S N1) m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d ('Parallel 'LeftToRight) ('S N1) m x
-> Either1
     (DiagramG d ('Parallel 'RightToLeft) ('S N1) m)
     (DiagramG d ('Parallel 'LeftToRight) ('S N1) m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d ('Parallel 'LeftToRight) ('S N1) m x
-> DiagramG d ('Parallel 'LeftToRight) ('S N1) m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d ('Parallel 'LeftToRight) ('S N1) m x
d)))
    ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m x
d x
a        -> d ('Parallel 'RightToLeft) ('S N1) m y
-> y -> Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) m y
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 d ('Parallel 'RightToLeft) ('S N1) m y
d' (h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf h x y
h x
a) where
      SDualBi (Right1 (DiagramG d ('Parallel 'RightToLeft) ('S N1) m y
d')) = h x y
-> SDualBi (DiagramG d ('Parallel 'RightToLeft) ('S N1) m) x
-> SDualBi (DiagramG d ('Parallel 'RightToLeft) ('S N1) m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
h (Either1
  (Dual1 (DiagramG d ('Parallel 'RightToLeft) ('S N1) m))
  (DiagramG d ('Parallel 'RightToLeft) ('S N1) m)
  x
-> SDualBi (DiagramG d ('Parallel 'RightToLeft) ('S N1) m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d ('Parallel 'RightToLeft) ('S N1) m x
-> Either1
     (DiagramG d ('Parallel 'LeftToRight) ('S N1) m)
     (DiagramG d ('Parallel 'RightToLeft) ('S N1) m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d ('Parallel 'RightToLeft) ('S N1) m x
-> DiagramG d ('Parallel 'RightToLeft) ('S N1) m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d ('Parallel 'RightToLeft) ('S N1) m x
d)))

-- | covariant mapping of 'Cone'.

cnMapCov ::
  ( HomD s h
  , NaturalDiagrammatic h d t n m
  )
  => Variant2 Covariant h x y -> Cone s p d t n m x -> Cone s p d t n m y
cnMapCov :: forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y (p :: Perspective).
(HomD s h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> Cone s p d t n m x -> Cone s p d t n m y
cnMapCov Variant2 'Covariant h x y
h Cone s p d t n m x
c = case Cone s p d t n m x
c of
  ConeProjective d t n m x
_ Point x
_ FinList n x
_ -> Variant2 'Covariant h x y
-> Cone Mlt p d t n m x -> Cone Mlt p d t n m 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 s p d t n m x
Cone Mlt p d t n m x
c
  ConeInjective d t n m x
_ Point x
_ FinList n x
_  -> Variant2 'Covariant h x y
-> Cone Mlt p d t n m x -> Cone Mlt p d t n m 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 s p d t n m x
Cone Mlt p d t n m x
c
  ConeKernel d ('Parallel 'LeftToRight) ('S N1) m x
_ x
_       -> Variant2 'Covariant h x y
-> Cone Dst p d t n m x -> Cone 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
-> Cone Dst p d t n m x -> Cone Dst p d t n m y
cnMapDstCov Variant2 'Covariant h x y
h Cone s p d t n m x
Cone Dst p d t n m x
c
  ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m x
_ x
_     -> Variant2 'Covariant h x y
-> Cone Dst p d t n m x -> Cone 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
-> Cone Dst p d t n m x -> Cone Dst p d t n m y
cnMapDstCov Variant2 'Covariant h x y
h Cone s p d t n m x
Cone Dst p d t n m x
c
  
--------------------------------------------------------------------------------

-- cnMap -


-- | mapping of a cone under a 'Multiplicative' homomorphism.

cnMapMlt ::
  ( HomMultiplicative h
  , t ~ Dual (Dual t)
  )
  => h x y -> Cone Mlt p Diagram t n m x -> Cone Mlt p Diagram t n m y
cnMapMlt :: forall (h :: * -> * -> *) (t :: DiagramType) x y (p :: Perspective)
       (n :: N') (m :: N').
(HomMultiplicative h, t ~ Dual (Dual t)) =>
h x y -> Cone Mlt p Diagram t n m x -> Cone Mlt p Diagram t n m y
cnMapMlt h x y
h = Variant2 'Covariant (HomDisj Mlt Op h) x y
-> Cone Mlt p Diagram t n m x -> Cone Mlt p Diagram t n m 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 (h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
hCov h x y
h) where
    hCov :: HomMultiplicative h => h x y -> Variant2 Covariant (HomDisj Mlt Op h) x y
    hCov :: forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
hCov = h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
forall (h :: * -> * -> *) s x y (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (HomDisj s o h) x y
homDisj

-- | mapping of a cone under a 'Distributive' homomorphism.

cnMapDst ::
  ( HomDistributive h
  , t ~ Dual (Dual t)
  )
  => h x y -> Cone Dst p Diagram t n m x -> Cone Dst p Diagram t n m y
cnMapDst :: forall (h :: * -> * -> *) (t :: DiagramType) x y (p :: Perspective)
       (n :: N') (m :: N').
(HomDistributive h, t ~ Dual (Dual t)) =>
h x y -> Cone Dst p Diagram t n m x -> Cone Dst p Diagram t n m y
cnMapDst h x y
h = Variant2 'Covariant (HomDisj Dst Op h) x y
-> Cone Dst p Diagram t n m x -> Cone Dst p Diagram 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
-> Cone Dst p d t n m x -> Cone Dst p d t n m y
cnMapDstCov (h x y -> Variant2 'Covariant (HomDisj Dst Op h) x y
forall (h :: * -> * -> *) x y.
HomDistributive h =>
h x y -> Variant2 'Covariant (HomDisj Dst Op h) x y
hCov h x y
h) where
    hCov :: HomDistributive h => h x y -> Variant2 Covariant (HomDisj Dst Op h) x y
    hCov :: forall (h :: * -> * -> *) x y.
HomDistributive h =>
h x y -> Variant2 'Covariant (HomDisj Dst Op h) x y
hCov = h x y -> Variant2 'Covariant (HomDisj Dst Op h) x y
forall (h :: * -> * -> *) s x y (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (HomDisj s o h) x y
homDisj

-- | mapping of a cone under a @__s__@ homomorphism.

cnMap ::
  ( Hom s h
  , t ~ Dual (Dual t)
  )
  => h x y -> Cone s p Diagram t n m x -> Cone s p Diagram t n m y
cnMap :: forall s (h :: * -> * -> *) (t :: DiagramType) x y
       (p :: Perspective) (n :: N') (m :: N').
(Hom s h, t ~ Dual (Dual t)) =>
h x y -> Cone s p Diagram t n m x -> Cone s p Diagram t n m y
cnMap h x y
h Cone s p Diagram t n m x
c = case Cone s p Diagram t n m x
c of
  ConeProjective Diagram t n m x
_ Point x
_ FinList n x
_ -> h x y -> Cone Mlt p Diagram t n m x -> Cone Mlt p Diagram t n m y
forall (h :: * -> * -> *) (t :: DiagramType) x y (p :: Perspective)
       (n :: N') (m :: N').
(HomMultiplicative h, t ~ Dual (Dual t)) =>
h x y -> Cone Mlt p Diagram t n m x -> Cone Mlt p Diagram t n m y
cnMapMlt h x y
h Cone s p Diagram t n m x
Cone Mlt p Diagram t n m x
c
  ConeInjective Diagram t n m x
_ Point x
_ FinList n x
_  -> h x y -> Cone Mlt p Diagram t n m x -> Cone Mlt p Diagram t n m y
forall (h :: * -> * -> *) (t :: DiagramType) x y (p :: Perspective)
       (n :: N') (m :: N').
(HomMultiplicative h, t ~ Dual (Dual t)) =>
h x y -> Cone Mlt p Diagram t n m x -> Cone Mlt p Diagram t n m y
cnMapMlt h x y
h Cone s p Diagram t n m x
Cone Mlt p Diagram t n m x
c
  ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m x
_ x
_       -> h x y -> Cone Dst p Diagram t n m x -> Cone Dst p Diagram t n m y
forall (h :: * -> * -> *) (t :: DiagramType) x y (p :: Perspective)
       (n :: N') (m :: N').
(HomDistributive h, t ~ Dual (Dual t)) =>
h x y -> Cone Dst p Diagram t n m x -> Cone Dst p Diagram t n m y
cnMapDst h x y
h Cone s p Diagram t n m x
Cone Dst p Diagram t n m x
c
  ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m x
_ x
_     -> h x y -> Cone Dst p Diagram t n m x -> Cone Dst p Diagram t n m y
forall (h :: * -> * -> *) (t :: DiagramType) x y (p :: Perspective)
       (n :: N') (m :: N').
(HomDistributive h, t ~ Dual (Dual t)) =>
h x y -> Cone Dst p Diagram t n m x -> Cone Dst p Diagram t n m y
cnMapDst h x y
h Cone s p Diagram t n m x
Cone Dst p Diagram t n m x
c
  
--------------------------------------------------------------------------------

-- cnMapCnt -


-- | mapping of a cone under a 'Multiplicative' contravariant homomorphism.

cnMapMltCnt ::
  ( 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 :: 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 (Contravariant2 h x y
h) Cone Mlt p d t n m x
c = case Struct (ObjectClass h) y -> Struct Mlt y
forall s x. Transformable s Mlt => Struct s x -> Struct Mlt x
tauMlt (h x y -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h x y
h) of
  Struct Mlt y
Struct                        -> case Cone Mlt p d t n m x
c of
    ConeProjective d t n m x
d Point x
t FinList n x
as       -> d (Dual t) n m y
-> Point y -> FinList n y -> Cone Mlt 'Injective d (Dual t) n m y
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 'Injective d t n m a
ConeInjective d (Dual t) n m y
d' (h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h Point x
t) ((x -> y) -> FinList n x -> FinList n y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf h x y
h) FinList n x
as) where
      SDualBi (Left1 (DiagramG d (Dual t) n m y
d')) = h x y
-> SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
h (Either1 (Dual1 (DiagramG d t n m)) (DiagramG d t n m) x
-> SDualBi (DiagramG d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d t n m x
-> Either1 (DiagramG d (Dual t) n m) (DiagramG d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d t n m x -> DiagramG d t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d t n m x
d)))
    ConeInjective d t n m x
d Point x
t FinList n x
as        -> d (Dual t) n m y
-> Point y -> FinList n y -> Cone Mlt 'Projective d (Dual t) n m y
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 d (Dual t) n m y
d' (h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h Point x
t) ((x -> y) -> FinList n x -> FinList n y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf h x y
h) FinList n x
as) where
      SDualBi (Left1 (DiagramG d (Dual t) n m y
d')) = h x y
-> SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
h (Either1 (Dual1 (DiagramG d t n m)) (DiagramG d t n m) x
-> SDualBi (DiagramG d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d t n m x
-> Either1 (DiagramG d (Dual t) n m) (DiagramG d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d t n m x -> DiagramG d t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d t n m x
d)))

-- | mapping of a cone under a 'Distributive' contravariant homomorphism.

cnMapDstCnt ::
  ( 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 :: 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 (Contravariant2 h x y
h) Cone Dst p d t n m x
c = case Struct (ObjectClass h) y -> Struct Dst y
forall s x. Transformable s Dst => Struct s x -> Struct Dst x
tauDst (h x y -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h x y
h) of
  Struct Dst y
Struct                        -> case Cone Dst p d t n m x
c of
    ConeKernel d ('Parallel 'LeftToRight) ('S N1) m x
d x
a              -> d ('Parallel 'RightToLeft) ('S N1) m y
-> y -> Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) m y
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 d ('Parallel 'RightToLeft) ('S N1) m y
d' (h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf h x y
h x
a) where
      SDualBi (Left1 (DiagramG d ('Parallel 'RightToLeft) ('S N1) m y
d')) = h x y
-> SDualBi (DiagramG d ('Parallel 'LeftToRight) ('S N1) m) x
-> SDualBi (DiagramG d ('Parallel 'LeftToRight) ('S N1) m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
h (Either1
  (Dual1 (DiagramG d ('Parallel 'LeftToRight) ('S N1) m))
  (DiagramG d ('Parallel 'LeftToRight) ('S N1) m)
  x
-> SDualBi (DiagramG d ('Parallel 'LeftToRight) ('S N1) m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d ('Parallel 'LeftToRight) ('S N1) m x
-> Either1
     (DiagramG d ('Parallel 'RightToLeft) ('S N1) m)
     (DiagramG d ('Parallel 'LeftToRight) ('S N1) m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d ('Parallel 'LeftToRight) ('S N1) m x
-> DiagramG d ('Parallel 'LeftToRight) ('S N1) m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d ('Parallel 'LeftToRight) ('S N1) m x
d)))
    ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m x
d x
a            -> d ('Parallel 'LeftToRight) ('S N1) m y
-> y -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m y
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  d ('Parallel 'LeftToRight) ('S N1) m y
d' (h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf h x y
h x
a) where
      SDualBi (Left1 (DiagramG d ('Parallel 'LeftToRight) ('S N1) m y
d')) = h x y
-> SDualBi (DiagramG d ('Parallel 'RightToLeft) ('S N1) m) x
-> SDualBi (DiagramG d ('Parallel 'RightToLeft) ('S N1) m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF h x y
h (Either1
  (Dual1 (DiagramG d ('Parallel 'RightToLeft) ('S N1) m))
  (DiagramG d ('Parallel 'RightToLeft) ('S N1) m)
  x
-> SDualBi (DiagramG d ('Parallel 'RightToLeft) ('S N1) m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d ('Parallel 'RightToLeft) ('S N1) m x
-> Either1
     (DiagramG d ('Parallel 'LeftToRight) ('S N1) m)
     (DiagramG d ('Parallel 'RightToLeft) ('S N1) m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d ('Parallel 'RightToLeft) ('S N1) m x
-> DiagramG d ('Parallel 'RightToLeft) ('S N1) m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d ('Parallel 'RightToLeft) ('S N1) m x
d)))

-- | mapping of a cone under a contravariant homomorphism.

cnMapCnt :: (HomD s h, NaturalDiagrammatic h d t n m)
  => Variant2 Contravariant h x y
  -> Cone s p d t n m x -> Dual1 (Cone s p d t n m) y
cnMapCnt :: forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y (p :: Perspective).
(HomD s h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> Cone s p d t n m x -> Dual1 (Cone s p d t n m) y
cnMapCnt Variant2 'Contravariant h x y
h Cone s p d t n m x
c = case Cone s p d t n m x
c of
  ConeProjective d t n m x
_ Point x
_ FinList n x
_ -> Variant2 'Contravariant h x y
-> Cone Mlt p d t n m x -> Dual1 (Cone Mlt p d t n m) 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 s p d t n m x
Cone Mlt p d t n m x
c
  ConeInjective d t n m x
_ Point x
_ FinList n x
_  -> Variant2 'Contravariant h x y
-> Cone Mlt p d t n m x -> Dual1 (Cone Mlt p d t n m) 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 s p d t n m x
Cone Mlt p d t n m x
c
  ConeKernel d ('Parallel 'LeftToRight) ('S N1) m x
_ x
_       -> Variant2 'Contravariant h x y
-> Cone Dst p d t n m x -> Dual1 (Cone 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
-> 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 s p d t n m x
Cone Dst p d t n m x
c
  ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m x
_ x
_     -> Variant2 'Contravariant h x y
-> Cone Dst p d t n m x -> Dual1 (Cone 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
-> 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 s p d t n m x
Cone Dst p d t n m x
c

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

-- cnMapS -

-- | mapping of 'Cone'.

cnMapS ::
  ( HomD s h
  , NaturalDiagrammatic h d t n m
  , NaturalDiagrammatic h d (Dual t) n m
  , p ~ Dual (Dual p)
  )
  => h x y -> SDualBi (Cone s p d t n m) x -> SDualBi (Cone s p d t n m) y
cnMapS :: forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') (p :: Perspective) x y.
(HomD s h, NaturalDiagrammatic h d t n m,
 NaturalDiagrammatic h d (Dual t) n m, p ~ Dual (Dual p)) =>
h x y
-> SDualBi (Cone s p d t n m) x -> SDualBi (Cone s p d t n m) y
cnMapS = (Variant2 'Covariant h x y
 -> Cone s p d t n m x -> Cone s p d t n m y)
-> (Variant2 'Covariant h x y
    -> Dual1 (Cone s p d t n m) x -> Dual1 (Cone s p d t n m) y)
-> (Variant2 'Contravariant h x y
    -> Cone s p d t n m x -> Dual1 (Cone s p d t n m) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (Cone s p d t n m) x -> Cone s p d t n m y)
-> h x y
-> SDualBi (Cone s p d t n m) x
-> SDualBi (Cone 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
-> Cone s p d t n m x -> Cone s p d t n m y
forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y (p :: Perspective).
(HomD s h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> Cone s p d t n m x -> Cone s p d t n m y
cnMapCov Variant2 'Covariant h x y
-> Dual1 (Cone s p d t n m) x -> Dual1 (Cone s p d t n m) y
Variant2 'Covariant h x y
-> Cone s (Dual p) d (Dual t) n m x
-> Cone s (Dual p) d (Dual t) n m y
forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y (p :: Perspective).
(HomD s h, NaturalDiagrammatic h d t n m) =>
Variant2 'Covariant h x y
-> Cone s p d t n m x -> Cone s p d t n m y
cnMapCov Variant2 'Contravariant h x y
-> Cone s p d t n m x -> Dual1 (Cone s p d t n m) y
forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y (p :: Perspective).
(HomD s h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> Cone s p d t n m x -> Dual1 (Cone s p d t n m) y
cnMapCnt Variant2 'Contravariant h x y
-> Dual1 (Cone s p d t n m) x -> Cone s p d t n m y
Variant2 'Contravariant h x y
-> Cone s (Dual p) d (Dual t) n m x
-> Dual1 (Cone s (Dual p) d (Dual t) n m) y
forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x y (p :: Perspective).
(HomD s h, NaturalDiagrammatic h d t n m) =>
Variant2 'Contravariant h x y
-> Cone s p d t n m x -> Dual1 (Cone s p d t n m) y
cnMapCnt

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

-- FunctorialG -


-- it is not possible to use the constraint HomD s h to make the declaration more generic!

instance
  ( HomMultiplicativeDisjunctive h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => ApplicativeG (SDualBi (Cone Mlt p d t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (Cone Mlt p d t n m) x -> SDualBi (Cone Mlt p d t n m) y
amapG = h x y
-> SDualBi (Cone Mlt p d t n m) x -> SDualBi (Cone Mlt p d t n m) y
forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') (p :: Perspective) x y.
(HomD s h, NaturalDiagrammatic h d t n m,
 NaturalDiagrammatic h d (Dual t) n m, p ~ Dual (Dual p)) =>
h x y
-> SDualBi (Cone s p d t n m) x -> SDualBi (Cone s p d t n m) y
cnMapS
  
instance
  ( HomMultiplicativeDisjunctive h
  , FunctorialOriented h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => FunctorialG (SDualBi (Cone Mlt p d t n m)) h (->)
  
instance
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => ApplicativeG (SDualBi (Cone Dst p d t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (Cone Dst p d t n m) x -> SDualBi (Cone Dst p d t n m) y
amapG = h x y
-> SDualBi (Cone Dst p d t n m) x -> SDualBi (Cone Dst p d t n m) y
forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') (p :: Perspective) x y.
(HomD s h, NaturalDiagrammatic h d t n m,
 NaturalDiagrammatic h d (Dual t) n m, p ~ Dual (Dual p)) =>
h x y
-> SDualBi (Cone s p d t n m) x -> SDualBi (Cone s p d t n m) y
cnMapS
  
instance
  ( HomDistributiveDisjunctive h
  , FunctorialOriented h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p)
  )
  => FunctorialG (SDualBi (Cone Dst p d t n m)) h (->)