{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DefaultSignatures #-}

-- |

-- Module      : OAlg.Hom.Additive

-- Description : homomorphisms between additive structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- homomorphisms between 'Additive' structures

module OAlg.Hom.Additive
  (
    -- * Additive

    HomAdditive

    -- * Duality

  , DualisableAdditive
  
    -- * Proposition

  , prpHomAdditive, prpHomAdd1, prpHomAdd2
  , prpDualisableAdditiveAdd1, prpDualisableAdditiveAdd2
  , prpHomDisjOpAdd
  )
  where

import Data.Kind

import OAlg.Prelude

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

import OAlg.Data.Variant

import OAlg.Structure.Oriented hiding (Path(..))
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive

import OAlg.Hom.Definition
import OAlg.Hom.Fibred

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

-- HomAdditive -


-- | type family of homomorphisms between 'Additive' structures.

--

-- __Property__ Let @__h__@ be a type instance of the class 'HomAdditive', then

-- for all @__a__@, @__b__@ and @f@ in @__h__@ @__a__@ @__b__@ holds:

--

-- (1) #HomAdd1#For all @r@ in @'Root' __a__@ holds:

-- @'amap' f ('zero' r) '==' 'zero' ('rmap' f r)@.

--

-- (2) #HomAdd2#For all @x@ and @y@ in @__a__@ with @'root' x '==' 'root' y@ holds:

-- @'amap' f (x '+' y) ) '==' 'amap' f x '+' 'amap' f y@.

--

--  Such a @__h__@ will be called a

--  __/family of homomorphisms between additive structures/__ and an entity @f@ of

--  @__h__@ @__a__@ @__b__@ a __/additive homomorphism/__ between @__a__@ and

-- @__b__@.

class (HomFibred h, Transformable (ObjectClass h) Add) => HomAdditive h

instance HomAdditive h => HomAdditive (Path h)
instance (TransformableFbr s, TransformableAdd s) => HomAdditive (HomEmpty s)
instance (HomAdditive h, Disjunctive2 h) => HomAdditive (Variant2 v h)

instance HomAdditive h => HomAdditive (Inv2 h)

instance (TransformableAdd s, HomAdditive h) => HomAdditive (Sub s h)

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

-- DualisableAdditive -


-- | duality according to @__o__@ on 'Additive'-structures

--

-- __Properties__ Let @'DualisableAdditive' __s o___@ then for all @__x__@

-- and @s@ in @'Struct' __s x__@ holds:

--

-- (1) For all @r@ in @'Root' __x__@ holds:

-- @'toDualStk' q s ('zero' r) '==' 'zero' ('toDualRt' q s r)@,

--

-- (2) For all @a@, @b@ in @__x__@ with @'root' a '==' 'root' b@ holds:

-- @'toDualStk' q s (a '+' b) '==' 'toDualStk' q s a '+' 'toDualStk' q s b@.

--

-- where @q@ is any proxy for @__o__@.

--

-- __Note__ @'Dualisable' __s__ 'Op'@ holds, because '+' is commutative.

class (DualisableFibred s o, Transformable s Add) => DualisableAdditive s o

instance ( TransformableType s, TransformableFbrOrt s, TransformableOp s
         , TransformableAdd s
         ) => DualisableAdditive s Op

instance (HomAdditive h, DualisableAdditive s o) => HomAdditive (HomDisj s o h)


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

-- prpDualisableAdditiveAdd1 -


relDualisableAdditiveAdd1 :: DualisableAdditive s o
  => q o -> Struct s x -> Struct Add x -> Struct Add (o x) -> Root x -> Statement
relDualisableAdditiveAdd1 :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableAdditive s o =>
q o
-> Struct s x
-> Struct Add x
-> Struct Add (o x)
-> Root x
-> Statement
relDualisableAdditiveAdd1 q o
q Struct s x
s Struct Add x
Struct Struct Add (o x)
Struct Root x
r
  = (q o -> Struct s x -> x -> o x
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> x -> o x
toDualStk q o
q Struct s x
s (Root x -> x
forall a. Additive a => Root a -> a
zero Root x
r) o x -> o x -> Bool
forall a. Eq a => a -> a -> Bool
== Root (o x) -> o x
forall a. Additive a => Root a -> a
zero (q o -> Struct s x -> Root x -> Root (o x)
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> Root x -> Root (o x)
toDualRt q o
q Struct s x
s Root x
r)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"r"String -> String -> Parameter
:=Root x -> String
forall a. Show a => a -> String
show Root x
r]

-- | validity according to 'DualisableAdditive', property 1.

prpDualisableAdditiveAdd1 :: DualisableAdditive s o
  => q o -> Struct s x -> Root x -> Statement
prpDualisableAdditiveAdd1 :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableAdditive s o =>
q o -> Struct s x -> Root x -> Statement
prpDualisableAdditiveAdd1 q o
q Struct s x
s Root x
r = String -> Label
Prp String
"DualisableAdditiveAdd1"
  Label -> Statement -> Statement
:<=>: q o
-> Struct s x
-> Struct Add x
-> Struct Add (o x)
-> Root x
-> Statement
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableAdditive s o =>
q o
-> Struct s x
-> Struct Add x
-> Struct Add (o x)
-> Root x
-> Statement
relDualisableAdditiveAdd1 q o
q Struct s x
s (Struct s x -> Struct Add x
forall x. Struct s x -> Struct Add x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
s) (Struct s (o x) -> Struct Add (o x)
forall x. Struct s x -> Struct Add 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)) Root x
r

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

-- prpDualisableAdditiveAdd2 -

relDualisableAdditiveAdd2 :: DualisableAdditive s o
  => q o -> Struct s x -> Struct Add x -> Struct Add (o x) -> Adbl2 x -> Statement
relDualisableAdditiveAdd2 :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableAdditive s o =>
q o
-> Struct s x
-> Struct Add x
-> Struct Add (o x)
-> Adbl2 x
-> Statement
relDualisableAdditiveAdd2 q o
q Struct s x
s Struct Add x
Struct Struct Add (o x)
Struct ad :: Adbl2 x
ad@(Adbl2 x
a x
b)
  = (q o -> Struct s x -> x -> o x
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> x -> o x
toDualStk q o
q Struct s x
s (x
a x -> x -> x
forall a. Additive a => a -> a -> a
+ x
b) o x -> o x -> Bool
forall a. Eq a => a -> a -> Bool
== q o -> Struct s x -> x -> o x
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> x -> o x
toDualStk q o
q Struct s x
s x
a o x -> o x -> o x
forall a. Additive a => a -> a -> a
+ q o -> Struct s x -> x -> o x
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> x -> o x
toDualStk q o
q Struct s x
s x
b) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"ad"String -> String -> Parameter
:=Adbl2 x -> String
forall a. Show a => a -> String
show Adbl2 x
ad]  

-- | validity according to 'DualisableAdditive', property 2.

prpDualisableAdditiveAdd2 :: DualisableAdditive s o
  => q o -> Struct s x -> Adbl2 x -> Statement
prpDualisableAdditiveAdd2 :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableAdditive s o =>
q o -> Struct s x -> Adbl2 x -> Statement
prpDualisableAdditiveAdd2 q o
q Struct s x
s Adbl2 x
ad = String -> Label
Prp String
"DualisableAdditiveAdd2"
  Label -> Statement -> Statement
:<=>: q o
-> Struct s x
-> Struct Add x
-> Struct Add (o x)
-> Adbl2 x
-> Statement
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableAdditive s o =>
q o
-> Struct s x
-> Struct Add x
-> Struct Add (o x)
-> Adbl2 x
-> Statement
relDualisableAdditiveAdd2 q o
q Struct s x
s (Struct s x -> Struct Add x
forall x. Struct s x -> Struct Add x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
s) (Struct s (o x) -> Struct Add (o x)
forall x. Struct s x -> Struct Add 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)) Adbl2 x
ad

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

-- prpHomAdd1 -


relHomAdd1Homomorphous :: (HomAdditive h, Show2 h)
  => Homomorphous Add a b -> h a b -> Root a -> Statement
relHomAdd1Homomorphous :: forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
Homomorphous Add a b -> h a b -> Root a -> Statement
relHomAdd1Homomorphous (Struct Add a
Struct :>: Struct Add b
Struct) h a b
f Root a
r
  = (h a b -> a -> b
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h a b
f (Root a -> a
forall a. Additive a => Root a -> a
zero Root a
r) b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== Root b -> b
forall a. Additive a => Root a -> a
zero (h a b -> Root a -> Root b
forall (h :: * -> * -> *) x y.
ApplicativeRoot h =>
h x y -> Root x -> Root y
rmap h a b
f Root a
r)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=h a b -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h a b
f,String
"r"String -> String -> Parameter
:=Root a -> String
forall a. Show a => a -> String
show Root a
r]

-- | validity according to "OAlg.Hom.Additive#HomAdd1".

prpHomAdd1 :: (HomAdditive h, Show2 h) => h a b -> Root a -> Statement
prpHomAdd1 :: forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
h a b -> Root a -> Statement
prpHomAdd1 h a b
f Root a
r = String -> Label
Prp String
"HomAdd1"
  Label -> Statement -> Statement
:<=>: Homomorphous Add a b -> h a b -> Root a -> Statement
forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
Homomorphous Add a b -> h a b -> Root a -> Statement
relHomAdd1Homomorphous (Homomorphous (ObjectClass h) a b -> Homomorphous Add a b
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h a b -> Homomorphous (ObjectClass h) a b
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h a b
f)) h a b
f Root a
r

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

-- prpHomAdd2 -


relHomAdd2Homomorphous :: (HomAdditive h, Show2 h)
  => Homomorphous Add a b -> h a b -> Adbl2 a -> Statement
relHomAdd2Homomorphous :: forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
Homomorphous Add a b -> h a b -> Adbl2 a -> Statement
relHomAdd2Homomorphous (Struct Add a
Struct:>:Struct Add b
Struct) h a b
f (Adbl2 a
x a
y)
  = (h a b -> a -> b
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h a b
f (a
xa -> a -> a
forall a. Additive a => a -> a -> a
+a
y) b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== h a b -> a -> b
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h a b
f a
x b -> b -> b
forall a. Additive a => a -> a -> a
+ h a b -> a -> b
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h a b
f a
y)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=h a b -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h a b
f,String
"x"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
x,String
"y"String -> String -> Parameter
:=a -> String
forall a. Show a => a -> String
show a
y]

-- | validity according to "OAlg.Hom.Additive#HomAdd2".

prpHomAdd2 :: (HomAdditive h, Show2 h) => h a b -> Adbl2 a -> Statement
prpHomAdd2 :: forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
h a b -> Adbl2 a -> Statement
prpHomAdd2 h a b
f Adbl2 a
xy = String -> Label
Prp String
"HomAdd2"
  Label -> Statement -> Statement
:<=>: Homomorphous Add a b -> h a b -> Adbl2 a -> Statement
forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
Homomorphous Add a b -> h a b -> Adbl2 a -> Statement
relHomAdd2Homomorphous (Homomorphous (ObjectClass h) a b -> Homomorphous Add a b
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h a b -> Homomorphous (ObjectClass h) a b
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h a b
f)) h a b
f Adbl2 a
xy

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

-- prpHomAdditive -


-- | validity according to 'HomAdditive'.

prpHomAdditive :: (HomAdditive h, Show2 h) => h x y -> XAdd x -> Statement
prpHomAdditive :: forall (h :: * -> * -> *) x y.
(HomAdditive h, Show2 h) =>
h x y -> XAdd x -> Statement
prpHomAdditive h x y
h (XAdd X N
_ X (Root x)
xr X x
_ X (Adbl2 x)
xa2 X (Adbl3 x)
_) = String -> Label
Prp String
"HomAdditive" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ X (Root x) -> (Root x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Root x)
xr (h x y -> Root x -> Statement
forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
h a b -> Root a -> Statement
prpHomAdd1 h x y
h)
      , X (Adbl2 x) -> (Adbl2 x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Adbl2 x)
xa2 (h x y -> Adbl2 x -> Statement
forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
h a b -> Adbl2 a -> Statement
prpHomAdd2 h x y
h)
      ]
  
--------------------------------------------------------------------------------

-- AddX -


data AddX

type instance Structure AddX x = (Additive x, FibredOriented x, XStandardAdd x)

instance Transformable AddX Ort where tau :: forall x. Struct AddX x -> Struct Ort x
tau Struct AddX x
Struct = Struct Ort x
forall s x. Structure s x => Struct s x
Struct
instance TransformableOrt AddX

instance Transformable AddX Fbr where tau :: forall x. Struct AddX x -> Struct Fbr x
tau Struct AddX x
Struct = Struct Fbr x
forall s x. Structure s x => Struct s x
Struct
instance TransformableFbr AddX

instance Transformable AddX FbrOrt where tau :: forall x. Struct AddX x -> Struct FbrOrt x
tau Struct AddX x
Struct = Struct FbrOrt x
forall s x. Structure s x => Struct s x
Struct
instance TransformableFbrOrt AddX

instance Transformable AddX Add where tau :: forall x. Struct AddX x -> Struct Add x
tau Struct AddX x
Struct = Struct Add x
forall s x. Structure s x => Struct s x
Struct
instance TransformableAdd AddX


instance TransformableG Op AddX AddX where tauG :: forall x. Struct AddX x -> Struct AddX (Op x)
tauG Struct AddX x
Struct = Struct AddX (Op x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableOp AddX

instance Transformable AddX Typ where tau :: forall x. Struct AddX x -> Struct Typ x
tau Struct AddX x
Struct = Struct Typ x
forall s x. Structure s x => Struct s x
Struct

instance Transformable AddX Type where tau :: forall x. Struct AddX x -> Struct (*) x
tau Struct AddX x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct
instance TransformableType AddX

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

-- xsoAddX


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

                 ]
        
--------------------------------------------------------------------------------

-- prpHomDisjOpAdd -


relHomAddAddX :: (HomAdditive h, Show2 h)
  => Homomorphous AddX x y -> h x y -> Statement
relHomAddAddX :: forall (h :: * -> * -> *) x y.
(HomAdditive h, Show2 h) =>
Homomorphous AddX x y -> h x y -> Statement
relHomAddAddX (Struct AddX x
Struct :>: Struct AddX y
Struct) h x y
h
  = [Statement] -> Statement
And [ X (Orientation (Point x))
-> (Orientation (Point x) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Orientation (Point x))
X (Root x)
xr (h x y -> Root x -> Statement
forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
h a b -> Root a -> Statement
prpHomAdd1 h x y
h)
        , X (Adbl2 x) -> (Adbl2 x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Adbl2 x)
xa2 (h x y -> Adbl2 x -> Statement
forall (h :: * -> * -> *) a b.
(HomAdditive h, Show2 h) =>
h a b -> Adbl2 a -> Statement
prpHomAdd2 h x y
h)
        ]
  where XAdd X N
_ X (Root x)
xr X x
_ X (Adbl2 x)
xa2 X (Adbl3 x)
_ = XAdd x
forall a. XStandardAdd a => XAdd a
xStandardAdd
  
relHomDisjOpAdd :: X (SomeMorphism (HomDisjEmpty AddX Op)) -> Statement
relHomDisjOpAdd :: X (SomeMorphism (HomDisjEmpty AddX Op)) -> Statement
relHomDisjOpAdd X (SomeMorphism (HomDisjEmpty AddX Op))
xsh = X (SomeMorphism (HomDisjEmpty AddX Op))
-> (SomeMorphism (HomDisjEmpty AddX Op) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism (HomDisjEmpty AddX Op))
xsh
  (\(SomeMorphism HomDisjEmpty AddX Op x y
h) -> Homomorphous AddX x y -> HomDisjEmpty AddX Op x y -> Statement
forall (h :: * -> * -> *) x y.
(HomAdditive h, Show2 h) =>
Homomorphous AddX x y -> h x y -> Statement
relHomAddAddX (Homomorphous AddX x y -> Homomorphous AddX x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (HomDisjEmpty AddX Op x y
-> Homomorphous (ObjectClass (HomDisjEmpty AddX Op)) x y
forall x y.
HomDisj AddX Op (HomEmpty AddX) x y
-> Homomorphous (ObjectClass (HomDisjEmpty AddX Op)) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous HomDisjEmpty AddX Op x y
h)) HomDisjEmpty AddX Op x y
h)

-- | validity of @'HomDisjEmpty' 'Add' 'Op'@ according to 'HomAdditive'.

prpHomDisjOpAdd :: Statement
prpHomDisjOpAdd :: Statement
prpHomDisjOpAdd = String -> Label
Prp String
"HomDisjOpAdd" Label -> Statement -> Statement
:<=>: X (SomeMorphism (HomDisjEmpty AddX Op)) -> Statement
relHomDisjOpAdd X (SomeMorphism (HomDisjEmpty AddX Op))
xsh where
  xsh :: X (SomeMorphism (HomDisjEmpty AddX Op))
  xsh :: X (SomeMorphism (HomDisjEmpty AddX Op))
xsh = (SomeCmpb2 (HomDisjEmpty AddX Op)
 -> SomeMorphism (HomDisjEmpty AddX Op))
-> X (SomeCmpb2 (HomDisjEmpty AddX Op))
-> X (SomeMorphism (HomDisjEmpty AddX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (HomDisjEmpty AddX Op)
-> SomeMorphism (HomDisjEmpty AddX Op)
forall (h :: * -> * -> *).
Category h =>
SomeCmpb2 h -> SomeMorphism h
smCmpb2 (X (SomeCmpb2 (HomDisjEmpty AddX Op))
 -> X (SomeMorphism (HomDisjEmpty AddX Op)))
-> X (SomeCmpb2 (HomDisjEmpty AddX Op))
-> X (SomeMorphism (HomDisjEmpty AddX Op))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X (SomeObjectClass (SHom AddX AddX Op (HomEmpty AddX)))
-> X (SomeMorphism (HomEmpty AddX))
-> X (SomeCmpb2 (HomDisjEmpty AddX 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 AddX AddX Op (HomEmpty AddX)))
xsoAddX X (SomeMorphism (HomEmpty AddX))
forall x. X x
XEmpty