{-# 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.Definition.Duality

-- Description : duality for a limes over a digrammatic object.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- duality of a 'Limes' over a 'OAlg.Entity.Diagram.Diagrammatic.Diagrammatic' object yielding

-- a 'Conic' object.

module OAlg.Limes.Definition.Duality
  (
    -- * Mapping

    lmMapS, lmMapCov, lmMapCnt

  ) where

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Either
import OAlg.Data.Variant

import OAlg.Limes.Cone

import OAlg.Limes.Definition.Core

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

-- LimesG - Dual -


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

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

-- lmMapCov -


-- | covariant mapping of 'LimesG'

lmMapCov :: NaturalConic (Inv2 h) c s p d t n m
  => Variant2 Covariant (Inv2 h) x y
  -> LimesG c s p d t n m x -> LimesG c s p d t n m y
lmMapCov :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s p d t n m y
lmMapCov (Covariant2 Inv2 h x y
i) (LimesProjective c s 'Projective d t n m x
uc Cone s 'Projective d t n m x -> x
uf)
  = c s 'Projective d t n m y
-> (Cone s 'Projective d t n m y -> y)
-> LimesG c s 'Projective d t n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective c s 'Projective d t n m y
uc' Cone s 'Projective d t n m y -> y
uf' where
  SDualBi (Right1 (ConeG c s 'Projective d t n m y
uc')) = Inv2 h x y
-> SDualBi (ConeG c s 'Projective d t n m) x
-> SDualBi (ConeG c s 'Projective d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 h x y
i (Either1
  (Dual1 (ConeG c s 'Projective d t n m))
  (ConeG c s 'Projective d t n m)
  x
-> SDualBi (ConeG c s 'Projective d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG c s 'Projective d t n m x
-> Either1
     (ConeG c s 'Injective d (Dual t) n m)
     (ConeG c s 'Projective d t n m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (c s 'Projective d t n m x -> ConeG c s 'Projective 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG c s 'Projective d t n m x
uc)))  
  uf' :: Cone s 'Projective d t n m y -> y
uf' Cone s 'Projective d t n m y
c' = Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf Inv2 h x y
i (Cone s 'Projective d t n m x -> x
uf Cone s 'Projective d t n m x
c) where
    SDualBi (Right1 (ConeG Cone s 'Projective d t n m x
c)) = Inv2 h y x
-> SDualBi (ConeG Cone s 'Projective d t n m) y
-> SDualBi (ConeG Cone s 'Projective d t n m) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i) (Either1
  (Dual1 (ConeG Cone s 'Projective d t n m))
  (ConeG Cone s 'Projective d t n m)
  y
-> SDualBi (ConeG Cone s 'Projective d t n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s 'Projective d t n m y
-> Either1
     (ConeG Cone s 'Injective d (Dual t) n m)
     (ConeG Cone s 'Projective d t n m)
     y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Cone s 'Projective d t n m y -> ConeG Cone s 'Projective 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG Cone s 'Projective d t n m y
c')))
lmMapCov (Covariant2 Inv2 h x y
i) (LimesInjective c s 'Injective d t n m x
uc Cone s 'Injective d t n m x -> x
uf)
  = c s 'Injective d t n m y
-> (Cone s 'Injective d t n m y -> y)
-> LimesG c s 'Injective d t n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Injective d t n m x
-> (Cone s 'Injective d t n m x -> x)
-> LimesG c s 'Injective d t n m x
LimesInjective c s 'Injective d t n m y
uc' Cone s 'Injective d t n m y -> y
uf' where
  SDualBi (Right1 (ConeG c s 'Injective d t n m y
uc')) = Inv2 h x y
-> SDualBi (ConeG c s 'Injective d t n m) x
-> SDualBi (ConeG c s 'Injective d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 h x y
i (Either1
  (Dual1 (ConeG c s 'Injective d t n m))
  (ConeG c s 'Injective d t n m)
  x
-> SDualBi (ConeG c s 'Injective d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG c s 'Injective d t n m x
-> Either1
     (ConeG c s 'Projective d (Dual t) n m)
     (ConeG c s 'Injective d t n m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (c s 'Injective d t n m x -> ConeG c s 'Injective 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG c s 'Injective d t n m x
uc)))  
  uf' :: Cone s 'Injective d t n m y -> y
uf' Cone s 'Injective d t n m y
c' = Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf Inv2 h x y
i (Cone s 'Injective d t n m x -> x
uf Cone s 'Injective d t n m x
c) where
    SDualBi (Right1 (ConeG Cone s 'Injective d t n m x
c)) = Inv2 h y x
-> SDualBi (ConeG Cone s 'Injective d t n m) y
-> SDualBi (ConeG Cone s 'Injective d t n m) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i) (Either1
  (Dual1 (ConeG Cone s 'Injective d t n m))
  (ConeG Cone s 'Injective d t n m)
  y
-> SDualBi (ConeG Cone s 'Injective d t n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s 'Injective d t n m y
-> Either1
     (ConeG Cone s 'Projective d (Dual t) n m)
     (ConeG Cone s 'Injective d t n m)
     y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Cone s 'Injective d t n m y -> ConeG Cone s 'Injective 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG Cone s 'Injective d t n m y
c')))

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

-- lmMapCnt -


-- | contravariant mapping of 'LimesG'

lmMapCnt :: NaturalConic (Inv2 h) c s p d t n m
  => Variant2 Contravariant (Inv2 h) x y
  -> LimesG c s p d t n m x -> LimesG c s (Dual p) d (Dual t) n m y
lmMapCnt :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s (Dual p) d (Dual t) n m y
lmMapCnt (Contravariant2 Inv2 h x y
i) (LimesProjective c s 'Projective d t n m x
uc Cone s 'Projective d t n m x -> x
uf)
  = c s 'Injective d (Dual t) n m y
-> (Cone s 'Injective d (Dual t) n m y -> y)
-> LimesG c s 'Injective d (Dual t) n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Injective d t n m x
-> (Cone s 'Injective d t n m x -> x)
-> LimesG c s 'Injective d t n m x
LimesInjective c s 'Injective d (Dual t) n m y
uc' Cone s 'Injective d (Dual t) n m y -> y
uf' where
  SDualBi (Left1 (ConeG c s 'Injective d (Dual t) n m y
uc')) = Inv2 h x y
-> SDualBi (ConeG c s 'Projective d t n m) x
-> SDualBi (ConeG c s 'Projective d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 h x y
i (Either1
  (Dual1 (ConeG c s 'Projective d t n m))
  (ConeG c s 'Projective d t n m)
  x
-> SDualBi (ConeG c s 'Projective d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG c s 'Projective d t n m x
-> Either1
     (ConeG c s 'Injective d (Dual t) n m)
     (ConeG c s 'Projective d t n m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (c s 'Projective d t n m x -> ConeG c s 'Projective 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG c s 'Projective d t n m x
uc)))
  uf' :: Cone s 'Injective d (Dual t) n m y -> y
uf' Cone s 'Injective d (Dual t) n m y
c' = Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf Inv2 h x y
i (Cone s 'Projective d t n m x -> x
uf Cone s 'Projective d t n m x
c) where
    SDualBi (Right1 (ConeG Cone s 'Projective d t n m x
c)) = Inv2 h y x
-> SDualBi (ConeG Cone s 'Projective d t n m) y
-> SDualBi (ConeG Cone s 'Projective d t n m) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i) (Either1
  (Dual1 (ConeG Cone s 'Projective d t n m))
  (ConeG Cone s 'Projective d t n m)
  y
-> SDualBi (ConeG Cone s 'Projective d t n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s 'Injective d (Dual t) n m y
-> Either1
     (ConeG Cone s 'Injective d (Dual t) n m)
     (ConeG Cone s 'Projective d t n m)
     y
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (Cone s 'Injective d (Dual t) n m y
-> ConeG Cone s 'Injective d (Dual 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG Cone s 'Injective d (Dual t) n m y
c')))

lmMapCnt (Contravariant2 Inv2 h x y
i) (LimesInjective c s 'Injective d t n m x
uc Cone s 'Injective d t n m x -> x
uf)
  = c s 'Projective d (Dual t) n m y
-> (Cone s 'Projective d (Dual t) n m y -> y)
-> LimesG c s 'Projective d (Dual t) n m y
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective c s 'Projective d (Dual t) n m y
uc' Cone s 'Projective d (Dual t) n m y -> y
uf' where
  SDualBi (Left1 (ConeG c s 'Projective d (Dual t) n m y
uc')) = Inv2 h x y
-> SDualBi (ConeG c s 'Injective d t n m) x
-> SDualBi (ConeG c s 'Injective d t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 h x y
i (Either1
  (Dual1 (ConeG c s 'Injective d t n m))
  (ConeG c s 'Injective d t n m)
  x
-> SDualBi (ConeG c s 'Injective d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG c s 'Injective d t n m x
-> Either1
     (ConeG c s 'Projective d (Dual t) n m)
     (ConeG c s 'Injective d t n m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (c s 'Injective d t n m x -> ConeG c s 'Injective 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG c s 'Injective d t n m x
uc)))
  uf' :: Cone s 'Projective d (Dual t) n m y -> y
uf' Cone s 'Projective d (Dual t) n m y
c' = Inv2 h x y -> x -> y
forall (h :: * -> * -> *) x y. Functorial h => h x y -> x -> y
amapf Inv2 h x y
i (Cone s 'Injective d t n m x -> x
uf Cone s 'Injective d t n m x
c) where
    SDualBi (Right1 (ConeG Cone s 'Injective d t n m x
c)) = Inv2 h y x
-> SDualBi (ConeG Cone s 'Injective d t n m) y
-> SDualBi (ConeG Cone s 'Injective d t n m) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (Inv2 h x y -> Inv2 h y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 h x y
i) (Either1
  (Dual1 (ConeG Cone s 'Injective d t n m))
  (ConeG Cone s 'Injective d t n m)
  y
-> SDualBi (ConeG Cone s 'Injective d t n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s 'Projective d (Dual t) n m y
-> Either1
     (ConeG Cone s 'Projective d (Dual t) n m)
     (ConeG Cone s 'Injective d t n m)
     y
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (Cone s 'Projective d (Dual t) n m y
-> ConeG Cone s 'Projective d (Dual 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG Cone s 'Projective d (Dual t) n m y
c')))


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

-- lmMapS -


-- | mapping of 'LimesG'

lmMapS :: NaturalConicBi (Inv2 h) c s p d t n m
  => Inv2 h x y -> SDualBi (LimesG c s p d t n m) x -> SDualBi (LimesG c s p d t n m) y
lmMapS :: forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Inv2 h x y
-> SDualBi (LimesG c s p d t n m) x
-> SDualBi (LimesG c s p d t n m) y
lmMapS = (Variant2 'Covariant (Inv2 h) x y
 -> LimesG c s p d t n m x -> LimesG c s p d t n m y)
-> (Variant2 'Covariant (Inv2 h) x y
    -> Dual1 (LimesG c s p d t n m) x
    -> Dual1 (LimesG c s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> LimesG c s p d t n m x -> Dual1 (LimesG c s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> Dual1 (LimesG c s p d t n m) x -> LimesG c s p d t n m y)
-> Inv2 h x y
-> SDualBi (LimesG c s p d t n m) x
-> SDualBi (LimesG c 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 (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s p d t n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s p d t n m y
lmMapCov Variant2 'Covariant (Inv2 h) x y
-> Dual1 (LimesG c s p d t n m) x -> Dual1 (LimesG c s p d t n m) y
Variant2 'Covariant (Inv2 h) x y
-> LimesG c s (Dual p) d (Dual t) n m x
-> LimesG c s (Dual p) d (Dual t) n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s p d t n m y
lmMapCov Variant2 'Contravariant (Inv2 h) x y
-> LimesG c s p d t n m x -> Dual1 (LimesG c s p d t n m) y
Variant2 'Contravariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s (Dual p) d (Dual t) n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s (Dual p) d (Dual t) n m y
lmMapCnt Variant2 'Contravariant (Inv2 h) x y
-> Dual1 (LimesG c s p d t n m) x -> LimesG c s p d t n m y
Variant2 'Contravariant (Inv2 h) x y
-> LimesG c s (Dual p) d (Dual t) n m x
-> LimesG c s (Dual (Dual p)) d (Dual (Dual t)) n m y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConic (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> LimesG c s p d t n m x -> LimesG c s (Dual p) d (Dual t) n m y
lmMapCnt

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

-- FunctorialG -


instance NaturalConicBi (Inv2 h) c s p d t n m
  => ApplicativeG (SDualBi (LimesG c s p d t n m)) (Inv2 h) (->) where
  amapG :: forall x y.
Inv2 h x y
-> SDualBi (LimesG c s p d t n m) x
   -> SDualBi (LimesG c s p d t n m) y
amapG = Inv2 h x y
-> SDualBi (LimesG c s p d t n m) x
-> SDualBi (LimesG c s p d t n m) y
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Inv2 h x y
-> SDualBi (LimesG c s p d t n m) x
-> SDualBi (LimesG c s p d t n m) y
lmMapS

instance NaturalConicBi (Inv2 h) c s p d t n m
  => FunctorialG (SDualBi (LimesG c s p d t n m)) (Inv2 h) (->)