{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Hom.Oriented.Definition

-- Description : definition of homomorphisms between oriented structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- definition of homomorphisms between 'Oriented' structures.

module OAlg.Hom.Oriented.Definition
  (

    -- * Covariant

    HomOriented

    -- * Disjunctive

  , HomOrientedDisjunctive, omapDisj

    -- * Applicative

  , FunctorialOriented

  , module V
  
    -- * Duality

  , DualisableOriented
  , toDualArw, toDualPnt, toDualOrt
  
    -- * Iso

  , toDualOpOrt

  )
  where

import OAlg.Prelude

import OAlg.Category.Dualisable
import OAlg.Category.Path

import OAlg.Data.Variant as V

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

import OAlg.Hom.Definition

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

-- HomOriented -


-- | covariant family of homomorphisms between 'Oriented' structures.

--

-- __Property__ Let @__h__@ be an instance of 'HomOriented', then

-- for all  @__a__@, @__b__@ and @h@ in @__h a b__@ holds:

--

-- (1) @'start' '.' 'amap' h '.=.' 'pmap' h '.' 'start'@.

--

-- (2) @'end' '.' 'amap' h '.=.' 'pmap' h '.' 'end'@.

--

-- __Note__ The above property is equivalent to

-- @'amap' h '.' 'orientation' '.=.' 'orientation' '.' 'omap' h@. 

class ( Morphism h, Applicative h, ApplicativePoint h
      , Transformable (ObjectClass h) Ort
      ) => HomOriented h where

instance HomOriented h => HomOriented (Path h)

instance TransformableOrt s => HomOriented (HomEmpty s)

instance HomOriented h => HomOriented (Id2 h)

instance TransformableOrt s => HomOriented (HomId s)

instance HomOriented h => HomOriented (Inv2 h)

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

-- omapDisj -


-- | induced application respecting the variant by applying 'opposite' for 'Contravariant' cases. 

omapDisj :: (ApplicativePoint h, Disjunctive2 h)
  => h x y -> Orientation (Point x) -> Orientation (Point y)
omapDisj :: forall (h :: * -> * -> *) x y.
(ApplicativePoint h, Disjunctive2 h) =>
h x y -> Orientation (Point x) -> Orientation (Point y)
omapDisj h x y
h = case h x y -> Variant
forall x y. h x y -> Variant
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
Disjunctive2 h =>
h x y -> Variant
variant2 h x y
h of
  Variant
Covariant     -> h x y -> Orientation (Point x) -> Orientation (Point y)
forall (h :: * -> * -> *) a b.
ApplicativePoint h =>
h a b -> Orientation (Point a) -> Orientation (Point b)
omap h x y
h
  Variant
Contravariant -> Orientation (Point y) -> Orientation (Point y)
forall p. Orientation p -> Orientation p
opposite (Orientation (Point y) -> Orientation (Point y))
-> (Orientation (Point x) -> Orientation (Point y))
-> Orientation (Point x)
-> Orientation (Point y)
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h x y -> Orientation (Point x) -> Orientation (Point y)
forall (h :: * -> * -> *) a b.
ApplicativePoint h =>
h a b -> Orientation (Point a) -> Orientation (Point b)
omap h x y
h

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

-- HomOrientedDisjunctive -


-- | disjunctive family of homomorphism between 'Oriented' structures.

--

-- __Properties__ Let @'HomOrientedDisjunctive' __h__@, then

-- for all @__x__@, @__y__@ and @h@ in @__h x y__@ holds:

--

-- (1) If @'variant2' h '==' 'Covariant'@ then holds:

--

--     (1) @'start' '.' 'amap' h '.=.' 'pmap' h '.' 'start'@.

--

--     (2) @'end' '.' 'amap' h '.=.' 'pmap' h '.' 'end'@.

--

-- (2) If @'variant2' h '==' 'Contravariant'@ then holds:

--

--     (1) @'start' '.' 'amap' h '.=.' 'pmap' h '.' 'end'@.

--

--     (2) @'end' ',' 'amap' h '.=.' 'pmap' h '.' 'start'@.

--

-- __Note__ The above property is equivalent to

-- @'orientation' '.' 'amap' h '.=.' 'omapDisj' h '.' 'orientation'@. 

class ( Morphism h, Applicative h, ApplicativePoint h
      , Transformable (ObjectClass h) Ort
      , Disjunctive2 h
      )
  => HomOrientedDisjunctive h

instance HomOrientedDisjunctive h => HomOrientedDisjunctive (Path h)

instance
  ( CategoryDisjunctive h
  , HomOrientedDisjunctive h
  )
  => HomOrientedDisjunctive (Inv2 h)

instance HomOrientedDisjunctive h => HomOriented (Variant2 Covariant h)

instance
  ( Transformable s Ort
  , HomOrientedDisjunctive h
  )
  => HomOrientedDisjunctive (Sub s h)

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

-- DualisableOriented -


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

--

-- __Properties__ Let @'DualisableOriented' __o s__@, then for all @__x__@

-- and @s@ in @'Struct' __s x__@ holds:

-- 

-- (1) @'start' '.' 'toDualArw' q s '.=.' 'toDualPnt' q s '.' 'end'@.

--

-- (2) @'end' '.' 'toDualArw' q s '.=.' 'toDualPnt' q s '.' 'start'@.

--

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

--

-- __Note__ The above property is equivalent to

-- @'orientation' '.' 'toDualArw' q s '.=.' 'toDualOrt' q s '.' 'orientation'@.

class (DualisableG s (->) o Id, DualisableG s (->) o Pnt, Transformable s Ort)
  => DualisableOriented s o

instance (TransformableType s, TransformableOrt s, TransformableOp s) => DualisableOriented s Op

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

-- toDualArw -


-- | the dual arrow given by @'DualisableOriented' __s o__@ and induced by

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

toDualArw :: DualisableOriented s o => q o -> Struct s x -> x -> o x
toDualArw :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o -> Struct s x -> x -> o x
toDualArw 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.
DualisableOriented s o =>
Struct s x -> DualityG s (->) o Id
d Struct s x
s) Struct s x
s) where
  d :: DualisableOriented s o => Struct s x -> DualityG s (->) o Id
  d :: forall s (o :: * -> *) x.
DualisableOriented 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

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

-- toDualPnt -


-- | the dual point given by @'DualisableOriented' __s o__@ and induced by

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

toDualPnt :: DualisableOriented s o => q o -> Struct s x -> Point x -> Point (o x)
toDualPnt :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o -> Struct s x -> Point x -> Point (o x)
toDualPnt q o
q Struct s x
s = (Pnt x -> Pnt (o x)) -> Point x -> Point (o x)
forall x y. (Pnt x -> Pnt y) -> Point x -> Point y
fromPntG (DualityG s (->) o Pnt -> Struct s x -> Pnt x -> Pnt (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 Pnt
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o -> Struct s x -> DualityG s (->) o Pnt
d q o
q Struct s x
s) Struct s x
s) where
  d :: DualisableOriented s o => q o -> Struct s x -> DualityG s (->) o Pnt
  d :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o -> Struct s x -> DualityG s (->) o Pnt
d q o
_ Struct s x
_ = DualityG s (->) o Pnt
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *).
DualisableG r c o d =>
DualityG r c o d
DualityG

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

-- toDualOrt -


-- | the induced dual orientation.

toDualOrt :: DualisableOriented s o => q o -> Struct s x
  -> Orientation (Point x) -> Orientation (Point (o x))
toDualOrt :: forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o
-> Struct s x -> Orientation (Point x) -> Orientation (Point (o x))
toDualOrt q o
q Struct s x
st (Point x
s :> Point x
e) = Orientation (Point (o x)) -> Orientation (Point (o x))
forall p. Orientation p -> Orientation p
opposite (Point x -> Point (o x)
t Point x
s Point (o x) -> Point (o x) -> Orientation (Point (o x))
forall p. p -> p -> Orientation p
:> Point x -> Point (o x)
t Point x
e) where t :: Point x -> Point (o x)
t = q o -> Struct s x -> Point x -> Point (o x)
forall s (o :: * -> *) (q :: (* -> *) -> *) x.
DualisableOriented s o =>
q o -> Struct s x -> Point x -> Point (o x)
toDualPnt q o
q Struct s x
st

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

-- HomDisj - HomOrientedDisjunctive -


instance (HomOriented h, DualisableOriented s o) => HomOrientedDisjunctive (HomDisj s o h)

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

-- FunctorialOriented -


-- | functorial morphismsm, i.e. 'Functorial' and 'FunctorialPoint'.

--

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

class (Functorial h, FunctorialPoint h) => FunctorialOriented h

instance FunctorialOriented h => FunctorialOriented (Inv2 h)

instance (HomOriented h, DualisableOriented s o) => FunctorialOriented (HomDisj s o h)

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

-- toDualOpOrt -


-- | the canonical 'Contravariant' isomorphism on 'Oriented' structures

-- between @__x__@ and @'Op' __x__@.

toDualOpOrt :: Oriented x => Variant2 Contravariant (IsoO Ort Op) x (Op x)
toDualOpOrt :: forall x.
Oriented x =>
Variant2 'Contravariant (IsoO Ort Op) x (Op x)
toDualOpOrt = Struct Ort x -> Variant2 'Contravariant (IsoO Ort Op) x (Op x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO Struct Ort x
forall s x. Structure s x => Struct s x
Struct