{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Category.Dualisable

-- Description : generalized duality for categories.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- generalized duality for categories.

module OAlg.Category.Dualisable
  (
    -- * Dualisable

    DualisableG(..), DualityG(..)
  , DualisableGId, DualisableGPnt
  
  , ReflexiveG(..), reflG'
  , toDualG'
  , tauO

  
    -- * Dualisable Pairing

  , DualisableGPair(..), DualisableGBi

    -- * Proposition

  , prpDualisableG

  ) where

import Data.Kind

import OAlg.Category.Definition
import OAlg.Data.Identity

import OAlg.Data.Dualisable
import OAlg.Data.EqualExtensional
import OAlg.Data.Statement.Definition

import OAlg.Structure.Definition
import OAlg.Structure.Oriented
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented

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

-- tauO -


-- | propagating the @__s__@ structure to @__o__@.

tauO :: Transformable1 o s => Struct s x -> Struct s (o x)
tauO :: forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO = Struct s x -> Struct s (o x)
forall x. Struct s x -> Struct s (o x)
forall (t :: * -> *) u v x.
TransformableG t u v =>
Struct u x -> Struct v (t x)
tauG

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

-- ReflexiveG -


-- | category @__c__@ equipped with a reflection on a subset of @'ObjectClass' __c__@ given by @__r__@.

class (Category c, Transformable r (ObjectClass c)) => ReflexiveG r c o d where
  reflG :: Struct r x -> Inv2 c (d x) (d (o (o x)))

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

-- DualisableG -


-- | category @__c__@ equipped with a duality via a reflection.

--

-- __Property__ Let @'DualisableG' __r c o d__@, then for all @__x__@ and @r@ in @'Struct' __r x__@

-- holds:

--

-- (1) @'toDualG'' q r' '.' 'toDualG'' q r '.=.' u@.

--

-- (2) @'toDualG'' q r '.' v '.=.' v' . 'toDualG'' q r''@.

--

-- (3) @'fromDualG'' q r '.=.' v '.' 'toDualG'' q r'@.

--

-- where @q@ is any proxy in @__q c o d__@, @r' = 'tau1' r@ , @r'' = 'tau1' r'@,

-- @'Inv2' u v = 'reflG'' q r@ and @'Inv2' _ v' = 'reflG'' q r'@.

--

-- __Note__ The properties above imply that @'toDualG' r@ and @'fromDualG' r@ are inverse

-- in @__c__@ for all @__x__@ and @r@ in @'Struct' __r x__@ and hence establish a duality

-- within @__r__@ structured types.

class (ReflexiveG r c o d, Transformable1 o r) => DualisableG r c o d where
  toDualG :: Struct r x -> c (d x) (d (o x))
  fromDualG :: Struct r x -> c (d (o x)) (d x)
  fromDualG Struct r x
r = c (d (o (o x))) (d x)
v c (d (o (o x))) (d x)
-> c (d (o x)) (d (o (o x))) -> c (d (o x)) (d x)
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct r (o x) -> c (d (o x)) (d (o (o x)))
forall x. Struct r x -> c (d x) (d (o x))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
DualisableG r c o d =>
Struct r x -> c (d x) (d (o x))
toDualG (Struct r x -> Struct r (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tau1 Struct r x
r) where Inv2 c (d x) (d (o (o x)))
_ c (d (o (o x))) (d x)
v = Struct r x -> Inv2 c (d x) (d (o (o x)))
forall x. Struct r x -> Inv2 c (d x) (d (o (o x)))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
ReflexiveG r c o d =>
Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG Struct r x
r

-- | helper class to avoid undecidable instances.

class DualisableG r (->) o Id => DualisableGId r o

-- | helper class to avoid undecidable instances.

class DualisableG r (->) o Pnt => DualisableGPnt r o

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

-- DualityG -


-- | attest of being 'DualisableG'.

data DualityG r c o d where DualityG :: DualisableG r c o d => DualityG r c o d

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

-- reflG' -


-- | prefixing a proxy.

reflG' :: ReflexiveG r c o d => q c o d -> Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG' :: forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
ReflexiveG r c o d =>
q c o d -> Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG' q c o d
_ = Struct r x -> Inv2 c (d x) (d (o (o x)))
forall x. Struct r x -> Inv2 c (d x) (d (o (o x)))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
ReflexiveG r c o d =>
Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG

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

-- toDualG' -


-- | prefixing a proxy.

toDualG' :: DualisableG r c o d => q c o d -> Struct r x -> c (d x) (d (o x))
toDualG' :: forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d x) (d (o x))
toDualG' q c o d
_ = Struct r x -> c (d x) (d (o x))
forall x. Struct r x -> c (d x) (d (o x))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
DualisableG r c o d =>
Struct r x -> c (d x) (d (o x))
toDualG

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

-- fromDualG' -


-- | prefixing a proxy.

fromDualG' :: DualisableG r c o d => q c o d -> Struct r x -> c (d (o x)) (d x)
fromDualG' :: forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d (o x)) (d x)
fromDualG' q c o d
_ = Struct r x -> c (d (o x)) (d x)
forall x. Struct r x -> c (d (o x)) (d x)
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
DualisableG r c o d =>
Struct r x -> c (d (o x)) (d x)
fromDualG

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

-- prpDualisableG -


-- | validity according to 'DualisableG'.

prpDualisableG :: (DualisableG r c o d, EqExt c)
  => q c o d -> Struct r x -> Statement
prpDualisableG :: forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
(DualisableG r c o d, EqExt c) =>
q c o d -> Struct r x -> Statement
prpDualisableG q c o d
q Struct r x
r = String -> Label
Prp String
"DualisableG" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (q c o d -> Struct r (o x) -> c (d (o x)) (d (o (o x)))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d x) (d (o x))
toDualG' q c o d
q Struct r (o x)
r' c (d (o x)) (d (o (o x)))
-> c (d x) (d (o x)) -> c (d x) (d (o (o x)))
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. q c o d -> Struct r x -> c (d x) (d (o x))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d x) (d (o x))
toDualG' q c o d
q Struct r x
r c (d x) (d (o (o x))) -> c (d x) (d (o (o x))) -> Statement
forall x y. c x y -> c x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. c (d x) (d (o (o x)))
u)
      , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (q c o d -> Struct r x -> c (d x) (d (o x))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d x) (d (o x))
toDualG' q c o d
q Struct r x
r c (d x) (d (o x))
-> c (d (o (o x))) (d x) -> c (d (o (o x))) (d (o x))
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c (d (o (o x))) (d x)
v c (d (o (o x))) (d (o x)) -> c (d (o (o x))) (d (o x)) -> Statement
forall x y. c x y -> c x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. c (d (o (o (o x)))) (d (o x))
v' c (d (o (o (o x)))) (d (o x))
-> c (d (o (o x))) (d (o (o (o x)))) -> c (d (o (o x))) (d (o x))
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. q c o d -> Struct r (o (o x)) -> c (d (o (o x))) (d (o (o (o x))))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d x) (d (o x))
toDualG' q c o d
q Struct r (o (o x))
r'')
      , String -> Label
Label String
"3" Label -> Statement -> Statement
:<=>: (q c o d -> Struct r x -> c (d (o x)) (d x)
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d (o x)) (d x)
fromDualG' q c o d
q Struct r x
r c (d (o x)) (d x) -> c (d (o x)) (d x) -> Statement
forall x y. c x y -> c x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. c (d (o (o x))) (d x)
v c (d (o (o x))) (d x)
-> c (d (o x)) (d (o (o x))) -> c (d (o x)) (d x)
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. q c o d -> Struct r (o x) -> c (d (o x)) (d (o (o x)))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d x) (d (o x))
toDualG' q c o d
q Struct r (o x)
r')
      ]
  where r' :: Struct r (o x)
r'        = Struct r x -> Struct r (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tau1 Struct r x
r
        r'' :: Struct r (o (o x))
r''       = Struct r (o x) -> Struct r (o (o x))
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tau1 Struct r (o x)
r' 
        Inv2 c (d x) (d (o (o x)))
u c (d (o (o x))) (d x)
v  = q c o d -> Struct r x -> Inv2 c (d x) (d (o (o x)))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
ReflexiveG r c o d =>
q c o d -> Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG' q c o d
q Struct r x
r
        Inv2 c (d (o x)) (d (o (o (o x))))
_ c (d (o (o (o x)))) (d (o x))
v' = q c o d -> Struct r (o x) -> Inv2 c (d (o x)) (d (o (o (o x))))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
ReflexiveG r c o d =>
q c o d -> Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG' q c o d
q Struct r (o x)
r'

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

-- DualisableGPair -


-- | category @__c__@ equipped with a duality pairing between @__a__@ and @__b__@ via reflections.

class (ReflexiveG r c o a, ReflexiveG r c o b, Transformable1 o r)
  => DualisableGPair r c o a b where
  toDualGLft :: Struct r x -> c (a x) (b (o x))
  toDualGRgt :: Struct r x -> c (b x) (a (o x))

  fromDualGLft :: Struct r x -> c (b (o x)) (a x)
  fromDualGLft Struct r x
r = c (a (o (o x))) (a x)
v c (a (o (o x))) (a x)
-> c (b (o x)) (a (o (o x))) -> c (b (o x)) (a x)
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct r (o x) -> c (b (o x)) (a (o (o x)))
forall x. Struct r x -> c (b x) (a (o x))
forall r (c :: * -> * -> *) (o :: * -> *) (a :: * -> *)
       (b :: * -> *) x.
DualisableGPair r c o a b =>
Struct r x -> c (b x) (a (o x))
toDualGRgt (Struct r x -> Struct r (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tau1 Struct r x
r) where Inv2 c (a x) (a (o (o x)))
_ c (a (o (o x))) (a x)
v = Struct r x -> Inv2 c (a x) (a (o (o x)))
forall x. Struct r x -> Inv2 c (a x) (a (o (o x)))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
ReflexiveG r c o d =>
Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG Struct r x
r
  
  fromDualGRgt :: Struct r x -> c (a (o x)) (b x)
  fromDualGRgt Struct r x
r = c (b (o (o x))) (b x)
v c (b (o (o x))) (b x)
-> c (a (o x)) (b (o (o x))) -> c (a (o x)) (b x)
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct r (o x) -> c (a (o x)) (b (o (o x)))
forall x. Struct r x -> c (a x) (b (o x))
forall r (c :: * -> * -> *) (o :: * -> *) (a :: * -> *)
       (b :: * -> *) x.
DualisableGPair r c o a b =>
Struct r x -> c (a x) (b (o x))
toDualGLft (Struct r x -> Struct r (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tau1 Struct r x
r) where Inv2 c (b x) (b (o (o x)))
_ c (b (o (o x))) (b x)
v = Struct r x -> Inv2 c (b x) (b (o (o x)))
forall x. Struct r x -> Inv2 c (b x) (b (o (o x)))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
ReflexiveG r c o d =>
Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG Struct r x
r

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

-- DualisableGBi -


-- | category @__c__@ equipped with a duality pairing between @__d__@ and its dual @'Dual1' __d__@

-- via reflections.

class DualisableGPair r c o d (Dual1 d) => DualisableGBi r c o d

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

-- Op - DualisableG - Id -


instance Transformable r Type => ReflexiveG r (->) Op Id where
  reflG :: forall x. Struct r x -> Inv2 (->) (Id x) (Id (Op (Op x)))
reflG Struct r x
_ = (Id x -> Id (Op (Op x)))
-> (Id (Op (Op x)) -> Id x) -> Inv2 (->) (Id x) (Id (Op (Op x)))
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 ((x -> Op (Op x)) -> Id x -> Id (Op (Op x))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Op x -> Op (Op x)
forall x. x -> Op x
Op (Op x -> Op (Op x)) -> (x -> Op x) -> x -> Op (Op x)
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
. x -> Op x
forall x. x -> Op x
Op)) ((Op (Op x) -> x) -> Id (Op (Op x)) -> Id x
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (Op x -> x
forall x. Op x -> x
fromOp (Op x -> x) -> (Op (Op x) -> Op x) -> Op (Op x) -> x
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
. Op (Op x) -> Op x
forall x. Op x -> x
fromOp))

instance (Transformable r Type, TransformableOp r) => DualisableG r (->) Op Id where
  toDualG :: forall x. Struct r x -> Id x -> Id (Op x)
toDualG Struct r x
_   = (x -> Op x) -> Id x -> Id (Op x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> Op x
forall x. x -> Op x
Op
  fromDualG :: forall x. Struct r x -> Id (Op x) -> Id x
fromDualG Struct r x
_ = (Op x -> x) -> Id (Op x) -> Id x
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Op x -> x
forall x. Op x -> x
fromOp

instance (TransformableType r, TransformableOp r) => DualisableGId r Op

instance ReflexiveG OrtX EqualExtOrt Op Id where
  reflG :: forall x. Struct OrtX x -> Inv2 EqualExtOrt (Id x) (Id (Op (Op x)))
reflG r :: Struct OrtX x
r@Struct OrtX x
Struct = EqualExtOrt (Id x) (Id (Op (Op x)))
-> EqualExtOrt (Id (Op (Op x))) (Id x)
-> Inv2 EqualExtOrt (Id x) (Id (Op (Op x)))
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 ((Id x -> Id (Op (Op x))) -> EqualExtOrt (Id x) (Id (Op (Op x)))
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub Id x -> Id (Op (Op x))
u) ((Id (Op (Op x)) -> Id x) -> EqualExtOrt (Id (Op (Op x))) (Id x)
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub Id (Op (Op x)) -> Id x
v) where Inv2 Id x -> Id (Op (Op x))
u Id (Op (Op x)) -> Id x
v = Struct OrtX x -> Inv2 (->) (Id x) (Id (Op (Op x)))
forall x. Struct OrtX x -> Inv2 (->) (Id x) (Id (Op (Op x)))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
ReflexiveG r c o d =>
Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG Struct OrtX x
r

instance DualisableG OrtX EqualExtOrt Op Id where
  toDualG :: forall x. Struct OrtX x -> EqualExtOrt (Id x) (Id (Op x))
toDualG r :: Struct OrtX x
r@Struct OrtX x
Struct = (Id x -> Id (Op x)) -> Sub EqEOrt (->) (Id x) (Id (Op x))
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub Id x -> Id (Op x)
t where t :: Id x -> Id (Op x)
t = Struct OrtX x -> Id x -> Id (Op x)
forall x. Struct OrtX x -> Id x -> Id (Op x)
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
DualisableG r c o d =>
Struct r x -> c (d x) (d (o x))
toDualG Struct OrtX x
r

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

-- Op - DualisableG - Pnt -


instance Transformable r Type => ReflexiveG r (->) Op Pnt where
  reflG :: forall x. Struct r x -> Inv2 (->) (Pnt x) (Pnt (Op (Op x)))
reflG Struct r x
_ = (Pnt x -> Pnt (Op (Op x)))
-> (Pnt (Op (Op x)) -> Pnt x)
-> Inv2 (->) (Pnt x) (Pnt (Op (Op x)))
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 Pnt x -> Pnt (Op (Op x))
forall x y. (Point x ~ Point y) => Pnt x -> Pnt y
idPnt Pnt (Op (Op x)) -> Pnt x
forall x y. (Point x ~ Point y) => Pnt x -> Pnt y
idPnt where
    
instance (Transformable r Type, TransformableOp r) => DualisableG r (->) Op Pnt where
  toDualG :: forall x. Struct r x -> Pnt x -> Pnt (Op x)
toDualG Struct r x
_   = Pnt x -> Pnt (Op x)
forall x y. (Point x ~ Point y) => Pnt x -> Pnt y
idPnt
  fromDualG :: forall x. Struct r x -> Pnt (Op x) -> Pnt x
fromDualG Struct r x
_ = Pnt (Op x) -> Pnt x
forall x y. (Point x ~ Point y) => Pnt x -> Pnt y
idPnt

instance (TransformableType r, TransformableOp r) => DualisableGPnt r Op

instance ReflexiveG OrtX EqualExtOrt Op Pnt where
  reflG :: forall x.
Struct OrtX x -> Inv2 EqualExtOrt (Pnt x) (Pnt (Op (Op x)))
reflG r :: Struct OrtX x
r@Struct OrtX x
Struct = EqualExtOrt (Pnt x) (Pnt (Op (Op x)))
-> EqualExtOrt (Pnt (Op (Op x))) (Pnt x)
-> Inv2 EqualExtOrt (Pnt x) (Pnt (Op (Op x)))
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 ((Pnt x -> Pnt (Op (Op x))) -> EqualExtOrt (Pnt x) (Pnt (Op (Op x)))
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub Pnt x -> Pnt (Op (Op x))
u) ((Pnt (Op (Op x)) -> Pnt x) -> EqualExtOrt (Pnt (Op (Op x))) (Pnt x)
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub Pnt (Op (Op x)) -> Pnt x
v) where Inv2 Pnt x -> Pnt (Op (Op x))
u Pnt (Op (Op x)) -> Pnt x
v = Struct OrtX x -> Inv2 (->) (Pnt x) (Pnt (Op (Op x)))
forall x. Struct OrtX x -> Inv2 (->) (Pnt x) (Pnt (Op (Op x)))
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
ReflexiveG r c o d =>
Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG Struct OrtX x
r

instance DualisableG OrtX EqualExtOrt Op Pnt where
  toDualG :: forall x. Struct OrtX x -> EqualExtOrt (Pnt x) (Pnt (Op x))
toDualG r :: Struct OrtX x
r@Struct OrtX x
Struct = (Pnt x -> Pnt (Op x)) -> Sub EqEOrt (->) (Pnt x) (Pnt (Op x))
forall s x y (c :: * -> * -> *).
(Structure s x, Structure s y) =>
c x y -> Sub s c x y
Sub Pnt x -> Pnt (Op x)
t where t :: Pnt x -> Pnt (Op x)
t = Struct OrtX x -> Pnt x -> Pnt (Op x)
forall x. Struct OrtX x -> Pnt x -> Pnt (Op x)
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
DualisableG r c o d =>
Struct r x -> c (d x) (d (o x))
toDualG Struct OrtX x
r 

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

-- toDualRtOp -


-- | the dual root for on 'FibredOriented'-structures.

toDualRtOp :: Struct FbrOrt x -> Rt x -> Rt (Op x)
toDualRtOp :: forall x. Struct FbrOrt x -> Rt x -> Rt (Op x)
toDualRtOp Struct FbrOrt x
Struct (Rt Root x
r) = Root (Op x) -> Rt (Op x)
forall x. Root x -> Rt x
Rt (Orientation (Point x) -> Orientation (Point x)
forall p. Orientation p -> Orientation p
opposite Orientation (Point x)
Root x
r)

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

-- Op - DualisableG - Rt -


instance Transformable r Type => ReflexiveG r (->) Op Rt where
  reflG :: forall x. Struct r x -> Inv2 (->) (Rt x) (Rt (Op (Op x)))
reflG Struct r x
_ = (Rt x -> Rt (Op (Op x)))
-> (Rt (Op (Op x)) -> Rt x) -> Inv2 (->) (Rt x) (Rt (Op (Op x)))
forall (c :: * -> * -> *) x y. c x y -> c y x -> Inv2 c x y
Inv2 Rt x -> Rt (Op (Op x))
forall x y. (Root x ~ Root y) => Rt x -> Rt y
idRt Rt (Op (Op x)) -> Rt x
forall x y. (Root x ~ Root y) => Rt x -> Rt y
idRt

instance (Transformable r Type, TransformableOp r, Transformable r FbrOrt)
  => DualisableG r (->) Op Rt where
  toDualG :: forall x. Struct r x -> Rt x -> Rt (Op x)
toDualG Struct r x
s = Struct FbrOrt x -> Rt x -> Rt (Op x)
forall x. Struct FbrOrt x -> Rt x -> Rt (Op x)
toDualRtOp (Struct r x -> Struct FbrOrt x
forall x. Struct r x -> Struct FbrOrt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct r x
s)