{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Hom.Fibred

-- Description : definition of homomorphisms between fibred structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- definition of homomorphisms between 'Fibred' structures

module OAlg.Hom.Fibred
  (
    -- * Fibred

    HomFibred, FunctorialFibred

    -- * Duality

  , DualisableFibred
  , toDualStk, toDualRt

    -- * X

  , xsoFbrOrtX

    -- * Proposition

  , prpHomFbr, prpHomDisjOpFbr
  , prpHomFibred
  )
  where

import OAlg.Prelude

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

import OAlg.Data.Variant

import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Oriented hiding (Path(..))

import OAlg.Hom.Definition

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

-- HomFibred -


-- | homomorphisms between 'Fibred' structures.

--

-- __Property__ Let @'HomFibred' __h__@, then for all @__x__@, @__y__@ and @h@ in

-- @__h x y__@ holds:

--

-- (1) @'root' '.' 'amap' h '.=.' 'rmap' h '.' 'root'@.

class ( Morphism h, Applicative h, ApplicativeRoot h
      , Transformable (ObjectClass h) Fbr
      ) => HomFibred h where


instance HomFibred h => HomFibred (Path h)
instance TransformableFbr s => HomFibred (HomEmpty s)

instance (HomFibred h, Disjunctive2 h)  => HomFibred (Variant2 v h)

instance HomFibred h => HomFibred (Inv2 h)

instance (Transformable s Fbr, HomFibred h) => HomFibred (Sub s h)

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

-- DualisableFibred -


-- | duality according to @__o__@ on 'FibredOriented' structures.

--

-- __Properties__ Let @'DualisableFibred' __s o__@, then

-- for all @__x__@ and @s@ in @'Struct' __s x__@ holds:

--

-- (1) @'root' '.' 'toDualStk' q s '.=.' 'toDualRt' q s '.' 'root'@.

--

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

class (DualisableG s (->) o Id, DualisableG s (->) o Rt, Transformable s Fbr)
  => DualisableFibred s o

instance (TransformableType s, TransformableFbrOrt s, TransformableOp s) => DualisableFibred s Op

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

-- toDualStk -


-- | the dual stalk ginven by @'DualisableFibred' __s o__@ and induced by

-- @'DualisableG' __s__ (->) __o__ 'Id'@.

toDualStk :: DualisableFibred s o => q o -> Struct s x -> x -> o x
toDualStk :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> x -> o x
toDualStk q o
_ Struct s x
s = (Id x -> Id (o x)) -> x -> o x
forall x y. (Id x -> Id y) -> x -> y
fromIdG (DualityG s (->) o Id -> Struct s x -> Id x -> Id (o x)
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d x) (d (o x))
toDualG' (Struct s x -> DualityG s (->) o Id
forall s (o :: * -> *) x.
DualisableFibred s o =>
Struct s x -> DualityG s (->) o Id
d Struct s x
s) Struct s x
s) where
  d :: DualisableFibred s o => Struct s x -> DualityG s (->) o Id
  d :: forall s (o :: * -> *) x.
DualisableFibred s o =>
Struct s x -> DualityG s (->) o Id
d Struct s x
_ = DualityG s (->) o Id
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *).
DualisableG r c o d =>
DualityG r c o d
DualityG

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

-- toDualRt -


-- | the dual root ginven by @'DualisableFibred' __s o__@ and induced by

-- @'DualisableG' __s__ (->) __o__ 'Rt'@.

toDualRt :: DualisableFibred s o => q o -> Struct s x -> Root x -> Root (o x)
toDualRt :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> Root x -> Root (o x)
toDualRt q o
q Struct s x
s = (Rt x -> Rt (o x)) -> Root x -> Root (o x)
forall x y. (Rt x -> Rt y) -> Root x -> Root y
fromRtG (DualityG s (->) o Rt -> Struct s x -> Rt x -> Rt (o x)
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *)
       (q :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) x.
DualisableG r c o d =>
q c o d -> Struct r x -> c (d x) (d (o x))
toDualG' (q o -> Struct s x -> DualityG s (->) o Rt
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> DualityG s (->) o Rt
d q o
q Struct s x
s) Struct s x
s) where
  d :: DualisableFibred s o => q o -> Struct s x -> DualityG s (->) o Rt
  d :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableFibred s o =>
q o -> Struct s x -> DualityG s (->) o Rt
d q o
_ Struct s x
_ = DualityG s (->) o Rt
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *).
DualisableG r c o d =>
DualityG r c o d
DualityG

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

-- HomDisj - HomFibred -


instance (HomFibred h, DualisableFibred s o) => HomFibred (HomDisj s o h)

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

-- Functorialibred -


-- | functorial morphism, i.e. 'Functorial' and 'FunctorialRoot'.

--

-- __Note__ It's not mandatory being an homomorphism!

class (Functorial h, FunctorialRoot h) => FunctorialFibred h

instance (HomFibred h, DualisableFibred s o) => FunctorialFibred (HomDisj s o h)

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

-- prpHomFbr -


relHomFbrStruct :: (HomFibred h, Show2 h)
  => Homomorphous Fbr x y -> h x y -> x -> Statement
relHomFbrStruct :: forall (h :: * -> * -> *) x y.
(HomFibred h, Show2 h) =>
Homomorphous Fbr x y -> h x y -> x -> Statement
relHomFbrStruct (Struct Fbr x
Struct :>: Struct Fbr y
Struct) h x y
h x
x
  = (y -> Root y
forall f. Fibred f => f -> Root f
root (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x) Root y -> Root y -> Bool
forall a. Eq a => a -> a -> Bool
== h x y -> Root x -> Root y
forall (h :: * -> * -> *) x y.
ApplicativeRoot h =>
h x y -> Root x -> Root y
rmap h x y
h (x -> Root x
forall f. Fibred f => f -> Root f
root x
x)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"h"String -> String -> Parameter
:=h x y -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h x y
h, String
"x"String -> String -> Parameter
:=x -> String
forall a. Show a => a -> String
show x
x]

-- | validity according to 'HomFibred'.

prpHomFbr :: (HomFibred h, Show2 h) => h x y -> x -> Statement
prpHomFbr :: forall (h :: * -> * -> *) x y.
(HomFibred h, Show2 h) =>
h x y -> x -> Statement
prpHomFbr h x y
h x
x = String -> Label
Prp String
"HomFbr" Label -> Statement -> Statement
:<=>: Homomorphous Fbr x y -> h x y -> x -> Statement
forall (h :: * -> * -> *) x y.
(HomFibred h, Show2 h) =>
Homomorphous Fbr x y -> h x y -> x -> Statement
relHomFbrStruct (Homomorphous (ObjectClass h) x y -> Homomorphous Fbr x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (h x y -> Homomorphous (ObjectClass h) x y
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h)) h x y
h x
x

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

-- prpHomFibred -


-- | validity according to 'HomFibred'.

prpHomFibred :: (HomFibred h, Show2 h)
  => X (SomeApplication h) -> Statement
prpHomFibred :: forall (h :: * -> * -> *).
(HomFibred h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomFibred X (SomeApplication h)
xsa = String -> Label
Prp String
"HomFibred" Label -> Statement -> Statement
:<=>: X (SomeApplication h)
-> (SomeApplication h -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeApplication h)
xsa (\(SomeApplication h x y
h x
x) -> h x y -> x -> Statement
forall (h :: * -> * -> *) x y.
(HomFibred h, Show2 h) =>
h x y -> x -> Statement
prpHomFbr h x y
h x
x)

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

-- xsoFbrOrtX -


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

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

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

-- prpHomDisOpFbr -


relHomFbrFbrOrtX :: (HomFibred h, Show2 h)
  => Homomorphous FbrOrtX x y -> h x y -> Statement
relHomFbrFbrOrtX :: forall (h :: * -> * -> *) x y.
(HomFibred h, Show2 h) =>
Homomorphous FbrOrtX x y -> h x y -> Statement
relHomFbrFbrOrtX (Struct FbrOrtX x
Struct :>: Struct FbrOrtX y
Struct) h x y
h
  = X x -> (x -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X x
forall x. XStandard x => X x
xStandard (h x y -> x -> Statement
forall (h :: * -> * -> *) x y.
(HomFibred h, Show2 h) =>
h x y -> x -> Statement
prpHomFbr h x y
h)

relHomDisjOpFbr :: (HomFibred h, Show2 h, Transformable s FbrOrtX, DualisableFibred s o)
  => X (SomeMorphism (HomDisj s o h)) -> Statement
relHomDisjOpFbr :: forall (h :: * -> * -> *) s (o :: * -> *).
(HomFibred h, Show2 h, Transformable s FbrOrtX,
 DualisableFibred s o) =>
X (SomeMorphism (HomDisj s o h)) -> Statement
relHomDisjOpFbr X (SomeMorphism (HomDisj s o h))
xsh = X (SomeMorphism (HomDisj s o h))
-> (SomeMorphism (HomDisj s o h) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism (HomDisj s o h))
xsh
  (\(SomeMorphism HomDisj s o h x y
h) -> Homomorphous FbrOrtX x y -> HomDisj s o h x y -> Statement
forall (h :: * -> * -> *) x y.
(HomFibred h, Show2 h) =>
Homomorphous FbrOrtX x y -> h x y -> Statement
relHomFbrFbrOrtX (Homomorphous s x y -> Homomorphous FbrOrtX x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (HomDisj s o h x y -> Homomorphous (ObjectClass (HomDisj s o h)) x y
forall x y.
HomDisj s o h x y -> Homomorphous (ObjectClass (HomDisj s o h)) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous HomDisj s o h x y
h)) HomDisj s o h x y
h)

-- | validity of @'HomDisjEmpty' 'FbrOrt' 'Op'@ according to 'HomFibred'.

prpHomDisjOpFbr :: Statement
prpHomDisjOpFbr :: Statement
prpHomDisjOpFbr = String -> Label
Prp String
"HomDisjOpFbr" Label -> Statement -> Statement
:<=>: X (SomeMorphism (HomDisjEmpty FbrOrtX Op)) -> Statement
forall (h :: * -> * -> *) s (o :: * -> *).
(HomFibred h, Show2 h, Transformable s FbrOrtX,
 DualisableFibred s o) =>
X (SomeMorphism (HomDisj s o h)) -> Statement
relHomDisjOpFbr X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
xsh where
  xsh :: X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
  xsh :: X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
xsh = (SomeCmpb2 (HomDisjEmpty FbrOrtX Op)
 -> SomeMorphism (HomDisjEmpty FbrOrtX Op))
-> X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
-> X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (HomDisjEmpty FbrOrtX Op)
-> SomeMorphism (HomDisjEmpty FbrOrtX Op)
forall (h :: * -> * -> *).
Category h =>
SomeCmpb2 h -> SomeMorphism h
smCmpb2 (X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
 -> X (SomeMorphism (HomDisjEmpty FbrOrtX Op)))
-> X (SomeCmpb2 (HomDisjEmpty FbrOrtX Op))
-> X (SomeMorphism (HomDisjEmpty FbrOrtX Op))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X (SomeObjectClass (SHom FbrOrtX FbrOrtX Op (HomEmpty FbrOrtX)))
-> X (SomeMorphism (HomEmpty FbrOrtX))
-> X (SomeCmpb2 (HomDisjEmpty FbrOrtX 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 FbrOrtX FbrOrtX Op (HomEmpty FbrOrtX)))
forall s.
(s ~ FbrOrtX) =>
X (SomeObjectClass (SHom s s Op (HomEmpty s)))
xsoFbrOrtX X (SomeMorphism (HomEmpty FbrOrtX))
forall x. X x
XEmpty