{-# LANGUAGE NoImplicitPrelude #-}

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


-- |
-- Module      : OAlg.Hom.Multiplicative.Definition
-- 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.Definition
  (
    -- * Multiplicative
    HomMultiplicative, IsoMultiplicative

    -- * OpHom
  -- , toOpHomMlt
  , isoFromOpOpMlt
  , isoOppositeMlt
  )
  where

import Data.Typeable

import OAlg.Prelude

import OAlg.Category.Path

import OAlg.Data.Constructable

-- this modules are imported to make the description easier
import OAlg.Structure.Oriented hiding (Path(..))
import OAlg.Structure.Multiplicative

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

--------------------------------------------------------------------------------
-- HomMultiplicative -

-- | type family of homomorphisms between 'Multiplicative' structures.
--
--   __Propoerty__ Let __@h@__ be a type instance of the class 'HomMultiplicative', then
--   for all __@a@__, __@b@__ and @f@ in __@h@__ __@a@__ __@b@__ holds:
--
--   (1) #HomMlt1#For all @p@ in @'Point' __a__@ holds:
--       @'amap' f ('one' p) '==' 'one' ('pmap' f p)@.
--
--   (2) #HomMlt2#For all @x@, @y@ in __@a@__ with @'start' x '==' 'end' y@ holds:
--       @'amap' f (x '*' y) '==' 'amap' f x '*' 'amap' f y@.
--
--  Such a __@h@__ will be called a
--  __/family of homomorphisms between multiplicative structures/__ and an entity @f@ of
--  __@h@__ __@a@__ __@b@__ a __/multiplicative homomorphism/__ between __@a@__ and
-- __@b@__.
--
-- __Note__ If we interpret the types @__a__@ and @__b__@ as small categories (see note at
-- 'Multiplicative') then we can interpret the type family @__h__@ as a family of covariant
-- functors.
class (EmbeddableMorphism h Mlt, HomOriented h) => HomMultiplicative h

instance HomMultiplicative h => HomMultiplicative (Path h)

instance ( HomMultiplicative h, Transformable1 Op t
         , ForgetfulMlt t, ForgetfulTyp t, Typeable t
         )
  => HomMultiplicative (Forget t h)

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

type instance Hom Mlt h = HomMultiplicative h

--------------------------------------------------------------------------------
-- IsoMultiplicative -

-- | isomorphisms between 'Multiplicative' structures.
type IsoMultiplicative h = ( FunctorialHomOriented h, Cayleyan2 h
                           , HomMultiplicative h
                           )

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

instance (TransformableOp s, ForgetfulMlt s, ForgetfulTyp s, Typeable s)
  => HomMultiplicative (IdHom s)

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

instance (TransformableOp s, ForgetfulMlt s, ForgetfulTyp s, Typeable s)
  => HomMultiplicative (HomOp s)

instance (TransformableOp s, ForgetfulMlt s, ForgetfulTyp s, Typeable s)
  => HomMultiplicative (IsoOp s)

--------------------------------------------------------------------------------
-- isoFromOpOpMlt -

-- | the induced isomorphism of 'Multiplicative' structures given by 'FromOpOp'.
isoFromOpOpMlt :: Multiplicative a => IsoOp Mlt (Op (Op a)) a
isoFromOpOpMlt :: forall a. Multiplicative a => IsoOp Mlt (Op (Op a)) a
isoFromOpOpMlt = forall x. Constructable x => Form x -> x
make (forall s a.
(Structure s (Op (Op a)), Structure s a) =>
HomOp s (Op (Op a)) a
FromOpOp forall (m :: * -> * -> *) p z x. m p z -> Path m x p -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath forall s x. Structure s x => Struct s x
Struct)

--------------------------------------------------------------------------------
-- isoOppositeMlt -

-- | the induced isomorphism of 'Oriented' structures given by 'Opposite'.
isoOppositeMlt :: Entity p => IsoOp Mlt (Op (Orientation p)) (Orientation p)
isoOppositeMlt :: forall p.
Entity p =>
IsoOp Mlt (Op (Orientation p)) (Orientation p)
isoOppositeMlt = forall x. Constructable x => Form x -> x
make (forall s p.
(Structure s (Op (Orientation p)), Structure s (Orientation p)) =>
HomOp s (Op (Orientation p)) (Orientation p)
Opposite forall (m :: * -> * -> *) p z x. m p z -> Path m x p -> Path m x z
:. forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath forall s x. Structure s x => Struct s x
Struct)

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

instance HomMultiplicative h => HomMultiplicative (OpHom h)