{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Hom.Multiplicative.Proposition
-- Description : propositions on homomorphisms between multiplicative structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on homomorphisms between 'Multiplicative' structures.
module OAlg.Hom.Multiplicative.Proposition
  (
    -- * Proposition
    prpHomOpMlt

    -- * Multiplicative
  , prpHomMlt, XHomMlt(..), coXHomMlt, coXHomMltInv
  , SomeApplPnt(..), coSomeApplPnt, coSomeApplPntInv
  , SomeApplMltp2(..), coSomeApplMltp2, coSomeApplMltp2Inv
  , prpHomMlt1, prpHomMlt2

    -- * X
  , xHomMlt, xHomMlt', xSomeApplPnt, xSomeApplMltp2
  )
  where

import Control.Monad

import OAlg.Prelude

import OAlg.Data.Symbol

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

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

--------------------------------------------------------------------------------
-- SomeApplPnt -

-- | some application on a point.
data SomeApplPnt h where
  SomeApplPnt :: h a b -> Point a -> SomeApplPnt h

--------------------------------------------------------------------------------
-- SomeApplPnt - Duality -

type instance Dual (SomeApplPnt h) = SomeApplPnt (OpHom h)

-- | to the dual of @'SomeApplPnt' __h__@ with its inverse 'coSomeApplPntInv'.
coSomeApplPnt :: Transformable1 Op (ObjectClass h) => SomeApplPnt h -> Dual (SomeApplPnt h)
coSomeApplPnt :: forall (h :: * -> * -> *).
Transformable1 Op (ObjectClass h) =>
SomeApplPnt h -> Dual (SomeApplPnt h)
coSomeApplPnt (SomeApplPnt h a b
h Point a
p) = forall (h :: * -> * -> *) a b. h a b -> Point a -> SomeApplPnt h
SomeApplPnt (forall (h :: * -> * -> *) a b.
Transformable1 Op (ObjectClass h) =>
h a b -> OpHom h (Op a) (Op b)
OpHom h a b
h) Point a
p

-- | from the dual of @'Dual' ('SomeApplPnt' __h__)@ with its inverse 'coSomeApplPnt'.
coSomeApplPntInv :: Dual (SomeApplPnt h) -> SomeApplPnt h
coSomeApplPntInv :: forall (h :: * -> * -> *). Dual (SomeApplPnt h) -> SomeApplPnt h
coSomeApplPntInv (SomeApplPnt (OpHom h x y
h) Point a
p) = forall (h :: * -> * -> *) a b. h a b -> Point a -> SomeApplPnt h
SomeApplPnt h x y
h Point a
p

--------------------------------------------------------------------------------
-- prpHomMlt1 -

relHomMlt1Homomorphous :: Hom Mlt h => Homomorphous Mlt a b -> h a b -> Point a -> Statement
relHomMlt1Homomorphous :: forall (h :: * -> * -> *) a b.
Hom Mlt h =>
Homomorphous Mlt a b -> h a b -> Point a -> Statement
relHomMlt1Homomorphous (Struct Mlt a
Struct:>:Struct Mlt b
Struct) h a b
f Point a
p
  = (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
f (forall c. Multiplicative c => Point c -> c
one Point a
p) forall a. Eq a => a -> a -> Bool
== forall c. Multiplicative c => Point c -> c
one (forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a b
f Point a
p)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"p"String -> String -> Parameter
:=forall a. Show a => a -> String
show Point a
p] 

-- | validity according to "OAlg.Hom.Multiplicative#HomMlt1".
prpHomMlt1 :: Hom Mlt h => h a b -> Point a -> Statement
prpHomMlt1 :: forall (h :: * -> * -> *) a b.
Hom Mlt h =>
h a b -> Point a -> Statement
prpHomMlt1 h a b
f Point a
p = String -> Label
Prp String
"HomMlt1"
  Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *) a b.
Hom Mlt h =>
Homomorphous Mlt a b -> h a b -> Point a -> Statement
relHomMlt1Homomorphous (forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h a b
f)) h a b
f Point a
p

--------------------------------------------------------------------------------
-- prpHomMlt2 -

relHomMlt2Homomorphous :: Hom Mlt h => Homomorphous Mlt a b -> h a b -> Mltp2 a -> Statement
relHomMlt2Homomorphous :: forall (h :: * -> * -> *) a b.
Hom Mlt h =>
Homomorphous Mlt a b -> h a b -> Mltp2 a -> Statement
relHomMlt2Homomorphous (Struct Mlt a
Struct:>:Struct Mlt b
Struct) h a b
f (Mltp2 a
x a
y)
  = (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
f (a
x forall c. Multiplicative c => c -> c -> c
* a
y) forall a. Eq a => a -> a -> Bool
== forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
f a
x forall c. Multiplicative c => c -> c -> c
* forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
f a
y)
      Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
x,String
"y"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
y]

-- | validity according to "OAlg.Hom.Multiplicative#HomMlt2".
prpHomMlt2 :: Hom Mlt h => h a b -> Mltp2 a -> Statement
prpHomMlt2 :: forall (h :: * -> * -> *) a b.
Hom Mlt h =>
h a b -> Mltp2 a -> Statement
prpHomMlt2 h a b
f Mltp2 a
m2 = String -> Label
Prp String
"HomMlt2"
  Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *) a b.
Hom Mlt h =>
Homomorphous Mlt a b -> h a b -> Mltp2 a -> Statement
relHomMlt2Homomorphous (forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h a b
f)) h a b
f Mltp2 a
m2

--------------------------------------------------------------------------------
-- SomeApplMltp2 -

-- | some application on multiplicable factors.
data SomeApplMltp2 h where
  SomeApplMltp2 :: h a b -> Mltp2 a -> SomeApplMltp2 h

--------------------------------------------------------------------------------
-- SomeApplMltp2 - Duality -

type instance Dual (SomeApplMltp2 h) = SomeApplMltp2 (OpHom h)

-- | to the dual of @'SomeApplMltp2' __h__@ with its inverse 'coSomeApplMltp2Inv'.
coSomeApplMltp2 :: HomMultiplicative h => SomeApplMltp2 h -> Dual (SomeApplMltp2 h)
coSomeApplMltp2 :: forall (h :: * -> * -> *).
HomMultiplicative h =>
SomeApplMltp2 h -> Dual (SomeApplMltp2 h)
coSomeApplMltp2 (SomeApplMltp2 h a b
h Mltp2 a
m2) = forall (h :: * -> * -> *) a b. h a b -> Mltp2 a -> SomeApplMltp2 h
SomeApplMltp2 OpHom h (Op a) (Op b)
h' Mltp2 (Op a)
m2' where
  h' :: OpHom h (Op a) (Op b)
h' = forall (h :: * -> * -> *) a b.
Transformable1 Op (ObjectClass h) =>
h a b -> OpHom h (Op a) (Op b)
OpHom h a b
h
  m2' :: Mltp2 (Op a)
m2' = forall a. Struct Ort a -> Mltp2 a -> Mltp2 (Op a)
toDualStruct (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h a b
h)) Mltp2 a
m2
  
  toDualStruct :: Struct Ort a -> Mltp2 a -> Mltp2 (Op a)
  toDualStruct :: forall a. Struct Ort a -> Mltp2 a -> Mltp2 (Op a)
toDualStruct Struct Ort a
Struct = forall x. Dualisable x => x -> Dual x
toDual

-- | from the dual of @'Dual' ('SomeApplMltp2' __h__)@ with its inverse 'coSomeApplMltp2'.
coSomeApplMltp2Inv :: HomMultiplicative h => Dual (SomeApplMltp2 h) -> SomeApplMltp2 h
coSomeApplMltp2Inv :: forall (h :: * -> * -> *).
HomMultiplicative h =>
Dual (SomeApplMltp2 h) -> SomeApplMltp2 h
coSomeApplMltp2Inv (SomeApplMltp2 (OpHom h x y
h) Mltp2 a
m2') = forall (h :: * -> * -> *) a b. h a b -> Mltp2 a -> SomeApplMltp2 h
SomeApplMltp2 h x y
h Mltp2 x
m2 where
  m2 :: Mltp2 x
m2 = forall a. Struct Ort a -> Mltp2 (Op a) -> Mltp2 a
fromDualStruct (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h x y
h)) Mltp2 a
m2'

  fromDualStruct :: Struct Ort a -> Mltp2 (Op a) -> Mltp2 a
  fromDualStruct :: forall a. Struct Ort a -> Mltp2 (Op a) -> Mltp2 a
fromDualStruct Struct Ort a
Struct = forall x. Dualisable x => Dual x -> x
fromDual

--------------------------------------------------------------------------------
-- XHomMlt -

-- | random variable for validating a type family @__h__@ according to 'HomMultiplicative'.
data XHomMlt h
  = XHomMlt (X (SomeApplPnt h)) (X (SomeApplMltp2 h))

--------------------------------------------------------------------------------
-- XHomMlt - Duality -

type instance Dual (XHomMlt h) = XHomMlt (OpHom h)

-- | to the dual of @'XHomMlt' __h__@ with its inverse 'coXHomMltInv'.
coXHomMlt :: HomMultiplicative h => XHomMlt h -> Dual (XHomMlt h)
coXHomMlt :: forall (h :: * -> * -> *).
HomMultiplicative h =>
XHomMlt h -> Dual (XHomMlt h)
coXHomMlt (XHomMlt X (SomeApplPnt h)
xsap X (SomeApplMltp2 h)
xsam2)
  = forall (h :: * -> * -> *).
X (SomeApplPnt h) -> X (SomeApplMltp2 h) -> XHomMlt h
XHomMlt (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (h :: * -> * -> *).
Transformable1 Op (ObjectClass h) =>
SomeApplPnt h -> Dual (SomeApplPnt h)
coSomeApplPnt X (SomeApplPnt h)
xsap) (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (h :: * -> * -> *).
HomMultiplicative h =>
SomeApplMltp2 h -> Dual (SomeApplMltp2 h)
coSomeApplMltp2 X (SomeApplMltp2 h)
xsam2)

-- | from the dual of @'Dual' ('XHomMlt' __h__)@ with its inverse 'coXHomMlt'.
coXHomMltInv :: HomMultiplicative h
  => Dual (XHomMlt h) -> XHomMlt h
coXHomMltInv :: forall (h :: * -> * -> *).
HomMultiplicative h =>
Dual (XHomMlt h) -> XHomMlt h
coXHomMltInv (XHomMlt X (SomeApplPnt (OpHom h))
xsap' X (SomeApplMltp2 (OpHom h))
xsam2')
  = forall (h :: * -> * -> *).
X (SomeApplPnt h) -> X (SomeApplMltp2 h) -> XHomMlt h
XHomMlt (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (h :: * -> * -> *). Dual (SomeApplPnt h) -> SomeApplPnt h
coSomeApplPntInv X (SomeApplPnt (OpHom h))
xsap') (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (h :: * -> * -> *).
HomMultiplicative h =>
Dual (SomeApplMltp2 h) -> SomeApplMltp2 h
coSomeApplMltp2Inv X (SomeApplMltp2 (OpHom h))
xsam2')

--------------------------------------------------------------------------------
-- prpHomMult -

-- | validity of homomorphisms between 'Multiplicative' structures according to
--   "OAlg.Hom.Multiplicative#HomMlt".
prpHomMlt :: Hom Mlt h => XHomMlt h -> Statement
prpHomMlt :: forall (h :: * -> * -> *). Hom Mlt h => XHomMlt h -> Statement
prpHomMlt (XHomMlt X (SomeApplPnt h)
xsap X (SomeApplMltp2 h)
xsam2) = String -> Label
Prp String
"HomMlt"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall a. X a -> (a -> Statement) -> Statement
Forall X (SomeApplPnt h)
xsap (\(SomeApplPnt h a b
f Point a
p) -> forall (h :: * -> * -> *) a b.
Hom Mlt h =>
h a b -> Point a -> Statement
prpHomMlt1 h a b
f Point a
p)
            , forall a. X a -> (a -> Statement) -> Statement
Forall X (SomeApplMltp2 h)
xsam2 (\(SomeApplMltp2 h a b
f Mltp2 a
m2) -> forall (h :: * -> * -> *) a b.
Hom Mlt h =>
h a b -> Mltp2 a -> Statement
prpHomMlt2 h a b
f Mltp2 a
m2)
            ]

--------------------------------------------------------------------------------
-- SomeApplMlt -

-- | some application on 'Oriented' 'Site'.
data SomeApplMlt d h where
  SomeApplMlt :: h a b -> XOrtSite d a -> SomeApplMlt d h

--------------------------------------------------------------------------------
-- SomeApplMlt - Dualisable -

type instance Dual (SomeApplMlt To h) = SomeApplMlt From (OpHom h)

-- | to the dual of @'SomeApplMlt' 'To' __h__@.
coSomeApplMltTo :: Transformable1 Op (ObjectClass h)
  => SomeApplMlt To h -> Dual (SomeApplMlt To h)
coSomeApplMltTo :: forall (h :: * -> * -> *).
Transformable1 Op (ObjectClass h) =>
SomeApplMlt 'To h -> Dual (SomeApplMlt 'To h)
coSomeApplMltTo (SomeApplMlt h a b
h xe :: XOrtSite 'To a
xe@(XEnd X (Point a)
_ Point a -> X a
_)) = forall (h :: * -> * -> *) a b (d :: Site).
h a b -> XOrtSite d a -> SomeApplMlt d h
SomeApplMlt OpHom h (Op a) (Op b)
h' Dual (XOrtSite 'To a)
xs' where
    h' :: OpHom h (Op a) (Op b)
h'  = forall (h :: * -> * -> *) a b.
Transformable1 Op (ObjectClass h) =>
h a b -> OpHom h (Op a) (Op b)
OpHom h a b
h
    xs' :: Dual (XOrtSite 'To a)
xs' = forall x. Dualisable x => x -> Dual x
toDual XOrtSite 'To a
xe

--------------------------------------------------------------------------------
-- xSomeApplPnt -

-- | random variable for some application on a point given by a 'SomeApplMlt'.
xSomeApplPnt :: SomeApplMlt d h -> X (SomeApplPnt h)
xSomeApplPnt :: forall (d :: Site) (h :: * -> * -> *).
SomeApplMlt d h -> X (SomeApplPnt h)
xSomeApplPnt (SomeApplMlt h a b
h (XStart X (Point a)
xp Point a -> X a
_))
  = X (Point a)
xp forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) a b. h a b -> Point a -> SomeApplPnt h
SomeApplPnt h a b
h
xSomeApplPnt (SomeApplMlt h a b
h (XEnd X (Point a)
xp Point a -> X a
_))
  = X (Point a)
xp forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) a b. h a b -> Point a -> SomeApplPnt h
SomeApplPnt h a b
h


--------------------------------------------------------------------------------
-- xSomeApplMltp2 -

-- | random variable for some application on multiplicable factors given by a 'SomeApplMlt'.
xSomeApplMltp2 :: Hom Mlt h => SomeApplMlt d h -> X (SomeApplMltp2 h)
xSomeApplMltp2 :: forall (h :: * -> * -> *) (d :: Site).
Hom Mlt h =>
SomeApplMlt d h -> X (SomeApplMltp2 h)
xSomeApplMltp2 (SomeApplMlt h a b
h xs :: XOrtSite d a
xs@(XStart X (Point a)
_ Point a -> X a
_))
  = forall a (h :: * -> * -> *) b.
XOrtSite 'From a -> Struct Mlt a -> h a b -> X (SomeApplMltp2 h)
xSam2Start XOrtSite d a
xs (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h a b
h)) h a b
h where
  
      xSam2Start :: XOrtSite From a -> Struct Mlt a
        -> h a b -> X (SomeApplMltp2 h)
      xSam2Start :: forall a (h :: * -> * -> *) b.
XOrtSite 'From a -> Struct Mlt a -> h a b -> X (SomeApplMltp2 h)
xSam2Start XOrtSite 'From a
xs Struct Mlt a
Struct h a b
h = forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp2 c)
xMltp2 XOrtSite 'From a
xs forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) a b. h a b -> Mltp2 a -> SomeApplMltp2 h
SomeApplMltp2 h a b
h
      
xSomeApplMltp2 sa :: SomeApplMlt d h
sa@(SomeApplMlt h a b
_ (XEnd X (Point a)
_ Point a -> X a
_))
  = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (h :: * -> * -> *).
HomMultiplicative h =>
Dual (SomeApplMltp2 h) -> SomeApplMltp2 h
coSomeApplMltp2Inv forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) (d :: Site).
Hom Mlt h =>
SomeApplMlt d h -> X (SomeApplMltp2 h)
xSomeApplMltp2 forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *).
Transformable1 Op (ObjectClass h) =>
SomeApplMlt 'To h -> Dual (SomeApplMlt 'To h)
coSomeApplMltTo SomeApplMlt d h
sa

--------------------------------------------------------------------------------
-- xHomMlt -

-- | the induced random variable of 'XHomMlt', given by 'SomeApplMlt'.
xHomMlt :: Hom Mlt h => SomeApplMlt d h -> XHomMlt h
xHomMlt :: forall (h :: * -> * -> *) (d :: Site).
Hom Mlt h =>
SomeApplMlt d h -> XHomMlt h
xHomMlt SomeApplMlt d h
sams = forall (h :: * -> * -> *).
X (SomeApplPnt h) -> X (SomeApplMltp2 h) -> XHomMlt h
XHomMlt X (SomeApplPnt h)
xsap X (SomeApplMltp2 h)
xsam2 where
  xsap :: X (SomeApplPnt h)
xsap  = forall (d :: Site) (h :: * -> * -> *).
SomeApplMlt d h -> X (SomeApplPnt h)
xSomeApplPnt SomeApplMlt d h
sams
  xsam2 :: X (SomeApplMltp2 h)
xsam2 = forall (h :: * -> * -> *) (d :: Site).
Hom Mlt h =>
SomeApplMlt d h -> X (SomeApplMltp2 h)
xSomeApplMltp2 SomeApplMlt d h
sams

--------------------------------------------------------------------------------
-- xHomMlt' -

-- | the induced random variable of 'XHomMlt'.
xHomMlt' :: h a b -> XMlt a -> XHomMlt h
xHomMlt' :: forall (h :: * -> * -> *) a b. h a b -> XMlt a -> XHomMlt h
xHomMlt' h a b
h (XMlt X N
_ X (Point a)
xp X a
_ X (Endo a)
_ X (Mltp2 a)
xa2 X (Mltp3 a)
_) = forall (h :: * -> * -> *).
X (SomeApplPnt h) -> X (SomeApplMltp2 h) -> XHomMlt h
XHomMlt X (SomeApplPnt h)
xsp X (SomeApplMltp2 h)
xsa2 where
  xsp :: X (SomeApplPnt h)
xsp = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall (h :: * -> * -> *) a b. h a b -> Point a -> SomeApplPnt h
SomeApplPnt h a b
h) X (Point a)
xp
  xsa2 :: X (SomeApplMltp2 h)
xsa2 = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall (h :: * -> * -> *) a b. h a b -> Mltp2 a -> SomeApplMltp2 h
SomeApplMltp2 h a b
h) X (Mltp2 a)
xa2

--------------------------------------------------------------------------------
-- prpHomOpMlt -

-- | validity of @'HomOp' 'Mlt'@ to be a family of 'Multiplicative' homomorphisms.
prpHomOpMlt :: Statement
prpHomOpMlt :: Statement
prpHomOpMlt = String -> Label
Prp String
"HomOpMlt"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall (h :: * -> * -> *). Hom Mlt h => XHomMlt h -> Statement
prpHomMlt XHomMlt (HomOp Mlt)
xsaToOpOp
            , forall (h :: * -> * -> *). Hom Mlt h => XHomMlt h -> Statement
prpHomMlt XHomMlt (HomOp Mlt)
xsaOpposite
            , forall (h :: * -> * -> *). Hom Mlt h => XHomMlt h -> Statement
prpHomMlt XHomMlt (HomOp Mlt)
xsaOpPathInv
            ] where

    xeo :: XOrtSite To (Orientation Symbol)
    xeo :: XOrtSite 'To (Orientation Symbol)
xeo = forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt X Symbol
xSymbol

    xsp' :: XOrtSite From (Path (Op (Orientation Symbol)))
    xsp' :: XOrtSite 'From (Path (Op (Orientation Symbol)))
xsp' = forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> XOrtSite s (Path c)
xosXOrtSitePath (forall x. Dualisable x => x -> Dual x
toDual XOrtSite 'To (Orientation Symbol)
xeo) N
10
    
    xsaOpposite :: XHomMlt (HomOp Mlt)
    xsaOpposite :: XHomMlt (HomOp Mlt)
xsaOpposite = forall (h :: * -> * -> *) (d :: Site).
Hom Mlt h =>
SomeApplMlt d h -> XHomMlt h
xHomMlt (forall (h :: * -> * -> *) a b (d :: Site).
h a b -> XOrtSite d a -> SomeApplMlt d h
SomeApplMlt forall s a.
(Structure s (Op (Orientation a)), Structure s (Orientation a)) =>
HomOp s (Op (Orientation a)) (Orientation a)
Opposite forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Dualisable x => x -> Dual x
toDual XOrtSite 'To (Orientation Symbol)
xeo)

    xsaOpPathInv :: XHomMlt (HomOp Mlt)
    xsaOpPathInv :: XHomMlt (HomOp Mlt)
xsaOpPathInv = forall (h :: * -> * -> *) (d :: Site).
Hom Mlt h =>
SomeApplMlt d h -> XHomMlt h
xHomMlt (forall (h :: * -> * -> *) a b (d :: Site).
h a b -> XOrtSite d a -> SomeApplMlt d h
SomeApplMlt forall s a.
(Structure s a, Structure s (Op (Path a)),
 Structure s (Path (Op a))) =>
HomOp s (Path (Op a)) (Op (Path a))
OpPathInv forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ XOrtSite 'From (Path (Op (Orientation Symbol)))
xsp')

    xsaToOpOp :: XHomMlt (HomOp Mlt)
    xsaToOpOp :: XHomMlt (HomOp Mlt)
xsaToOpOp = forall (h :: * -> * -> *) (d :: Site).
Hom Mlt h =>
SomeApplMlt d h -> XHomMlt h
xHomMlt (forall (h :: * -> * -> *) a b (d :: Site).
h a b -> XOrtSite d a -> SomeApplMlt d h
SomeApplMlt forall s a.
(Structure s (Op (Op a)), Structure s a) =>
HomOp s a (Op (Op a))
ToOpOp XOrtSite 'To (Orientation Symbol)
xeo)