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

{-# LANGUAGE NoImplicitPrelude #-}

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

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


-- |

-- Module      : OAlg.Limes.Limits.Duality

-- Description : duality for limits.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- duality for 'LimitsG'.

module OAlg.Limes.Limits.Duality
  (
    -- * Mapp

    lmsMapS, lmsMapCov, lmsMapCnt
  ) where

import OAlg.Prelude

import OAlg.Category.SDuality

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

import OAlg.Entity.Diagram

import OAlg.Limes.Cone

import OAlg.Limes.Limits.Core

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

-- LimitsG - Dual -


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

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

-- lmsMapCov -


-- | covariant mapping for 'LimitsG'.

lmsMapCov :: NaturalConicBi (Inv2 h) c s p d t n m
  => Variant2 Covariant (Inv2 h) x y
  -> LimitsG c s p d t n m x -> LimitsG c s p d t n m y
lmsMapCov :: 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 =>
Variant2 'Covariant (Inv2 h) x y
-> LimitsG c s p d t n m x -> LimitsG c s p d t n m y
lmsMapCov (Covariant2 Inv2 h x y
i) (LimitsG d t n m x -> LimesG c s p d t n m x
u) = (d t n m y -> LimesG c s p d t n m y) -> LimitsG c 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.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG d t n m y -> LimesG c s p d t n m y
u' where
  u' :: d t n m y -> LimesG c s p d t n m y
u' d t n m y
d' = LimesG c s p d t n m y
l where
    SDualBi (Right1 LimesG c s p d t n m y
l)            = 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 (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 (LimesG c s p d t n m)) (LimesG c s p d t n m) x
-> SDualBi (LimesG c s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s p d t n m x
-> Either1
     (LimesG c s (Dual p) d (Dual t) n m) (LimesG c s p d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d t n m x -> LimesG c s p d t n m x
u d t n m x
d)))
    SDualBi (Right1 (DiagramG d t n m x
d)) = Inv2 h y x
-> SDualBi (DiagramG d t n m) y -> SDualBi (DiagramG 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 (DiagramG d t n m)) (DiagramG d t n m) y
-> SDualBi (DiagramG d t n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d t n m y
-> Either1 (DiagramG d (Dual t) n m) (DiagramG d t n m) y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d t n m y -> DiagramG d t n m y
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 y
d')))

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

-- lmsMapCnt -


-- | contravariant mapping for 'LimitsG'.

lmsMapCnt :: NaturalConicBi (Inv2 h) c s p d t n m
  => Variant2 Contravariant (Inv2 h) x y
  -> LimitsG c s p d t n m x -> Dual1 (LimitsG c s p d t n m) y
lmsMapCnt :: 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 =>
Variant2 'Contravariant (Inv2 h) x y
-> LimitsG c s p d t n m x -> Dual1 (LimitsG c s p d t n m) y
lmsMapCnt (Contravariant2 Inv2 h x y
i) (LimitsG d t n m x -> LimesG c s p d t n m x
u) = (d (Dual t) n m y -> LimesG c s (Dual p) d (Dual t) n m y)
-> LimitsG c s (Dual p) 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.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG d (Dual t) n m y -> Dual1 (LimesG c s p d t n m) y
d (Dual t) n m y -> LimesG c s (Dual p) d (Dual t) n m y
u' where
  u' :: d (Dual t) n m y -> Dual1 (LimesG c s p d t n m) y
u' d (Dual t) n m y
d' = Dual1 (LimesG c s p d t n m) y
l where
    SDualBi (Left1 Dual1 (LimesG c s p d t n m) y
l)            = 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 (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 (LimesG c s p d t n m)) (LimesG c s p d t n m) x
-> SDualBi (LimesG c s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c s p d t n m x
-> Either1
     (LimesG c s (Dual p) d (Dual t) n m) (LimesG c s p d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d t n m x -> LimesG c s p d t n m x
u d t n m x
d)))
    SDualBi (Left1 (DiagramG d t n m x
d)) = Inv2 h y x
-> SDualBi (DiagramG d (Dual t) n m) y
-> SDualBi (DiagramG d (Dual 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 (DiagramG d (Dual t) n m)) (DiagramG d (Dual t) n m) y
-> SDualBi (DiagramG d (Dual t) n m) y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d (Dual t) n m y
-> Either1
     (DiagramG d (Dual (Dual t)) n m) (DiagramG d (Dual t) n m) y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d (Dual t) n m y -> DiagramG d (Dual t) n m y
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 (Dual t) n m y
d')))

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

-- lmsMapS -


-- | mapping for 'LimitsG'.

lmsMapS :: NaturalConicBi (Inv2 h) c s p d t n m
  => Inv2 h x y -> SDualBi (LimitsG c s p d t n m) x -> SDualBi (LimitsG c s p d t n m) y
lmsMapS :: 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 (LimitsG c s p d t n m) x
-> SDualBi (LimitsG c s p d t n m) y
lmsMapS = (Variant2 'Covariant (Inv2 h) x y
 -> LimitsG c s p d t n m x -> LimitsG c s p d t n m y)
-> (Variant2 'Covariant (Inv2 h) x y
    -> Dual1 (LimitsG c s p d t n m) x
    -> Dual1 (LimitsG c s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> LimitsG c s p d t n m x -> Dual1 (LimitsG c s p d t n m) y)
-> (Variant2 'Contravariant (Inv2 h) x y
    -> Dual1 (LimitsG c s p d t n m) x -> LimitsG c s p d t n m y)
-> Inv2 h x y
-> SDualBi (LimitsG c s p d t n m) x
-> SDualBi (LimitsG 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
-> LimitsG c s p d t n m x -> LimitsG 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 =>
Variant2 'Covariant (Inv2 h) x y
-> LimitsG c s p d t n m x -> LimitsG c s p d t n m y
lmsMapCov Variant2 'Covariant (Inv2 h) x y
-> Dual1 (LimitsG c s p d t n m) x
-> Dual1 (LimitsG c s p d t n m) y
Variant2 'Covariant (Inv2 h) x y
-> LimitsG c s (Dual p) d (Dual t) n m x
-> LimitsG 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.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Covariant (Inv2 h) x y
-> LimitsG c s p d t n m x -> LimitsG c s p d t n m y
lmsMapCov Variant2 'Contravariant (Inv2 h) x y
-> LimitsG c s p d t n m x -> Dual1 (LimitsG 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 =>
Variant2 'Contravariant (Inv2 h) x y
-> LimitsG c s p d t n m x -> Dual1 (LimitsG c s p d t n m) y
lmsMapCnt Variant2 'Contravariant (Inv2 h) x y
-> Dual1 (LimitsG c s p d t n m) x -> LimitsG c s p d t n m y
Variant2 'Contravariant (Inv2 h) x y
-> LimitsG c s (Dual p) d (Dual t) n m x
-> Dual1 (LimitsG 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.
NaturalConicBi (Inv2 h) c s p d t n m =>
Variant2 'Contravariant (Inv2 h) x y
-> LimitsG c s p d t n m x -> Dual1 (LimitsG c s p d t n m) y
lmsMapCnt

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

-- FunctorialG -


instance NaturalConicBi (Inv2 h) c s p d t n m
  => ApplicativeG (SDualBi (LimitsG c s p d t n m)) (Inv2 h) (->) where
  amapG :: forall x y.
Inv2 h x y
-> SDualBi (LimitsG c s p d t n m) x
   -> SDualBi (LimitsG c s p d t n m) y
amapG = Inv2 h x y
-> SDualBi (LimitsG c s p d t n m) x
-> SDualBi (LimitsG 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 (LimitsG c s p d t n m) x
-> SDualBi (LimitsG c s p d t n m) y
lmsMapS

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