{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Hom.Oriented.Proposition
-- Description : propositions on homomorphisms between oriented structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- propositions on homomorphisms between 'Oriented' structures.
module OAlg.Hom.Oriented.Proposition
  (
    -- * Proposition
    prpIdHomOrt, prpHomOpOrt

  , prpIsoOpOrtCategory, prpIsoOpOrtFunctorial

    -- * Oriented
  , prpHomOrt, XHomOrt
  , prpHomOrt'
  , prpHomOrt1
  , relHomOrtHomomorphous

    -- * X
  , xIsoOpOrtFrom
  )
  where

import Control.Monad
import Control.Applicative

import Data.Type.Equality

import OAlg.Prelude

import OAlg.Data.Constructable

import OAlg.Category.Path as C
import OAlg.Category.Unify

import OAlg.Data.Symbol

import OAlg.Structure.Oriented as O
import OAlg.Structure.Multiplicative

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


--------------------------------------------------------------------------------
-- XHomOrt -

-- | random variable to validate homomorphisms between 'Oriented' structures.
type XHomOrt h = XAppl h

--------------------------------------------------------------------------------
-- prpHomOrt -

-- | validity of homomorphisms between 'Oriented' for a given value in the domain.
relHomOrtHomomorphous :: Hom Ort h
  => Homomorphous Ort a b -> h a b -> a -> Statement
relHomOrtHomomorphous :: forall (h :: * -> * -> *) a b.
Hom Ort h =>
Homomorphous Ort a b -> h a b -> a -> Statement
relHomOrtHomomorphous (Struct Ort a
Struct:>:Struct Ort b
Struct) h a b
f a
x
  = [Statement] -> Statement
And [ (forall q. Oriented q => q -> Point q
start b
fx forall a. Eq a => a -> a -> Bool
== forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a b
f (forall q. Oriented q => q -> Point q
start a
x)) Bool -> Message -> Statement
:?> Message
prms
        , (forall q. Oriented q => q -> Point q
end b
fx forall a. Eq a => a -> a -> Bool
== forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Point a -> Point b
pmap h a b
f (forall q. Oriented q => q -> Point q
end a
x)) Bool -> Message -> Statement
:?> Message
prms
        ]
  where prms :: Message
prms = [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h a b
f,String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
x]
        fx :: b
fx = forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
f a
x

--------------------------------------------------------------------------------
-- prpHomOrt1 -

-- | validity of homomorphisms between 'Oriented' structures based on the given values.
prpHomOrt1 :: Hom Ort h => h a b -> a -> Statement
prpHomOrt1 :: forall (h :: * -> * -> *) a b. Hom Ort h => h a b -> a -> Statement
prpHomOrt1 h a b
f a
x = String -> Label
Prp String
"HomOrt1" Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *) a b.
Hom Ort h =>
Homomorphous Ort a b -> h a b -> a -> Statement
relHomOrtHomomorphous (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 a
x



-- | validity of homomorphisms between 'Oriented' structures based on the given
-- random variable.
prpHomOrt :: Hom Ort h => XHomOrt h -> Statement
prpHomOrt :: forall (h :: * -> * -> *). Hom Ort h => XHomOrt h -> Statement
prpHomOrt XHomOrt h
xfx = String -> Label
Prp String
"HomOrt"
  Label -> Statement -> Statement
:<=>: forall p. X p -> (p -> Statement) -> Statement
Forall XHomOrt h
xfx (\(SomeApplication h x y
f x
x)
                    -> forall (h :: * -> * -> *) a b.
Hom Ort h =>
Homomorphous Ort a b -> h a b -> a -> Statement
relHomOrtHomomorphous (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 x y
f)) h x y
f x
x
                   )
-- | validity of homomorphisms between 'Oriented' structures based on the given
-- random variable.
prpHomOrt' :: Hom Ort h => h a b -> XOrt a -> Statement
prpHomOrt' :: forall (h :: * -> * -> *) a b.
Hom Ort h =>
h a b -> XOrt a -> Statement
prpHomOrt' h a b
f XOrt a
xa = String -> Label
Label String
"prpHomOrt'" Label -> Statement -> Statement
:<=>:
  forall p. X p -> (p -> Statement) -> Statement
Forall XOrt a
xa (forall (h :: * -> * -> *) a b.
Hom Ort h =>
Homomorphous Ort a b -> h a b -> a -> Statement
relHomOrtHomomorphous (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)
  
--------------------------------------------------------------------------------
-- prpIdHomOrt -

-- | validity of @'IdHom' 'Ort'@ to be a family of 'Oriented' homomorphisms between
-- @'Orientation' 'Symbol'@ and t'Z'.
prpIdHomOrt :: Statement
prpIdHomOrt :: Statement
prpIdHomOrt = String -> Label
Prp String
"IdHomOrt"
  Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *). Hom Ort h => XHomOrt h -> Statement
prpHomOrt XHomOrt (IdHom Ort)
xa where
  
    xa :: XHomOrt (IdHom Ort)
    xa :: XHomOrt (IdHom Ort)
xa = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. [a] -> X a
xOneOf [ XHomOrt (IdHom Ort)
xsaIdHomOrnt
                       , forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: * -> * -> *) p y. h p y -> p -> SomeApplication h
SomeApplication forall s a. Structure s a => IdHom s a a
IdHom) X Z
xZ
                       ]

    xsaIdHomOrnt :: X (SomeApplication (IdHom Ort))
    xsaIdHomOrnt :: XHomOrt (IdHom Ort)
xsaIdHomOrnt = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: * -> * -> *) p y. h p y -> p -> SomeApplication h
SomeApplication forall s a. Structure s a => IdHom s a a
IdHom) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall p. X p -> XOrt (Orientation p)
xOrtOrnt X Symbol
xSymbol

--------------------------------------------------------------------------------
-- prpHomOpOrt -

-- | validity of @'HomOp' 'Ort'@ according to 'HomOriented' on @'Orientation' 'Symbol'@.
prpHomOpOrt :: Statement
prpHomOpOrt :: Statement
prpHomOpOrt = String -> Label
Prp String
"HomOpOrt"
  Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *). Hom Ort h => XHomOrt h -> Statement
prpHomOrt XHomOrt (HomOp Ort)
xa where

    xo :: XOrt OS
xo = forall p. X p -> XOrt (Orientation p)
xOrtOrnt X Symbol
xSymbol
    xs :: XOrtSite 'From OS
xs = forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X Symbol
xSymbol

    xpth :: N -> X (Path OS)
xpth N
n = N -> N -> X N
xNB N
0 N
n forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> X (Path c)
xosPath XOrtSite 'From OS
xs
    
    xa :: XHomOrt (HomOp Ort)
    xa :: XHomOrt (HomOp Ort)
xa = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. [a] -> X a
xOneOf [ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: * -> * -> *) p y. h p y -> p -> SomeApplication h
SomeApplication forall s a.
(Structure s (Op (Op a)), Structure s a) =>
HomOp s (Op (Op a)) a
FromOpOp forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. x -> Op x
Op forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. x -> Op x
Op) XOrt OS
xo 
                       , forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: * -> * -> *) p y. h p y -> p -> SomeApplication h
SomeApplication forall s p.
(Structure s p, Structure s (Op (Path p)),
 Structure s (Path (Op p))) =>
HomOp s (Op (Path p)) (Path (Op p))
OpPath forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. x -> Op x
Op) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ N -> X (Path OS)
xpth N
10
                       , forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (h :: * -> * -> *) p y. h p y -> p -> SomeApplication h
SomeApplication forall s p.
(Structure s (Op (Orientation p)), Structure s (Orientation p)) =>
HomOp s (Op (Orientation p)) (Orientation p)
Opposite forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. x -> Op x
Op) XOrt OS
xo
                       ]
         

--------------------------------------------------------------------------------
-- prpIsoOpOrtCategory -

-- | validity of @'IsoOp' 'Ort'@ according to 'Category' on @'Orientation' 'Symbol'@.
prpIsoOpOrtCategory :: Statement
prpIsoOpOrtCategory :: Statement
prpIsoOpOrtCategory = String -> Label
Prp String
"IsoOpOrtCategory"
  Label -> Statement -> Statement
:<=>: forall (c :: * -> * -> *).
(Category c, Eq2 c, Show2 c) =>
XCat c -> Statement
prpCategory (forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> XCat c
xCat forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (s :: Site) (m :: * -> * -> *).
XFnctMrphSite s m -> XMrphSite s m
xMrphSite XFnctMrphSite 'From (IsoOp Ort)
xIsoOpOrtFrom)

--------------------------------------------------------------------------------
-- prpIsoOpOrtFunctorial -

-- | validity of @'IsoOp' 'Ort'@ according 'Functorial'. 
prpIsoOpOrtFunctorial :: Statement
prpIsoOpOrtFunctorial :: Statement
prpIsoOpOrtFunctorial = String -> Label
Prp String
"IsoOpOrtFunctorial"
  Label -> Statement -> Statement
:<=>: forall (c :: * -> * -> *).
(Functorial c, Show2 c) =>
XFnct c -> Statement
prpFunctorial (forall (c :: * -> * -> *) (s :: Site).
(Category c, Transformable (ObjectClass c) Ent) =>
XFnctMrphSite s c -> XFnct c
xFnct XFnctMrphSite 'From (IsoOp Ort)
xIsoOpOrtFrom)

--------------------------------------------------------------------------------
-- xIsoOpOrtFrom -

-- | random variale of @'IsoOp' 'Ort'@.
xIsoOpOrtFrom :: XFnctMrphSite From (IsoOp Ort)
xIsoOpOrtFrom :: XFnctMrphSite 'From (IsoOp Ort)
xIsoOpOrtFrom = forall (s :: Site) (m :: * -> * -> *).
XMrphSite s m
-> (forall x. Struct (ObjectClass m) x -> X x) -> XFnctMrphSite s m
XFnctMrphSite (forall (m :: * -> * -> *).
X (SomeObjectClass m)
-> (forall x.
    Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x))
-> XMrphSite 'From m
XDomain X (SomeObjectClass (IsoOp Ort))
xss forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdm) forall {a}. Struct Ort a -> X a
xox where
  
  domOpPath :: Struct Ort (Op (O.Path OS))
  domOpPath :: Struct Ort (Op (Path OS))
domOpPath = forall s x. Structure s x => Struct s x
Struct

  domOpPathInv :: Struct Ort (O.Path (Op OS))
  domOpPathInv :: Struct Ort (Path (Op OS))
domOpPathInv = forall s x. Structure s x => Struct s x
Struct

  domOpOS :: Struct Ort (Op OS)
  domOpOS :: Struct Ort (Op OS)
domOpOS = forall s x. Structure s x => Struct s x
Struct

  domOpOpOS :: Struct Ort (Op (Op OS))
  domOpOpOS :: Struct Ort (Op (Op OS))
domOpOpOS = forall s x. Structure s x => Struct s x
Struct
  
  domOS :: Struct Ort OS
  domOS :: Struct Ort OS
domOS = forall s x. Structure s x => Struct s x
Struct

  xOS :: XOrt OS
xOS = forall p. X p -> XOrt (Orientation p)
xOrtOrnt X Symbol
xSymbol
  
  xox :: Struct Ort a -> X a
xox Struct Ort a
d =     forall {a}. Struct Ort a -> X a
xdomOS Struct Ort a
d forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}. Struct Ort a -> X a
xdomOpOS Struct Ort a
d
          forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}. Struct Ort a -> X a
xdomOpPath Struct Ort a
d forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}. Struct Ort a -> X a
xdomOpPathInv Struct Ort a
d
          forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {a}. Struct Ort a -> X a
xdomOpOpOS Struct Ort a
d

  xdomOS :: Struct Ort x -> X x
  xdomOS :: forall {a}. Struct Ort a -> X a
xdomOS Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort OS
domOS of
    Just x :~: OS
Refl -> XOrt OS
xOS
    Maybe (x :~: OS)
Nothing   -> forall x. X x
XEmpty

  xdomOpOS :: Struct Ort x -> X x
  xdomOpOS :: forall {a}. Struct Ort a -> X a
xdomOpOS Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort (Op OS)
domOpOS of
    Just x :~: Op OS
Refl -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op XOrt OS
xOS
    Maybe (x :~: Op OS)
Nothing   -> forall x. X x
XEmpty

  xdomOpPath :: Struct Ort x -> X x
  xdomOpPath :: forall {a}. Struct Ort a -> X a
xdomOpPath Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort (Op (Path OS))
domOpPath of
    Just x :~: Op (Path OS)
Refl -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. x -> Op x
Op (N -> N -> X N
xNB N
0 N
10 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> X (Path c)
xosPath (forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X Symbol
xSymbol))
    Maybe (x :~: Op (Path OS))
Nothing   -> forall x. X x
XEmpty

  xdomOpPathInv :: Struct Ort x -> X x
  xdomOpPathInv :: forall {a}. Struct Ort a -> X a
xdomOpPathInv Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort (Path (Op OS))
domOpPathInv of
    Just x :~: Path (Op OS)
Refl -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => x -> Dual x
toDual (N -> N -> X N
xNB N
0 N
10 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> X (Path c)
xosPath (forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X Symbol
xSymbol))
    Maybe (x :~: Path (Op OS))
Nothing   -> forall x. X x
XEmpty

  xdomOpOpOS :: Struct Ort x -> X x
  xdomOpOpOS :: forall {a}. Struct Ort a -> X a
xdomOpOpOS Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort (Op (Op OS))
domOpOpOS of
    Just x :~: Op (Op OS)
Refl -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall x. x -> Op x
Op forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall x. x -> Op x
Op) XOrt OS
xOS
    Maybe (x :~: Op (Op OS))
Nothing   -> forall x. X x
XEmpty
  
  xss :: X (SomeObjectClass (IsoOp Ort))
xss = forall a. [a] -> X a
xOneOf [ forall (m :: * -> * -> *) p.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) p -> SomeObjectClass m
SomeObjectClass Struct Ort OS
domOS
               , forall (m :: * -> * -> *) p.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) p -> SomeObjectClass m
SomeObjectClass Struct Ort (Op (Path OS))
domOpPath
               , forall (m :: * -> * -> *) p.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) p -> SomeObjectClass m
SomeObjectClass Struct Ort (Path (Op OS))
domOpPathInv
               , forall (m :: * -> * -> *) p.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) p -> SomeObjectClass m
SomeObjectClass Struct Ort (Op OS)
domOpOS
               , forall (m :: * -> * -> *) p.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) p -> SomeObjectClass m
SomeObjectClass Struct Ort (Op (Op OS))
domOpOpOS
               ]

  xsdm :: Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdm Struct Ort x
d =    forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmFromOpOp Struct Ort x
d forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmToOpOp Struct Ort x
d
          forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmOpPath Struct Ort x
d forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmOpPathInv Struct Ort x
d
          forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmOpposite Struct Ort x
d forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmOppositeInv Struct Ort x
d
          
  xsdmFromOpOp :: Struct Ort x -> X (SomeMorphismSite From (IsoOp Ort) x)
  xsdmFromOpOp :: forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmFromOpOp Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort (Op (Op OS))
domOpOpOS of
    Just x :~: Op (Op OS)
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x p. m x p -> SomeMorphismSite 'From m x
SomeMorphismDomain (forall a.
(a ~ OS) =>
Struct Ort (Op (Op a)) -> IsoOp Ort (Op (Op a)) a
f Struct Ort x
d)
    Maybe (x :~: Op (Op OS))
_         -> forall x. X x
XEmpty

  xsdmToOpOp :: Struct Ort x -> X (SomeMorphismSite From (IsoOp Ort) x)
  xsdmToOpOp :: forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmToOpOp Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort OS
domOS of
    Just x :~: OS
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x p. m x p -> SomeMorphismSite 'From m x
SomeMorphismDomain (forall a. Struct Ort a -> IsoOp Ort a (Op (Op a))
f' Struct Ort x
d)
    Maybe (x :~: OS)
_         -> forall x. X x
XEmpty

  xsdmOpPath :: Struct Ort x -> X (SomeMorphismSite From (IsoOp Ort) x)
  xsdmOpPath :: forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmOpPath Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort (Op (Path OS))
domOpPath of
    Just x :~: Op (Path OS)
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x p. m x p -> SomeMorphismSite 'From m x
SomeMorphismDomain (forall a.
(a ~ OS) =>
Struct Ort (Op (Path a)) -> IsoOp Ort (Op (Path a)) (Path (Op a))
p Struct Ort x
d)
    Maybe (x :~: Op (Path OS))
_         -> forall x. X x
XEmpty

  xsdmOpPathInv :: Struct Ort x -> X (SomeMorphismSite From (IsoOp Ort) x)
  xsdmOpPathInv :: forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmOpPathInv Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort (Path (Op OS))
domOpPathInv of
    Just x :~: Path (Op OS)
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x p. m x p -> SomeMorphismSite 'From m x
SomeMorphismDomain (forall a.
(a ~ OS) =>
Struct Ort (Path (Op a)) -> IsoOp Ort (Path (Op a)) (Op (Path a))
p' Struct Ort x
d)
    Maybe (x :~: Path (Op OS))
_         -> forall x. X x
XEmpty

  xsdmOpposite :: Struct Ort x -> X (SomeMorphismSite From (IsoOp Ort) x)
  xsdmOpposite :: forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmOpposite Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort (Op OS)
domOpOS of
    Just x :~: Op OS
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x p. m x p -> SomeMorphismSite 'From m x
SomeMorphismDomain (forall a. (a ~ OS) => Struct Ort (Op a) -> IsoOp Ort (Op a) a
o Struct Ort x
d)
    Maybe (x :~: Op OS)
_         -> forall x. X x
XEmpty

  xsdmOppositeInv :: Struct Ort x -> X (SomeMorphismSite From (IsoOp Ort) x)
  xsdmOppositeInv :: forall {x}.
Struct Ort x -> X (SomeMorphismSite 'From (IsoOp Ort) x)
xsdmOppositeInv Struct Ort x
d = case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Struct Ort x
d Struct Ort OS
domOS of
    Just x :~: OS
Refl -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x p. m x p -> SomeMorphismSite 'From m x
SomeMorphismDomain (forall a. (a ~ OS) => Struct Ort a -> IsoOp Ort a (Op a)
o' Struct Ort x
d)
    Maybe (x :~: OS)
_         -> forall x. X x
XEmpty


  f' :: Struct Ort a -> IsoOp Ort a (Op (Op a))
  f' :: forall a. Struct Ort a -> IsoOp Ort a (Op (Op a))
f' Struct Ort a
Struct = forall (c :: * -> * -> *) x y. Cayleyan2 c => c x y -> c y x
invert2 forall a. Oriented a => IsoOp Ort (Op (Op a)) a
isoFromOpOpOrt

  f :: a ~ OS => Struct Ort (Op (Op a)) -> IsoOp Ort (Op (Op a)) a
  f :: forall a.
(a ~ OS) =>
Struct Ort (Op (Op a)) -> IsoOp Ort (Op (Op a)) a
f Struct Ort (Op (Op a))
Struct = forall a. Oriented a => IsoOp Ort (Op (Op a)) a
isoFromOpOpOrt

  p :: a ~ OS => Struct Ort (Op (O.Path a)) -> IsoOp Ort (Op (O.Path a)) (O.Path (Op a))
  p :: forall a.
(a ~ OS) =>
Struct Ort (Op (Path a)) -> IsoOp Ort (Op (Path a)) (Path (Op a))
p Struct Ort (Op (Path a))
Struct = forall x. Constructable x => Form x -> x
make (forall s p.
(Structure s p, Structure s (Op (Path p)),
 Structure s (Path (Op p))) =>
HomOp s (Op (Path p)) (Path (Op p))
OpPath forall (m :: * -> * -> *) p z x. m p z -> Path m x p -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath forall s x. Structure s x => Struct s x
Struct)

  p' :: a ~ OS => Struct Ort (O.Path (Op a)) -> IsoOp Ort (O.Path (Op a)) (Op (O.Path a))
  p' :: forall a.
(a ~ OS) =>
Struct Ort (Path (Op a)) -> IsoOp Ort (Path (Op a)) (Op (Path a))
p' Struct Ort (Path (Op a))
Struct = forall x. Constructable x => Form x -> x
make (forall s p.
(Structure s p, Structure s (Op (Path p)),
 Structure s (Path (Op p))) =>
HomOp s (Path (Op p)) (Op (Path p))
OpPathInv forall (m :: * -> * -> *) p z x. m p z -> Path m x p -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath forall s x. Structure s x => Struct s x
Struct)

  o :: a ~ OS => Struct Ort (Op a) -> IsoOp Ort (Op a) a
  o :: forall a. (a ~ OS) => Struct Ort (Op a) -> IsoOp Ort (Op a) a
o Struct Ort (Op a)
Struct = forall x. Constructable x => Form x -> x
make (forall s p.
(Structure s (Op (Orientation p)), Structure s (Orientation p)) =>
HomOp s (Op (Orientation p)) (Orientation p)
Opposite forall (m :: * -> * -> *) p z x. m p z -> Path m x p -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath forall s x. Structure s x => Struct s x
Struct)

  o' :: a ~ OS => Struct Ort a -> IsoOp Ort a (Op a)
  o' :: forall a. (a ~ OS) => Struct Ort a -> IsoOp Ort a (Op a)
o' Struct Ort a
Struct = forall x. Constructable x => Form x -> x
make (forall s p.
(Structure s (Op (Orientation p)), Structure s (Orientation p)) =>
HomOp s (Orientation p) (Op (Orientation p))
OppositeInv forall (m :: * -> * -> *) p z x. m p z -> Path m x p -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath forall s x. Structure s x => Struct s x
Struct)