{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DefaultSignatures #-}
module OAlg.Hom.Additive
(
HomAdditive
, prpHomAdd1, prpHomAdd2
)
where
import Data.Typeable
import OAlg.Prelude
import OAlg.Category.Path
import OAlg.Structure.Fibred
import OAlg.Structure.Additive
import OAlg.Hom.Definition
import OAlg.Hom.Oriented.Definition
import OAlg.Hom.Fibred
class (EmbeddableMorphism h Add, HomFibred h) => HomAdditive h
instance HomAdditive h => HomAdditive (Path h)
type instance Hom Add h = HomAdditive h
instance (ForgetfulAdd s, ForgetfulTyp s, Typeable s) => HomAdditive (IdHom s)
instance (TransformableOp s, ForgetfulFbrOrt s, ForgetfulAdd s, ForgetfulTyp s, Typeable s)
=> HomAdditive (HomOp s)
instance (TransformableOp s, ForgetfulFbrOrt s, ForgetfulAdd s, ForgetfulTyp s, Typeable s)
=> HomAdditive (IsoOp s)
instance (HomAdditive h, HomFibredOriented h) => HomAdditive (OpHom h)
relHomAdd1Homomorphous :: HomAdditive h
=> Homomorphous Add a b -> h a b -> Root a -> Statement
relHomAdd1Homomorphous :: forall (h :: * -> * -> *) a b.
HomAdditive 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
= (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
f (forall a. Additive a => Root a -> a
zero Root a
r) forall a. Eq a => a -> a -> Bool
== forall a. Additive a => Root a -> a
zero (forall (h :: * -> * -> *) a b.
HomFibred h =>
h a b -> Root a -> Root b
rmap h a b
f Root a
r)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h a b
f,String
"r"String -> String -> Parameter
:=forall a. Show a => a -> String
show Root a
r]
prpHomAdd1 :: HomAdditive h => h a b -> Root a -> Statement
prpHomAdd1 :: forall (h :: * -> * -> *) a b.
HomAdditive h =>
h a b -> Root a -> Statement
prpHomAdd1 h a b
f Root a
r = String -> Label
Prp String
"HomAdd1"
Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *) a b.
HomAdditive h =>
Homomorphous Add a b -> h a b -> Root a -> Statement
relHomAdd1Homomorphous (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 Root a
r
relHomAdd2Homomorphous :: HomAdditive h
=> Homomorphous Add a b -> h a b -> Adbl2 a -> Statement
relHomAdd2Homomorphous :: forall (h :: * -> * -> *) a b.
HomAdditive 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)
= (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
f (a
xforall a. Additive a => a -> a -> a
+a
y) forall a. Eq a => a -> a -> Bool
== forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
f a
x forall a. Additive a => a -> a -> a
+ forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap h a b
f a
y)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"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,String
"y"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
y]
prpHomAdd2 :: HomAdditive h => h a b -> Adbl2 a -> Statement
prpHomAdd2 :: forall (h :: * -> * -> *) a b.
HomAdditive h =>
h a b -> Adbl2 a -> Statement
prpHomAdd2 h a b
f Adbl2 a
xy = String -> Label
Prp String
"HomAdd2"
Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *) a b.
HomAdditive h =>
Homomorphous Add a b -> h a b -> Adbl2 a -> Statement
relHomAdd2Homomorphous (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 Adbl2 a
xy