{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Category.NaturalTransformable

-- Description : natural transformable applications.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- Natural transformable applications.

module OAlg.Category.NaturalTransformable
  (

    -- * Transformable

    NaturalTransformable
  , NaturalTransformation(..), roh'
  , NaturalFunctorial

    -- * Natural

  , Natural(..) -- , rohSub


    -- * Duality

  , NaturalTransformableDual1
  
    -- * Proposition

  , prpNaturalTransformable, SomeNaturalApplication(..)
  , relNaturalTransformable
  -- , prpNaturalTransformableEqExt


  ) where

import OAlg.Prelude 

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

-- Natural -


-- | natural associations on @__s__@-structured types

-- between @__f__@ and @__g__@ within @__b__@.

class Natural s b f g where
  roh :: Struct s x -> b (f x) (g x)


{-
--------------------------------------------------------------------------------
-- rohSub -

rohSubStruct :: Natural s b f g
  => Struct v (f x) -> Struct v (g x) -> Struct (SubStruct t s) x
  -> Struct s x -> Sub v b (f x) (g x)
rohSubStruct Struct Struct Struct = Sub . roh

rohSub :: ( Natural s b f g
          , Transformable t s, TransformableG f t v, TransformableG g t v
          )
  => Struct (SubStruct t s) x -> Sub v b (f x) (g x)
rohSub t = rohSubStruct (tauGSubStruct t) (tauGSubStruct t) t (tau (tauSubStruct t)) 

instance ( Natural s b f g, Transformable t s
         , TransformableG f t v, TransformableG g t v
         )
  => Natural (SubStruct t s) (Sub v b) f g where
  roh = rohSub
-}

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

-- NaturalTransformable -


-- | natural generalized associations.

--

-- __Property__ Let @'NaturalTransformable' __s a b f g__@ and

-- @n@ in @'NatrualTransormation __s a b r f g__@, then holds:

--

-- (1) For all @__x__@, @__y__@ and @a@ in @__a x y__@ holds:

-- @'amapG' a '.' 'roh'' n ('domain' a) '.=.' 'roh'' n ('range' a) '.' 'amapG' a@.

class
  ( Natural (ObjectClass a) b f g
  , FunctorialG f a b, FunctorialG g a b
  )
  => NaturalTransformable a b f g

{-
instance ( NaturalTransformable s a b f g
         , TransformableObjectClass v b
         , TransformableG f t v, TransformableG g t v
         , Transformable t s
         )
  => NaturalTransformable (SubStruct t s) (Sub t a) (Sub v b) f g 
-}
--------------------------------------------------------------------------------

-- NaturalTransformation -


-- | witness for a 'NaturalTransformable'.

data NaturalTransformation a b f g where
  NaturalTransformation :: NaturalTransformable a b f g => NaturalTransformation a b f g

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

-- NaturalFunctorial -


-- | natural transformables admitting the functorial propperty.

type NaturalFunctorial a b f g
  = ( NaturalTransformable a b f g
    , FunctorialG f a b, FunctorialG g a b
    )

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

-- NaturalTransformableDual1 -


-- | helper class to avoid undecidable instances.

class NaturalTransformable h b (Dual1 f) (Dual1 g)
  => NaturalTransformableDual1 h b f g
  
--------------------------------------------------------------------------------

-- roh' -


-- | the induced 'roh'.

roh' :: NaturalTransformation a b f g -> Struct (ObjectClass a) x -> b (f x) (g x)
roh' :: forall (a :: * -> * -> *) (b :: * -> * -> *) (f :: * -> *)
       (g :: * -> *) x.
NaturalTransformation a b f g
-> Struct (ObjectClass a) x -> b (f x) (g x)
roh' NaturalTransformation a b f g
NaturalTransformation = Struct (ObjectClass a) x -> b (f x) (g x)
forall x. Struct (ObjectClass a) x -> b (f x) (g x)
forall s (b :: * -> * -> *) (f :: * -> *) (g :: * -> *) x.
Natural s b f g =>
Struct s x -> b (f x) (g x)
roh

{-
--------------------------------------------------------------------------------
-- prpNaturalTransformableEqExt -

relNaturalTransformableEqExt :: EqExt b => NaturalTransformation a b f g -> a x y -> Statement
relNaturalTransformableEqExt n@NaturalTransformation a
  = amapG a . roh' n (domain a) .=. roh' n (range a) . amapG a

-- | validity for 'NaturalTransformable' within 'EqExt'. 
prpNaturalTransformableEqExt :: EqExt b
  => NaturalTransformation s a b f g -> X (SomeMorphism a) -> Statement
prpNaturalTransformableEqExt n xa = Prp "NaturalTransformableEqExt" :<=>:
  Forall xa (\(SomeMorphism a) -> relNaturalTransformableEqExt n a)

instance (EqExt b, XStandard (SomeMorphism a)) => Validable (NaturalTransformation s a b f g) where
  valid n = prpNaturalTransformableEqExt n xStandard
-}
--------------------------------------------------------------------------------

-- SomeNaturalApplication -


-- | some @f@-indexed application.

data SomeNaturalApplication a f g where
  SomeNaturalApplication
    :: (Show2 a, Eq (g y), Show (f x))
    => a x y -> f x -> SomeNaturalApplication a f g

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

-- prpNaturalTransformable -


-- | validity according to 'NaturalTransformable' for some applications.

relNaturalTransformable :: (Show2 a, Eq (g y), Show (f x))
  => NaturalTransformation a (->) f g -> a x y -> f x -> Statement
relNaturalTransformable :: forall (a :: * -> * -> *) (g :: * -> *) y (f :: * -> *) x.
(Show2 a, Eq (g y), Show (f x)) =>
NaturalTransformation a (->) f g -> a x y -> f x -> Statement
relNaturalTransformable n :: NaturalTransformation a (->) f g
n@NaturalTransformation a (->) f g
NaturalTransformation a x y
a f x
f
  = ((a x y -> g x -> g y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a x y
a (g x -> g y) -> g x -> g y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ NaturalTransformation a (->) f g
-> Struct (ObjectClass a) x -> f x -> g x
forall (a :: * -> * -> *) (b :: * -> * -> *) (f :: * -> *)
       (g :: * -> *) x.
NaturalTransformation a b f g
-> Struct (ObjectClass a) x -> b (f x) (g x)
roh' NaturalTransformation a (->) f g
n (a x y -> Struct (ObjectClass a) x
forall x y. a x y -> Struct (ObjectClass a) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain a x y
a) f x
f) g y -> g y -> Bool
forall a. Eq a => a -> a -> Bool
== (NaturalTransformation a (->) f g
-> Struct (ObjectClass a) y -> f y -> g y
forall (a :: * -> * -> *) (b :: * -> * -> *) (f :: * -> *)
       (g :: * -> *) x.
NaturalTransformation a b f g
-> Struct (ObjectClass a) x -> b (f x) (g x)
roh' NaturalTransformation a (->) f g
n (a x y -> Struct (ObjectClass a) y
forall x y. a x y -> Struct (ObjectClass a) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range a x y
a) (f y -> g y) -> f y -> g y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ a x y -> f x -> f y
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a x y
a f x
f))
    Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"a"String -> String -> Parameter
:=a x y -> String
forall a b. a a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 a x y
a,String
"f x"String -> String -> Parameter
:=f x -> String
forall a. Show a => a -> String
show f x
f]

-- | validity according to 'NaturalTransformable' for some applications.

prpNaturalTransformable :: NaturalTransformation a (->) f g
  -> X (SomeNaturalApplication a f g) -> Statement
prpNaturalTransformable :: forall (a :: * -> * -> *) (f :: * -> *) (g :: * -> *).
NaturalTransformation a (->) f g
-> X (SomeNaturalApplication a f g) -> Statement
prpNaturalTransformable NaturalTransformation a (->) f g
n X (SomeNaturalApplication a f g)
xsa = String -> Label
Prp String
"NaturalTransformable" Label -> Statement -> Statement
:<=>:
  X (SomeNaturalApplication a f g)
-> (SomeNaturalApplication a f g -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeNaturalApplication a f g)
xsa (\(SomeNaturalApplication a x y
a f x
f) -> NaturalTransformation a (->) f g -> a x y -> f x -> Statement
forall (a :: * -> * -> *) (g :: * -> *) y (f :: * -> *) x.
(Show2 a, Eq (g y), Show (f x)) =>
NaturalTransformation a (->) f g -> a x y -> f x -> Statement
relNaturalTransformable NaturalTransformation a (->) f g
n a x y
a f x
f)

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

-- NaturalTransformation - Validable -