{-# LANGUAGE NoImplicitPrelude #-}

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


-- |

-- Module      : OAlg.Hom.Multiplicative

-- Description : definition of homomorphisms between multiplicative structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- definition of homomorphisms between 'Multiplicative' structures.

module OAlg.Hom.Multiplicative
  (
    -- * Disjunctive

    HomMultiplicativeDisjunctive
  , toDualOpMlt, homDisjOpMlt

    -- * Covariant

  , HomMultiplicative

    -- * Dualisable

  , DualisableMultiplicative

    -- * X

  , XHomMlt, xMltHomMlt
  , xosHomMlt
  
    -- * Proposition

  , prpHomMultiplicativeDisjunctive
  , prpHomMultiplicative
  , prpHomDisjMultiplicative, prpHomDisjOpMlt
  , prpDualisableMultiplicativeOne
  , prpDualisableMultiplicativeMlt
  , relMapMltOne, relMapMltCov, relMapMltCnt
  )
  where

import OAlg.Prelude

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

import OAlg.Structure.Oriented hiding (Path(..))
import OAlg.Structure.Multiplicative

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

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

-- HomMultiplicative -


-- | covariant family of homomorphisms between 'Multiplicative' structures.

--

-- __Propoerty__ Let @'HomMultiplicative' __h__@, then

-- for all __@a@__, __@b@__ and @h@ in __@h@__ __@a@__ __@b@__ holds:

--

-- (1) For all @p@ in @'Point' __a__@ holds:

--     @'amap' h ('one' p) '==' 'one' ('pmap' h p)@.

--

-- (2) For all @x@, @y@ in __@a@__ with @'start' x '==' 'end' y@ holds:

--     @'amap'h (x '*' y) '==' 'amap' h x '*' 'amap' h y@.

class (HomOriented h, Transformable (ObjectClass h) Mlt) => HomMultiplicative h

instance HomMultiplicative h => HomMultiplicative (Path h)

instance TransformableMlt s => HomMultiplicative (HomEmpty s)

type instance Hom Mlt h = HomMultiplicative h

instance HomMultiplicative h => HomMultiplicative (Inv2 h)

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

-- HomMultiplicativeDisjunctive -


-- | disjunctive family of homomorphisms between 'Multiplicative' structures.

--

-- __Propoerty__ Let @'HomMultiplicativeDisjunctive' __h__@, then

-- for all __@a@__, __@b@__ and @h@ in __@h@__ __@a@__ __@b@__ holds:

--

-- (1) If @'variant2' h '==' 'Covariant'@ then holds:

--

--     (1) For all @p@ in @'Point' __a__@ holds:

--     @'amap' h ('one' p) '==' 'one' ('pmap' h p)@.

--

--     (2) For all @x@, @y@ in __@a@__ with @'start' x '==' 'end' y@ holds:

--     @'amap' h (x '*' y) '==' 'amap' h x '*' 'amap' h y@.

--

-- (2) If @'variant2' h '==' 'Contravariant'@ then holds:

--

--     (1) For all @p@ in @'Point' __a__@ holds:

--     @'amap' h ('one' p) '==' 'one' ('pmap' h p)@.

--

--     (2) For all @x@, @y@ in __@a@__ with @'start' x '==' 'end' y@ holds:

--     @'amap' h (x '*' y) '==' 'amap' h y '*' 'amap' h x@.

class (HomOrientedDisjunctive h, Transformable (ObjectClass h) Mlt) => HomMultiplicativeDisjunctive h

instance
  ( CategoryDisjunctive h
  , HomMultiplicativeDisjunctive h
  )
  => HomMultiplicativeDisjunctive (Inv2 h)


instance HomMultiplicativeDisjunctive h => HomMultiplicative (Variant2 Covariant h)

instance
  ( TransformableMlt s
  , HomMultiplicativeDisjunctive h
  )
  => HomMultiplicativeDisjunctive (Sub s h)


type instance HomD Mlt h = HomMultiplicativeDisjunctive h

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

-- DualisableMultiplicative -


-- | duality according to @__o__@ on @__s__@-structured 'Multiplicative' types,

--

-- __Properties__ Let @'DualisableMultiplicative' __o s__@ then for all @__x__@

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

-- 

-- (1) For all @p@ in @'Point' __x__@ holds:

-- @'toDualArw' q s ('one' p) '==' 'one' ('toDualPnt' q s p)@. 

--

-- (2) For all @x@, @y@ in @__x__@ with @'start' x '==' 'end' y@ holds:

-- @'toDualArw' q s (x '*' y) '==' 'toDualArw' q s y '*' 'toDualArw' q s x@.

--

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

class (DualisableOriented s o, Transformable s Mlt) => DualisableMultiplicative s o

instance (HomMultiplicative h, DualisableMultiplicative s o)
  => HomMultiplicativeDisjunctive (HomDisj s o h)

instance ( TransformableOrt s, TransformableMlt s, TransformableOp s
         , TransformableType s
         ) => DualisableMultiplicative s Op

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

-- toDualOpMlt -


-- | the canonical 'Contravariant' isomorphism on 'Multiplicative' structures

-- between @__x__@ and @'Op' __x__@.

toDualOpMlt :: Multiplicative x => Variant2 Contravariant (IsoO Mlt Op) x (Op x)
toDualOpMlt :: forall x.
Multiplicative x =>
Variant2 'Contravariant (IsoO Mlt Op) x (Op x)
toDualOpMlt = Struct Mlt x -> Variant2 'Contravariant (IsoO Mlt Op) x (Op x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO Struct Mlt x
forall s x. Structure s x => Struct s x
Struct

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

-- relMapMltOne -


-- | validity that 'one' maps to 'one' according to the given mapplings.

relMapMltOne :: Struct Mlt x -> Struct Mlt y
  -> (x -> y) -> (Point x -> Point y) -> X (Point x) -> Statement
relMapMltOne :: forall x y.
Struct Mlt x
-> Struct Mlt y
-> (x -> y)
-> (Point x -> Point y)
-> X (Point x)
-> Statement
relMapMltOne Struct Mlt x
Struct Struct Mlt y
Struct x -> y
mArw Point x -> Point y
mPnt X (Point x)
xp = X (Point x) -> (Point x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Point x)
xp
  (\Point x
p -> (x -> y
mArw (Point x -> x
forall c. Multiplicative c => Point c -> c
one Point x
p) y -> y -> Bool
forall a. Eq a => a -> a -> Bool
== Point y -> y
forall c. Multiplicative c => Point c -> c
one (Point x -> Point y
mPnt Point x
p)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"p"String -> String -> Parameter
:=Point x -> String
forall a. Show a => a -> String
show Point x
p])

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

-- relMapMlt -


-- | validity of '*' as covariant operation according to the given mapping. 

relMapMltCov :: Struct Mlt x -> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
relMapMltCov :: forall x y.
Struct Mlt x
-> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
relMapMltCov Struct Mlt x
Struct Struct Mlt y
Struct x -> y
mArw X (Mltp2 x)
xmp = String -> Label
Label String
"Cov" Label -> Statement -> Statement
:<=>: X (Mltp2 x) -> (Mltp2 x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Mltp2 x)
xmp
  (\(Mltp2 x
f x
g) -> (x -> y
mArw (x
f x -> x -> x
forall c. Multiplicative c => c -> c -> c
* x
g) y -> y -> Bool
forall a. Eq a => a -> a -> Bool
== x -> y
mArw x
f y -> y -> y
forall c. Multiplicative c => c -> c -> c
* x -> y
mArw x
g) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
f,String
"g"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
g])

-- | validity of '*' as contravariant operation according to the given mapping. 

relMapMltCnt :: Struct Mlt x -> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
relMapMltCnt :: forall x y.
Struct Mlt x
-> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
relMapMltCnt Struct Mlt x
Struct Struct Mlt y
Struct x -> y
mArw X (Mltp2 x)
xmp = String -> Label
Label String
"Cnt" Label -> Statement -> Statement
:<=>: X (Mltp2 x) -> (Mltp2 x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (Mltp2 x)
xmp
  (\(Mltp2 x
f x
g) -> (x -> y
mArw (x
f x -> x -> x
forall c. Multiplicative c => c -> c -> c
* x
g) y -> y -> Bool
forall a. Eq a => a -> a -> Bool
== x -> y
mArw x
g y -> y -> y
forall c. Multiplicative c => c -> c -> c
* x -> y
mArw x
f) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
f,String
"g"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
g])
  
--------------------------------------------------------------------------------

-- prpDualisableMultiplicativeOne -


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

prpDualisableMultiplicativeOne :: DualisableMultiplicative s o
  => q o -> Struct s x -> X (Point x) -> Statement
prpDualisableMultiplicativeOne :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableMultiplicative s o =>
q o -> Struct s x -> X (Point x) -> Statement
prpDualisableMultiplicativeOne q o
q Struct s x
s X (Point x)
xp = String -> Label
Prp String
"DualisableMultiplicativeOne" Label -> Statement -> Statement
:<=>: String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>:
  Struct Mlt x
-> Struct Mlt (o x)
-> (x -> o x)
-> (Point x -> Point (o x))
-> X (Point x)
-> Statement
forall x y.
Struct Mlt x
-> Struct Mlt y
-> (x -> y)
-> (Point x -> Point y)
-> X (Point x)
-> Statement
relMapMltOne (Struct s x -> Struct Mlt x
forall x. Struct s x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
s) (Struct s (o x) -> Struct Mlt (o x)
forall x. Struct s x -> Struct Mlt 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)) x -> o x
mArw Point x -> Point (o x)
mPnt X (Point x)
xp where
    mArw :: x -> o x
mArw = 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
    mPnt :: Point x -> Point (o x)
mPnt = 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

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

-- prpDualisableMultiplicativeMlt -


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

prpDualisableMultiplicativeMlt :: DualisableMultiplicative s o
  => q o -> Struct s x -> X (Mltp2 x) -> Statement
prpDualisableMultiplicativeMlt :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableMultiplicative s o =>
q o -> Struct s x -> X (Mltp2 x) -> Statement
prpDualisableMultiplicativeMlt q o
q Struct s x
s X (Mltp2 x)
xmp = String -> Label
Prp String
"DualisableMultiplicativeMlt" Label -> Statement -> Statement
:<=>: String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>:
  Struct Mlt x
-> Struct Mlt (o x) -> (x -> o x) -> X (Mltp2 x) -> Statement
forall x y.
Struct Mlt x
-> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
relMapMltCnt (Struct s x -> Struct Mlt x
forall x. Struct s x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
s) (Struct s (o x) -> Struct Mlt (o x)
forall x. Struct s x -> Struct Mlt 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)) x -> o x
mArw X (Mltp2 x)
xmp where
    mArw :: x -> o x
mArw = 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

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

-- XHomMlt -


-- | random variable for testing multiplicative homomorphisms.

data XHomMlt x = XHomMlt (X (Point x)) (X (Mltp2 x))

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

-- xMltXHomMlt -


-- | the underlying 'XHomMlt'.

xMltHomMlt :: XMlt x -> XHomMlt x
xMltHomMlt :: forall x. XMlt x -> XHomMlt x
xMltHomMlt (XMlt X N
_ X (Point x)
xp X x
_ X (Endo x)
_ X (Mltp2 x)
xm2 X (Mltp3 x)
_) = X (Point x) -> X (Mltp2 x) -> XHomMlt x
forall x. X (Point x) -> X (Mltp2 x) -> XHomMlt x
XHomMlt X (Point x)
xp X (Mltp2 x)
xm2

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

-- xosHomMlt -


-- | the 'XHomMlt' given by a @'XOrtSite' __d__@

xosHomMlt :: Multiplicative x => XOrtSite d x -> XHomMlt x
xosHomMlt :: forall x (d :: Site). Multiplicative x => XOrtSite d x -> XHomMlt x
xosHomMlt XOrtSite d x
xos = X (Point x) -> X (Mltp2 x) -> XHomMlt x
forall x. X (Point x) -> X (Mltp2 x) -> XHomMlt x
XHomMlt (XOrtSite d x -> X (Point x)
forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint XOrtSite d x
xos) (XOrtSite d x -> X (Mltp2 x)
forall c (d :: Site).
Multiplicative c =>
XOrtSite d c -> X (Mltp2 c)
xMltp2 XOrtSite d x
xos)

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

-- prpHomMultiplicativeDisjunctive -


-- | validity according to 'HomMultiplicativeDisjunctive'.

prpHomMultiplicativeDisjunctive :: HomMultiplicativeDisjunctive h
  => h x y -> XHomMlt x -> Statement
prpHomMultiplicativeDisjunctive :: forall (h :: * -> * -> *) x y.
HomMultiplicativeDisjunctive h =>
h x y -> XHomMlt x -> Statement
prpHomMultiplicativeDisjunctive h x y
h (XHomMlt X (Point x)
xp X (Mltp2 x)
xm2) = String -> Label
Prp String
"HomDisjunctiveMultipliative"
  Label -> Statement -> Statement
:<=>: case h x y -> Variant
forall x y. h x y -> Variant
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
Disjunctive2 h =>
h x y -> Variant
variant2 h x y
h of
    Variant
Covariant     -> String -> Label
Label String
"Cov" Label -> Statement -> Statement
:<=>:
      [Statement] -> Statement
And [ Struct Mlt x
-> Struct Mlt y
-> (x -> y)
-> (Point x -> Point y)
-> X (Point x)
-> Statement
forall x y.
Struct Mlt x
-> Struct Mlt y
-> (x -> y)
-> (Point x -> Point y)
-> X (Point x)
-> Statement
relMapMltOne Struct Mlt x
sx Struct Mlt y
sy x -> y
mArw Point x -> Point y
mPnt X (Point x)
xp
          , Struct Mlt x
-> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
forall x y.
Struct Mlt x
-> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
relMapMltCov Struct Mlt x
sx Struct Mlt y
sy x -> y
mArw X (Mltp2 x)
xm2
          ]
    Variant
Contravariant -> String -> Label
Label String
"Cnt" Label -> Statement -> Statement
:<=>:
      [Statement] -> Statement
And [ Struct Mlt x
-> Struct Mlt y
-> (x -> y)
-> (Point x -> Point y)
-> X (Point x)
-> Statement
forall x y.
Struct Mlt x
-> Struct Mlt y
-> (x -> y)
-> (Point x -> Point y)
-> X (Point x)
-> Statement
relMapMltOne Struct Mlt x
sx Struct Mlt y
sy x -> y
mArw Point x -> Point y
mPnt X (Point x)
xp
          , Struct Mlt x
-> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
forall x y.
Struct Mlt x
-> Struct Mlt y -> (x -> y) -> X (Mltp2 x) -> Statement
relMapMltCnt Struct Mlt x
sx Struct Mlt y
sy x -> y
mArw X (Mltp2 x)
xm2
          ]
  where
    sx :: Struct Mlt x
sx = Struct (ObjectClass h) x -> Struct Mlt x
forall x. Struct (ObjectClass h) x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (h x y -> Struct (ObjectClass h) x
forall x y. h x y -> Struct (ObjectClass h) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h x y
h)
    sy :: Struct Mlt y
sy = Struct (ObjectClass h) y -> Struct Mlt y
forall x. Struct (ObjectClass h) x -> Struct Mlt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (h x y -> Struct (ObjectClass h) y
forall x y. h x y -> Struct (ObjectClass h) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range h x y
h)
    
    mArw :: x -> y
mArw = h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h
    mPnt :: Point x -> Point y
mPnt = 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

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

-- homDisjOpMlt -


-- | embedding a multiplicative homomorphism into a covariant @'HomDisj' __Mlt Op__@.

homDisjOpMlt :: HomMultiplicative h
  => h x y -> Variant2 Covariant (HomDisj Mlt Op h) x y
homDisjOpMlt :: forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
homDisjOpMlt = h x y -> Variant2 'Covariant (HomDisj Mlt 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

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

-- prpHomMultiplicative -


-- | validity according to 'HomMultiplicative'.

prpHomMultiplicative :: HomMultiplicative h
  => h x y -> XHomMlt x -> Statement
prpHomMultiplicative :: forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
h x y -> XHomMlt x -> Statement
prpHomMultiplicative h x y
h XHomMlt x
xhMlt = String -> Label
Prp String
"HomMultiplicative"
  Label -> Statement -> Statement
:<=>: HomDisj Mlt Op h x y -> XHomMlt x -> Statement
forall (h :: * -> * -> *) x y.
HomMultiplicativeDisjunctive h =>
h x y -> XHomMlt x -> Statement
prpHomMultiplicativeDisjunctive HomDisj Mlt Op h x y
h' XHomMlt x
xhMlt where Covariant2 HomDisj Mlt Op h x y
h' = h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
forall (h :: * -> * -> *) x y.
HomMultiplicative h =>
h x y -> Variant2 'Covariant (HomDisj Mlt Op h) x y
homDisjOpMlt h x y
h

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

-- prpHomDisjMultiplicative -


-- | validity according to 'HomMultiplicativeDisjunctive'.

prpHomDisjMultiplicative :: (HomMultiplicative h, DualisableMultiplicative s o)
  => Struct MltX x -> HomDisj s o h x y -> Statement
prpHomDisjMultiplicative :: forall (h :: * -> * -> *) s (o :: * -> *) x y.
(HomMultiplicative h, DualisableMultiplicative s o) =>
Struct MltX x -> HomDisj s o h x y -> Statement
prpHomDisjMultiplicative Struct MltX x
Struct HomDisj s o h x y
h = HomDisj s o h x y -> XHomMlt x -> Statement
forall (h :: * -> * -> *) x y.
HomMultiplicativeDisjunctive h =>
h x y -> XHomMlt x -> Statement
prpHomMultiplicativeDisjunctive HomDisj s o h x y
h (XMlt x -> XHomMlt x
forall x. XMlt x -> XHomMlt x
xMltHomMlt XMlt x
forall c. XStandardMlt c => XMlt c
xStandardMlt)

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

-- xsoMltX -


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

xsoMltX :: s ~ MltX => X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoMltX :: forall s.
(s ~ MltX) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoMltX = [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 MltX OS
forall s x. Structure s x => Struct s x
Struct :: Struct MltX 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 MltX N
forall s x. Structure s x => Struct s x
Struct :: Struct MltX 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 MltX (Op OS)
forall s x. Structure s x => Struct s x
Struct :: Struct MltX (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 MltX (Id OS)
forall s x. Structure s x => Struct s x
Struct :: Struct MltX (Id OS))
                 ]

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

-- prpHomDisjOpMlt -


-- | validity for @'HomDisjEmpty' 'MltX' 'Op'@ beeing 'HomMultiplicativeDisjunctive'.

prpHomDisjOpMlt :: Statement
prpHomDisjOpMlt :: Statement
prpHomDisjOpMlt = String -> Label
Prp String
"prpHomDisjOpMlt" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ X (SomeMorphism (HomDisjEmpty MltX Op))
-> (SomeMorphism (HomDisjEmpty MltX Op) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism (HomDisjEmpty MltX Op))
xm (\(SomeMorphism HomDisjEmpty MltX Op x y
h) -> Struct MltX x -> HomDisjEmpty MltX Op x y -> Statement
forall (h :: * -> * -> *) s (o :: * -> *) x y.
(HomMultiplicative h, DualisableMultiplicative s o) =>
Struct MltX x -> HomDisj s o h x y -> Statement
prpHomDisjMultiplicative (HomDisjEmpty MltX Op x y
-> Struct (ObjectClass (HomDisjEmpty MltX Op)) x
forall x y.
HomDisj MltX Op (HomEmpty MltX) x y
-> Struct (ObjectClass (HomDisjEmpty MltX Op)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain HomDisjEmpty MltX Op x y
h) HomDisjEmpty MltX Op x y
h)
      ]
  where
    xm :: X (SomeMorphism (HomDisjEmpty MltX Op))
    xm :: X (SomeMorphism (HomDisjEmpty MltX Op))
xm = (SomeCmpb2 (HomDisjEmpty MltX Op)
 -> SomeMorphism (HomDisjEmpty MltX Op))
-> X (SomeCmpb2 (HomDisjEmpty MltX Op))
-> X (SomeMorphism (HomDisjEmpty MltX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (HomDisjEmpty MltX Op)
-> SomeMorphism (HomDisjEmpty MltX Op)
forall (h :: * -> * -> *).
Category h =>
SomeCmpb2 h -> SomeMorphism h
smCmpb2 (X (SomeCmpb2 (HomDisjEmpty MltX Op))
 -> X (SomeMorphism (HomDisjEmpty MltX Op)))
-> X (SomeCmpb2 (HomDisjEmpty MltX Op))
-> X (SomeMorphism (HomDisjEmpty MltX Op))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X (SomeObjectClass (SHom MltX MltX Op (HomEmpty MltX)))
-> X (SomeMorphism (HomEmpty MltX))
-> X (SomeCmpb2 (HomDisjEmpty MltX 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 MltX MltX Op (HomEmpty MltX)))
forall s.
(s ~ MltX) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoMltX X (SomeMorphism (HomEmpty MltX))
forall x. X x
XEmpty