{-# 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

    -- * Proposition
  , 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

--------------------------------------------------------------------------------
-- 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 (EmbeddableMorphism h Add, HomFibred h) => HomAdditive h

instance HomAdditive h => HomAdditive (Path h)

--------------------------------------------------------------------------------
-- Hom -

type instance Hom Add h = HomAdditive h

--------------------------------------------------------------------------------
-- IdHom - Hom -

instance (ForgetfulAdd s, ForgetfulTyp s, Typeable s) => HomAdditive (IdHom s)

--------------------------------------------------------------------------------
-- IsoOp - Hom -

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)

--------------------------------------------------------------------------------
-- OpHom -

instance (HomAdditive h, HomFibredOriented h) => HomAdditive (OpHom h)

--------------------------------------------------------------------------------
-- prpHomAdd1 -

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]

-- | validity according to "OAlg.Hom.Additive#HomAdd1".
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

--------------------------------------------------------------------------------
-- prpHomAdd2 -

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]

-- | validity according to "OAlg.Hom.Additive#HomAdd2".
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