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

{-# LANGUAGE NoImplicitPrelude #-}

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

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


-- |

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

-- Description : duality for conic objects.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- duality for conic objects.

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

    NaturalConicBi

    -- * Map

  , sdbToCncObj, sdbFromCncObj
    
  ) where

import OAlg.Prelude

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

import OAlg.Data.Either

import OAlg.Entity.Diagram

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

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

import OAlg.Limes.Cone.Definition

import OAlg.Limes.Cone.Conic.Core

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

-- sdbToCncObj -


-- | canonical mapping to its underlying conic object.

sdbToCncObj ::
  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 :: 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 (SDualBi (Right1 (ConeG c s p d t n m x
c))) = Either1 (Dual1 (c s p d t n m)) (c s p d t n m) x
-> SDualBi (c s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (c s p d t n m x
-> Either1 (c s (Dual p) d (Dual t) n m) (c s p d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 c s p d t n m x
c)
sdbToCncObj (SDualBi (Left1 (ConeG c s (Dual p) d (Dual t) n m x
c'))) = Either1 (Dual1 (c s p d t n m)) (c s p d t n m) x
-> SDualBi (c s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (c s (Dual p) d (Dual t) n m x
-> Either1 (c s (Dual p) d (Dual t) n m) (c s p d t n m) x
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 c s (Dual p) d (Dual t) n m x
c')

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

-- sdbFromCncObj -


-- | canonical mapping from its underlying conic object.

sdbFromCncObj :: 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 :: 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 (Right1 c s p d t n m x
c)) = Either1 (Dual1 (ConeG c s p d t n m)) (ConeG c s p d t n m) x
-> SDualBi (ConeG c s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG c s p d t n m x
-> Either1
     (ConeG c s (Dual p) d (Dual t) n m) (ConeG c s p d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (c s p d t n m x -> ConeG c 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG c s p d t n m x
c))
sdbFromCncObj (SDualBi (Left1 Dual1 (c s p d t n m) x
c')) = Either1 (Dual1 (ConeG c s p d t n m)) (ConeG c s p d t n m) x
-> SDualBi (ConeG c s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG c s (Dual p) d (Dual t) n m x
-> Either1
     (ConeG c s (Dual p) d (Dual t) n m) (ConeG c s p d t n m) x
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (c s (Dual p) d (Dual t) n m x
-> ConeG c s (Dual p) d (Dual 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 (Dual p) d (Dual t) n m x
Dual1 (c s p d t n m) x
c'))

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

-- Cone - Mlt -


instance
  ( HomMultiplicativeDisjunctive h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  )
  => ApplicativeG (SDualBi (ConeG Cone Mlt p d t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (ConeG Cone Mlt p d t n m) x
   -> SDualBi (ConeG Cone Mlt p d t n m) y
amapG h x y
h = SDualBi (Cone Mlt p d t n m) y
-> SDualBi (ConeG Cone Mlt 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 (Cone Mlt p d t n m) y
 -> SDualBi (ConeG Cone Mlt p d t n m) y)
-> (SDualBi (ConeG Cone Mlt p d t n m) x
    -> SDualBi (Cone Mlt p d t n m) y)
-> SDualBi (ConeG Cone Mlt p d t n m) x
-> SDualBi (ConeG Cone Mlt 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 (Cone Mlt p d t n m) x -> SDualBi (Cone Mlt p d t n m) y
forall x y.
h x y
-> SDualBi (Cone Mlt p d t n m) x -> SDualBi (Cone Mlt 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 (Cone Mlt p d t n m) x -> SDualBi (Cone Mlt p d t n m) y)
-> (SDualBi (ConeG Cone Mlt p d t n m) x
    -> SDualBi (Cone Mlt p d t n m) x)
-> SDualBi (ConeG Cone Mlt p d t n m) x
-> SDualBi (Cone Mlt 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 Cone Mlt p d t n m) x
-> SDualBi (Cone Mlt 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
  ( HomMultiplicativeDisjunctive h
  , FunctorialOriented h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (ConeG Cone Mlt p d t n m)) h (->)

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

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

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

-- Cone - Dst -


instance
  ( HomDistributiveDisjunctive h
  , NaturalDiagrammaticBi h d t n m
  , p ~ Dual (Dual p), t ~ Dual (Dual t)
  )
  => ApplicativeG (SDualBi (ConeG Cone Dst p d t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (ConeG Cone Dst p d t n m) x
   -> SDualBi (ConeG Cone Dst p d t n m) y
amapG h x y
h = SDualBi (Cone Dst p d t n m) y
-> SDualBi (ConeG Cone Dst 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 (Cone Dst p d t n m) y
 -> SDualBi (ConeG Cone Dst p d t n m) y)
-> (SDualBi (ConeG Cone Dst p d t n m) x
    -> SDualBi (Cone Dst p d t n m) y)
-> SDualBi (ConeG Cone Dst p d t n m) x
-> SDualBi (ConeG Cone Dst 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 (Cone Dst p d t n m) x -> SDualBi (Cone Dst p d t n m) y
forall x y.
h x y
-> SDualBi (Cone Dst p d t n m) x -> SDualBi (Cone Dst 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 (Cone Dst p d t n m) x -> SDualBi (Cone Dst p d t n m) y)
-> (SDualBi (ConeG Cone Dst p d t n m) x
    -> SDualBi (Cone Dst p d t n m) x)
-> SDualBi (ConeG Cone Dst p d t n m) x
-> SDualBi (Cone Dst 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 Cone Dst p d t n m) x
-> SDualBi (Cone Dst 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), t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (ConeG Cone Dst 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 Cone Dst p d t n m)) (SDualBi (ConeG Cone Dst p d t n m))

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

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

-- NaturalConicBi -


-- | natrual conic for @__p__@, @__t__@ and also @'Dual' __p__@, @'Dual' __t__@.

type NaturalConicBi h c s p d t n m =
  ( NaturalConic h c s p d t n m
  , NaturalConic h c s (Dual p) d (Dual t) n m
  )