{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- 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
  (
    -- * Disjunctive Homomorphism

    prpHomOrientedDisjunctive
  , prpHomOriented

    -- * Duality

  , prpDualisableOriented

    -- * HomDisj

  , prpHomDisjOpOrt
  )
  where

import Control.Monad hiding (Functor(..))

import OAlg.Prelude

import OAlg.Category.Dualisable
import OAlg.Category.SDuality
import OAlg.Category.Unify

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

import OAlg.Structure.Oriented

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

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

-- prpDualisableOriented -


-- | validity according to 'DualisableOriented'.

relDualisableOriented :: DualisableOriented s o
  => q o -> Struct s x -> Struct Ort x -> Struct Ort (o x) -> XOrt x -> Statement
relDualisableOriented :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o
-> Struct s x
-> Struct Ort x
-> Struct Ort (o x)
-> XOrt x
-> Statement
relDualisableOriented q o
q Struct s x
s Struct Ort x
Struct Struct Ort (o x)
Struct XOrt x
xx = XOrt x -> (x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall XOrt x
xx
    (\x
x -> [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: ((o x -> Point (o x)
forall q. Oriented q => q -> Point q
start (o x -> Point (o x)) -> o x -> Point (o x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ x -> o x
tArw x
x) Point (o x) -> Point (o x) -> Bool
forall a. Eq a => a -> a -> Bool
== (Point x -> Point (o x)
tPnt (Point x -> Point (o x)) -> Point x -> Point (o x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ x -> Point x
forall q. Oriented q => q -> Point q
end x
x)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]
               , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: ((o x -> Point (o x)
forall q. Oriented q => q -> Point q
end (o x -> Point (o x)) -> o x -> Point (o x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ x -> o x
tArw x
x) Point (o x) -> Point (o x) -> Bool
forall a. Eq a => a -> a -> Bool
== (Point x -> Point (o x)
tPnt (Point x -> Point (o x)) -> Point x -> Point (o x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ x -> Point x
forall q. Oriented q => q -> Point q
start x
x)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]
               ]
    )
  where
    tArw :: x -> o x
tArw = q o -> Struct s x -> x -> o x
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o -> Struct s x -> x -> o x
toDualArw q o
q Struct s x
s
    tPnt :: Point x -> Point (o x)
tPnt = q o -> Struct s x -> Point x -> Point (o x)
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o -> Struct s x -> Point x -> Point (o x)
toDualPnt q o
q Struct s x
s

-- | validity according to 'DualisableOriented'.

prpDualisableOriented :: DualisableOriented s o
  => q o -> Struct s x -> XOrt x -> Statement
prpDualisableOriented :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o -> Struct s x -> XOrt x -> Statement
prpDualisableOriented q o
q Struct s x
s XOrt x
xx = String -> Label
Prp String
"DualisableOriented" Label -> Statement -> Statement
:<=>:
  q o
-> Struct s x
-> Struct Ort x
-> Struct Ort (o x)
-> XOrt x
-> Statement
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o
-> Struct s x
-> Struct Ort x
-> Struct Ort (o x)
-> XOrt x
-> Statement
relDualisableOriented q o
q Struct s x
s (Struct s x -> Struct Ort x
forall x. Struct s x -> Struct Ort x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
s) (Struct s (o x) -> Struct Ort (o x)
forall x. Struct s x -> Struct Ort x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct s (o x)
forall (o :: * -> *) s x.
Transformable1 o s =>
Struct s x -> Struct s (o x)
tauO Struct s x
s)) XOrt x
xx where

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

-- prpHomDisjOrtVariant -


relHomDisjOrtCov :: (HomOrientedDisjunctive h, Show2 h)
  => Homomorphous Ort x y -> Variant2 Covariant h x y  -> x -> Statement
relHomDisjOrtCov :: forall (h :: * -> * -> *) x y.
(HomOrientedDisjunctive h, Show2 h) =>
Homomorphous Ort x y -> Variant2 'Covariant h x y -> x -> Statement
relHomDisjOrtCov (Struct Ort x
Struct:>:Struct Ort y
Struct) (Covariant2 h x y
h) x
x = String -> Label
Label String
"Covariant" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (y -> Point y
forall q. Oriented q => q -> Point q
start (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x) Point y -> Point y -> Bool
forall a. Eq a => a -> a -> Bool
== h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h (x -> Point x
forall q. Oriented q => q -> Point q
start x
x)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h"String -> String -> Parameter
:= h x y -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h x y
h, String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]
      , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (y -> Point y
forall q. Oriented q => q -> Point q
end (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x) Point y -> Point y -> Bool
forall a. Eq a => a -> a -> Bool
== h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h (x -> Point x
forall q. Oriented q => q -> Point q
end x
x)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h"String -> String -> Parameter
:= h x y -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h x y
h, String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]
      ]

relHomDisjOrtCnt :: (HomOrientedDisjunctive h, Show2 h)
  => Homomorphous Ort x y -> Variant2 Contravariant h x y  -> x -> Statement
relHomDisjOrtCnt :: forall (h :: * -> * -> *) x y.
(HomOrientedDisjunctive h, Show2 h) =>
Homomorphous Ort x y
-> Variant2 'Contravariant h x y -> x -> Statement
relHomDisjOrtCnt (Struct Ort x
Struct:>:Struct Ort y
Struct) (Contravariant2 h x y
h) x
x = String -> Label
Label String
"Contravariant" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (y -> Point y
forall q. Oriented q => q -> Point q
start (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x) Point y -> Point y -> Bool
forall a. Eq a => a -> a -> Bool
== h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h (x -> Point x
forall q. Oriented q => q -> Point q
end x
x)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h"String -> String -> Parameter
:= h x y -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h x y
h, String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]
      , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (y -> Point y
forall q. Oriented q => q -> Point q
end (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x) Point y -> Point y -> Bool
forall a. Eq a => a -> a -> Bool
== h x y -> Point x -> Point y
forall (h :: * -> * -> *) x y.
ApplicativePoint h =>
h x y -> Point x -> Point y
pmap h x y
h (x -> Point x
forall q. Oriented q => q -> Point q
start x
x)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h"String -> String -> Parameter
:= h x y -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h x y
h, String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]
      ]

relHomDisjOrtVariant :: (HomOrientedDisjunctive h, Show2 h)
  => Either2 (Variant2 Contravariant h) (Variant2 Covariant h) x y -> x -> Statement
relHomDisjOrtVariant :: forall (h :: * -> * -> *) x y.
(HomOrientedDisjunctive h, Show2 h) =>
Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
-> x -> Statement
relHomDisjOrtVariant Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
h x
x = case Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
h of
  Right2 Variant2 'Covariant h x y
hCov -> Homomorphous Ort x y -> Variant2 'Covariant h x y -> x -> Statement
forall (h :: * -> * -> *) x y.
(HomOrientedDisjunctive h, Show2 h) =>
Homomorphous Ort x y -> Variant2 'Covariant h x y -> x -> Statement
relHomDisjOrtCov (Homomorphous (ObjectClass h) x y -> Homomorphous Ort x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
-> Homomorphous
     (ObjectClass
        (Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h)))
     x
     y
forall x y.
Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
-> Homomorphous
     (ObjectClass
        (Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h)))
     x
     y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
h)) Variant2 'Covariant h x y
hCov x
x
  Left2 Variant2 'Contravariant h x y
hCnt  -> Homomorphous Ort x y
-> Variant2 'Contravariant h x y -> x -> Statement
forall (h :: * -> * -> *) x y.
(HomOrientedDisjunctive h, Show2 h) =>
Homomorphous Ort x y
-> Variant2 'Contravariant h x y -> x -> Statement
relHomDisjOrtCnt (Homomorphous (ObjectClass h) x y -> Homomorphous Ort x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
-> Homomorphous
     (ObjectClass
        (Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h)))
     x
     y
forall x y.
Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
-> Homomorphous
     (ObjectClass
        (Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h)))
     x
     y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
h)) Variant2 'Contravariant h x y
hCnt x
x

-- | validity according to property (2) of 'HomOrientedDisjunctive'.

prpHomDisjOrtVariant :: (HomOrientedDisjunctive h, Show2 h)
  => X (SomeApplication h) -> Statement
prpHomDisjOrtVariant :: forall (h :: * -> * -> *).
(HomOrientedDisjunctive h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomDisjOrtVariant X (SomeApplication h)
xsa = String -> Label
Prp String
"HomDisjOrtVariant" Label -> Statement -> Statement
:<=>: X (SomeApplication h)
-> (SomeApplication h -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeApplication h)
xsa
  (\(SomeApplication h x y
h x
x) -> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
-> x -> Statement
forall (h :: * -> * -> *) x y.
(HomOrientedDisjunctive h, Show2 h) =>
Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
-> x -> Statement
relHomDisjOrtVariant (h x y
-> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
forall (h :: * -> * -> *) x y.
Disjunctive2 h =>
h x y
-> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
toVariant2 h x y
h) x
x
  )

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

-- prpHomOrientedDisjunctive -


-- | validity according to 'HomOrientedDisjunctive'.

prpHomOrientedDisjunctive :: (HomOrientedDisjunctive h, Show2 h)
  => X (SomeApplication h) -> Statement
prpHomOrientedDisjunctive :: forall (h :: * -> * -> *).
(HomOrientedDisjunctive h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomOrientedDisjunctive X (SomeApplication h)
xa = String -> Label
Prp String
"HomOrientedDisjunctive" Label -> Statement -> Statement
:<=>: X (SomeApplication h) -> Statement
forall (h :: * -> * -> *).
(HomOrientedDisjunctive h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomDisjOrtVariant X (SomeApplication h)
xa

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

-- prpHomOriented -


-- | validity according to 'HomOriented'.

prpHomOriented :: (HomOriented h, Show2 h)
  => X (SomeApplication h) -> Statement
prpHomOriented :: forall (h :: * -> * -> *).
(HomOriented h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomOriented X (SomeApplication h)
xa = String -> Label
Prp String
"HomOriented" Label -> Statement -> Statement
:<=>: X (SomeApplication (HomDisj Ort Op h)) -> Statement
forall (h :: * -> * -> *).
(HomOrientedDisjunctive h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomOrientedDisjunctive ((SomeApplication h -> SomeApplication (HomDisj Ort Op h))
-> X (SomeApplication h) -> X (SomeApplication (HomDisj Ort Op h))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeApplication h -> SomeApplication (HomDisj Ort Op h)
forall (h :: * -> * -> *).
HomOriented h =>
SomeApplication h -> SomeApplication (HomDisj Ort Op h)
saDisj X (SomeApplication h)
xa) where
  saDisj :: HomOriented h => SomeApplication h -> SomeApplication (HomDisj Ort Op h)
  saDisj :: forall (h :: * -> * -> *).
HomOriented h =>
SomeApplication h -> SomeApplication (HomDisj Ort Op h)
saDisj (SomeApplication h x y
h x
x) = HomDisj Ort Op h x y -> x -> SomeApplication (HomDisj Ort Op h)
forall (h :: * -> * -> *) x y. h x y -> x -> SomeApplication h
SomeApplication HomDisj Ort Op h x y
h' x
x where Covariant2 HomDisj Ort Op h x y
h' = h x y -> Variant2 'Covariant (HomDisj Ort Op h) x y
forall (h :: * -> * -> *) s x y (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (HomDisj s o h) x y
homDisj h x y
h

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

-- xsoOrtX -


-- | random variable for some object classes for 'OrtX'.

xsoOrtX :: s ~ OrtX => X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoOrtX :: forall s.
(s ~ OrtX) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoOrtX = [SomeObjectClass (SHom s s Op (HomEmpty s))]
-> X (SomeObjectClass (SHom s s Op (HomEmpty s)))
forall a. [a] -> X a
xOneOf [ Struct (ObjectClass (SHom s s Op (HomEmpty s))) OS
-> SomeObjectClass (SHom s s Op (HomEmpty s))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct OrtX OS
forall s x. Structure s x => Struct s x
Struct :: Struct OrtX OS)
               , Struct (ObjectClass (SHom s s Op (HomEmpty s))) N
-> SomeObjectClass (SHom s s Op (HomEmpty s))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct OrtX N
forall s x. Structure s x => Struct s x
Struct :: Struct OrtX N)
               , Struct (ObjectClass (SHom s s Op (HomEmpty s))) (Op OS)
-> SomeObjectClass (SHom s s Op (HomEmpty s))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct OrtX (Op OS)
forall s x. Structure s x => Struct s x
Struct :: Struct OrtX (Op (OS)))
               , Struct (ObjectClass (SHom s s Op (HomEmpty s))) (Id OS)
-> SomeObjectClass (SHom s s Op (HomEmpty s))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct OrtX (Id OS)
forall s x. Structure s x => Struct s x
Struct :: Struct OrtX (Id (OS)))
               , Struct (ObjectClass (SHom s s Op (HomEmpty s))) (Id Z)
-> SomeObjectClass (SHom s s Op (HomEmpty s))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct OrtX (Id Z)
forall s x. Structure s x => Struct s x
Struct :: Struct OrtX (Id Z))
               ]

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

-- prpHomDisjOpOrt -


-- | validity of @'HomDisjEmpty' 'Ort' 'Op'@ according to 'prpCategoryDisjunctive',

-- 'prpCategoryDualisable', 'prpFunctorialG' and 'prpHomOrientedDisjunctive'.

prpHomDisjOpOrt :: Statement
prpHomDisjOpOrt :: Statement
prpHomDisjOpOrt
  = [Statement] -> Statement
And [ X (SomeObjectClass (HomDisjEmpty OrtX Op))
-> X (SomeCmpb2 (HomDisjEmpty OrtX Op)) -> Statement
forall (c :: * -> * -> *).
(CategoryDisjunctive c, Show2 c) =>
X (SomeObjectClass c) -> X (SomeCmpb2 c) -> Statement
prpCategoryDisjunctive X (SomeObjectClass (HomDisjEmpty OrtX Op))
xo X (SomeCmpb2 (HomDisjEmpty OrtX Op))
xfg
        , Proxy2 Op (HomDisjEmpty OrtX Op)
-> X (SomeObjectClass (HomDisjEmpty OrtX Op)) -> Statement
forall (o :: * -> *) (h :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> *).
(CategoryDualisable o h, EqExt h) =>
q o h -> X (SomeObjectClass h) -> Statement
prpCategoryDualisable Proxy2 Op (HomDisjEmpty OrtX Op)
q X (SomeObjectClass (HomDisjEmpty OrtX Op))
xo
        , FunctorG Id (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt
-> X (SomeObjectClass (Sub OrtX (HomDisjEmpty OrtX Op)))
-> X (SomeCmpb2 (Sub OrtX (HomDisjEmpty OrtX Op)))
-> Statement
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *).
(FunctorialG t a b, EqExt b) =>
q t a b -> X (SomeObjectClass a) -> X (SomeCmpb2 a) -> Statement
prpFunctorialG FunctorG Id (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt
qId' X (SomeObjectClass (Sub OrtX (HomDisjEmpty OrtX Op)))
xo' X (SomeCmpb2 (Sub OrtX (HomDisjEmpty OrtX Op)))
xfg'
        , FunctorG Pnt (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt
-> X (SomeObjectClass (Sub OrtX (HomDisjEmpty OrtX Op)))
-> X (SomeCmpb2 (Sub OrtX (HomDisjEmpty OrtX Op)))
-> Statement
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *).
(FunctorialG t a b, EqExt b) =>
q t a b -> X (SomeObjectClass a) -> X (SomeCmpb2 a) -> Statement
prpFunctorialG FunctorG Pnt (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt
qPt' X (SomeObjectClass (Sub OrtX (HomDisjEmpty OrtX Op)))
xo' X (SomeCmpb2 (Sub OrtX (HomDisjEmpty OrtX Op)))
xfg'
        , X (SomeApplication (HomDisjEmpty OrtX Op)) -> Statement
forall (h :: * -> * -> *).
(HomOrientedDisjunctive h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomOrientedDisjunctive X (SomeApplication (HomDisjEmpty OrtX Op))
xsa
        ] where

  q :: Proxy2 Op (HomDisjEmpty OrtX Op)
q    = Proxy2 Op (HomDisjEmpty OrtX Op)
forall {k} {k1} (a :: k) (b :: k1). Proxy2 a b
Proxy2 :: Proxy2 Op (HomDisjEmpty OrtX Op)
  qId' :: FunctorG Id (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt
qId' = FunctorG Id (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *).
FunctorialG t a b =>
FunctorG t a b
FunctorG :: FunctorG Id (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt
  qPt' :: FunctorG Pnt (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt
qPt' = FunctorG Pnt (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *).
FunctorialG t a b =>
FunctorG t a b
FunctorG :: FunctorG Pnt (Sub OrtX (HomDisjEmpty OrtX Op)) EqualExtOrt

  
  xo :: X (SomeObjectClass (HomDisjEmpty OrtX Op))
  xo :: X (SomeObjectClass (HomDisjEmpty OrtX Op))
xo = (SomeObjectClass (SHom OrtX OrtX Op (HomEmpty OrtX))
 -> SomeObjectClass (HomDisjEmpty OrtX Op))
-> X (SomeObjectClass (SHom OrtX OrtX Op (HomEmpty OrtX)))
-> X (SomeObjectClass (HomDisjEmpty OrtX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(SomeObjectClass Struct (ObjectClass (SHom OrtX OrtX Op (HomEmpty OrtX))) x
s) -> Struct (ObjectClass (HomDisjEmpty OrtX Op)) x
-> SomeObjectClass (HomDisjEmpty OrtX Op)
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass Struct (ObjectClass (SHom OrtX OrtX Op (HomEmpty OrtX))) x
Struct (ObjectClass (HomDisjEmpty OrtX Op)) x
s) X (SomeObjectClass (SHom OrtX OrtX Op (HomEmpty OrtX)))
forall s.
(s ~ OrtX) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoOrtX
  

  xo' :: X (SomeObjectClass (Sub OrtX (HomDisjEmpty OrtX Op)))
  xo' :: X (SomeObjectClass (Sub OrtX (HomDisjEmpty OrtX Op)))
xo' = (SomeObjectClass (HomDisjEmpty OrtX Op)
 -> SomeObjectClass (Sub OrtX (HomDisjEmpty OrtX Op)))
-> X (SomeObjectClass (HomDisjEmpty OrtX Op))
-> X (SomeObjectClass (Sub OrtX (HomDisjEmpty OrtX Op)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(SomeObjectClass Struct (ObjectClass (HomDisjEmpty OrtX Op)) x
s) -> Struct (ObjectClass (Sub OrtX (HomDisjEmpty OrtX Op))) x
-> SomeObjectClass (Sub OrtX (HomDisjEmpty OrtX Op))
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass Struct (ObjectClass (Sub OrtX (HomDisjEmpty OrtX Op))) x
Struct (ObjectClass (HomDisjEmpty OrtX Op)) x
s) X (SomeObjectClass (HomDisjEmpty OrtX Op))
xo

  xfg :: X (SomeCmpb2 (HomDisjEmpty OrtX Op))
  xfg :: X (SomeCmpb2 (HomDisjEmpty OrtX Op))
xfg = X (SomeObjectClass (SHom OrtX OrtX Op (HomEmpty OrtX)))
-> X (SomeMorphism (HomEmpty OrtX))
-> X (SomeCmpb2 (HomDisjEmpty OrtX Op))
forall (o :: * -> *) s (h :: * -> * -> *).
(TransformableG o s s, Morphism h,
 Transformable (ObjectClass h) s) =>
X (SomeObjectClass (SHom s s o h))
-> X (SomeMorphism h) -> X (SomeCmpb2 (HomDisj s o h))
xscmHomDisj X (SomeObjectClass (SHom OrtX OrtX Op (HomEmpty OrtX)))
forall s.
(s ~ OrtX) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoOrtX X (SomeMorphism (HomEmpty OrtX))
forall x. X x
XEmpty

  xfg' :: X (SomeCmpb2 (Sub OrtX (HomDisjEmpty OrtX Op)))
  xfg' :: X (SomeCmpb2 (Sub OrtX (HomDisjEmpty OrtX Op)))
xfg' = (SomeCmpb2 (HomDisjEmpty OrtX Op)
 -> SomeCmpb2 (Sub OrtX (HomDisjEmpty OrtX Op)))
-> X (SomeCmpb2 (HomDisjEmpty OrtX Op))
-> X (SomeCmpb2 (Sub OrtX (HomDisjEmpty OrtX Op)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(SomeCmpb2 HomDisjEmpty OrtX Op y z
f HomDisjEmpty OrtX Op x y
g) -> Sub OrtX (HomDisjEmpty OrtX Op) y z
-> Sub OrtX (HomDisjEmpty OrtX Op) x y
-> SomeCmpb2 (Sub OrtX (HomDisjEmpty OrtX Op))
forall (c :: * -> * -> *) y z x. c y z -> c x y -> SomeCmpb2 c
SomeCmpb2 (HomDisjEmpty OrtX Op y z -> Sub OrtX (HomDisjEmpty OrtX Op) y z
forall (h :: * -> * -> *) s x y.
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Sub s h x y
sub HomDisjEmpty OrtX Op y z
f) (HomDisjEmpty OrtX Op x y -> Sub OrtX (HomDisjEmpty OrtX Op) x y
forall (h :: * -> * -> *) s x y.
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Sub s h x y
sub HomDisjEmpty OrtX Op x y
g)) X (SomeCmpb2 (HomDisjEmpty OrtX Op))
xfg

  xsa :: X (SomeApplication (HomDisjEmpty OrtX Op))
  xsa :: X (SomeApplication (HomDisjEmpty OrtX Op))
xsa = X (X (SomeApplication (HomDisjEmpty OrtX Op)))
-> X (SomeApplication (HomDisjEmpty OrtX Op))
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join
      (X (X (SomeApplication (HomDisjEmpty OrtX Op)))
 -> X (SomeApplication (HomDisjEmpty OrtX Op)))
-> X (X (SomeApplication (HomDisjEmpty OrtX Op)))
-> X (SomeApplication (HomDisjEmpty OrtX Op))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (SomeCmpb2 (HomDisjEmpty OrtX Op)
 -> X (SomeApplication (HomDisjEmpty OrtX Op)))
-> X (SomeCmpb2 (HomDisjEmpty OrtX Op))
-> X (X (SomeApplication (HomDisjEmpty OrtX Op)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1
          (  (\(SomeMorphism HomDisjEmpty OrtX Op x y
m) -> HomDisjEmpty OrtX Op x y
-> X (SomeApplication (HomDisjEmpty OrtX Op))
forall (m :: * -> * -> *) x y.
(Morphism m, Transformable (ObjectClass m) XStd) =>
m x y -> X (SomeApplication m)
xSomeAppl HomDisjEmpty OrtX Op x y
m)
           (SomeMorphism (HomDisjEmpty OrtX Op)
 -> X (SomeApplication (HomDisjEmpty OrtX Op)))
-> (SomeCmpb2 (HomDisjEmpty OrtX Op)
    -> SomeMorphism (HomDisjEmpty OrtX Op))
-> SomeCmpb2 (HomDisjEmpty OrtX Op)
-> X (SomeApplication (HomDisjEmpty OrtX Op))
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
. (\(SomeCmpb2 HomDisjEmpty OrtX Op y z
f HomDisjEmpty OrtX Op x y
g) -> HomDisjEmpty OrtX Op x z -> SomeMorphism (HomDisjEmpty OrtX Op)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (HomDisjEmpty OrtX Op y z
f HomDisjEmpty OrtX Op y z
-> HomDisjEmpty OrtX Op x y -> HomDisjEmpty OrtX Op x z
forall y z x.
HomDisjEmpty OrtX Op y z
-> HomDisjEmpty OrtX Op x y -> HomDisjEmpty OrtX Op x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. HomDisjEmpty OrtX Op x y
g))
          )
      (X (SomeCmpb2 (HomDisjEmpty OrtX Op))
 -> X (X (SomeApplication (HomDisjEmpty OrtX Op))))
-> X (SomeCmpb2 (HomDisjEmpty OrtX Op))
-> X (X (SomeApplication (HomDisjEmpty OrtX Op)))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X (SomeCmpb2 (HomDisjEmpty OrtX Op))
xfg