{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Hom.Oriented
-- Description : homomorphisms between fibred structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- homomorphisms between 'Fibred' structures
module OAlg.Hom.Fibred
  (
    -- * Fibred
    HomFibred(..), FunctorialHomFibred

    -- * Fibred Oriented
  , HomFibredOriented

    -- * Proposition
  , prpHomFbrOrt
  )
  where

import Data.Typeable

import OAlg.Prelude

import OAlg.Category.Path

import OAlg.Structure.Fibred

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

--------------------------------------------------------------------------------
-- HomFibred -

-- | type family of homomorphisms between 'Fibred' structures.
--
-- __Property__ Let @h@ be an instance of 'HomFibred' then for all @__a__@, @__b__@ and @f@ in
-- @__h__ __a__ __b__@ and @x@ in @__a__@ holds: @'root' ('amap' f x) '==' 'rmap' f ('root' x)@.
class ( EmbeddableMorphism h Fbr, Applicative h, Entity2 h
      , EmbeddableMorphismTyp h
      ) => HomFibred h where
  rmap :: h a b -> Root a -> Root b
  default rmap :: (EmbeddableMorphism h FbrOrt, HomOriented h)
               => h a b -> Root a -> Root b
  rmap h a b
h = forall (h :: * -> * -> *) a b.
HomOriented h =>
Homomorphous FbrOrt a b -> h a b -> Root a -> Root b
rmap' (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
h)) h a b
h where

    rmap' :: HomOriented h => Homomorphous FbrOrt a b -> h a b -> Root a -> Root b
    rmap' :: forall (h :: * -> * -> *) a b.
HomOriented h =>
Homomorphous FbrOrt a b -> h a b -> Root a -> Root b
rmap' (Struct FbrOrt a
Struct :>: Struct FbrOrt b
Struct) = forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Orientation (Point a) -> Orientation (Point b)
omap

instance HomFibred h => HomFibred (Path h) where
  rmap :: forall a b. Path h a b -> Root a -> Root b
rmap (IdPath Struct (ObjectClass h) a
_) Root a
r = Root a
r
  rmap (h y b
f :. Path h a y
pth) Root a
r = forall (h :: * -> * -> *) a b.
HomFibred h =>
h a b -> Root a -> Root b
rmap h y b
f forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (h :: * -> * -> *) a b.
HomFibred h =>
h a b -> Root a -> Root b
rmap Path h a y
pth Root a
r

--------------------------------------------------------------------------------
-- FunctorialHomFibred -

-- | functorial application of 'Fibred' homomorphisms.
class (Category h, Functorial h, HomFibred h) => FunctorialHomFibred h

instance FunctorialHomFibred h => FunctorialHomFibred (Path h)

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

type instance Hom Fbr h = HomFibred h

--------------------------------------------------------------------------------
-- HomFibredOriented -

-- | type family of homomorphisms between 'FibredOriented' structures.
--
-- __Property__ Let @h@ be an instance of 'HomFibredOriented' then for all @__a__@, @__b__@ and @f@ in
-- @__h__ __a__ __b__@ and @r@ in @'Root' __a__@ holds: @'rmap' f r '==' 'omap' f r@.
class (EmbeddableMorphism h FbrOrt, HomFibred h, HomOriented h)
  => HomFibredOriented h

instance HomFibredOriented h => HomFibredOriented (Path h)

--------------------------------------------------------------------------------
-- prpHomFbrOrt -

relHomFbrOrtHomomorphous :: HomFibredOriented h
  => Homomorphous FbrOrt a b -> h a b -> Root a -> Statement
relHomFbrOrtHomomorphous :: forall (h :: * -> * -> *) a b.
HomFibredOriented h =>
Homomorphous FbrOrt a b -> h a b -> Root a -> Statement
relHomFbrOrtHomomorphous (Struct FbrOrt a
Struct :>: Struct FbrOrt b
Struct) h a b
f Root a
r
  = (forall (h :: * -> * -> *) a b.
HomFibred h =>
h a b -> Root a -> Root b
rmap h a b
f Root a
r forall a. Eq a => a -> a -> Bool
== forall (h :: * -> * -> *) a b.
HomOriented h =>
h a b -> Orientation (Point a) -> Orientation (Point b)
omap 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 'HomFibredOriented'.
prpHomFbrOrt :: HomFibredOriented h => h a b -> Root a -> Statement
prpHomFbrOrt :: forall (h :: * -> * -> *) a b.
HomFibredOriented h =>
h a b -> Root a -> Statement
prpHomFbrOrt h a b
f Root a
r = String -> Label
Prp String
"HomFbrOrt"
  Label -> Statement -> Statement
:<=>: forall (h :: * -> * -> *) a b.
HomFibredOriented h =>
Homomorphous FbrOrt a b -> h a b -> Root a -> Statement
relHomFbrOrtHomomorphous (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

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

type instance Hom FbrOrt h = HomFibredOriented h

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

instance (ForgetfulFbr s, ForgetfulTyp s, Typeable s)
  => HomFibred (IdHom s) where
  rmap :: forall a b. IdHom s a b -> Root a -> Root b
rmap IdHom s a b
IdHom Root a
r = Root a
r
  
instance (TransformableOp s, ForgetfulFbrOrt s, ForgetfulTyp s, Typeable s)
  => HomFibredOriented (IdHom s)

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

instance (TransformableOp s, ForgetfulFbrOrt s, ForgetfulTyp s, Typeable s)
  => HomFibred (HomOp s)
instance (TransformableOp s, ForgetfulFbrOrt s, ForgetfulTyp s, Typeable s)
  => HomFibredOriented (HomOp s)
instance (TransformableOp s, ForgetfulFbrOrt s, ForgetfulTyp s, Typeable s)
  => HomFibred (IsoOp s)
instance (TransformableOp s, ForgetfulFbrOrt s, ForgetfulTyp s, Typeable s)
  => HomFibredOriented (IsoOp s)

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

instance HomFibredOriented h => HomFibred (OpHom h)
instance HomFibredOriented h => HomFibredOriented (OpHom h)