{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Structure.FibredOriented

-- Description : definition of fibred oriented structures.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- definition of 'FibredOriented' structures.

module OAlg.Structure.FibredOriented
  (
    -- * Fibred Oriented

    FibredOriented, FbrOrt, TransformableFbrOrt, tauFbrOrt

    -- * X

  , xoFbrOrt, xFbrOrtOrnt
  , XFbrOrt, FbrOrtX

    -- * Proposition

  , prpFbrOrt
  )
  where

import Data.Kind

import Data.List (map)

import OAlg.Prelude

import OAlg.Structure.Oriented

import OAlg.Structure.Fibred.Definition

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

-- FibredOriented -



-- | 'Fibred' and 'Oriented' structure with matching 'root' and 'orientation'.

--

--   __Property__ Let __@d@__ be a 'FibredOriented' structure, then holds:

--

--   (1) @'root' '.=.' 'orientation'@.

--

--   __Note__ 'FibredOriented' structures are required for

--  'OAlg.Structure.Distributive.Distributive' structures.

class (Fibred d, Oriented d, Root d ~ Orientation (Point d)) => FibredOriented d

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

-- Fibred - Instance -


instance FibredOriented ()
instance FibredOriented Int
instance FibredOriented Integer
instance FibredOriented N
instance FibredOriented Z
instance FibredOriented Q
instance Entity p => FibredOriented (Orientation p)
instance FibredOriented x => FibredOriented (Id x)
instance FibredOriented x => Fibred (Op x)
instance FibredOriented x => FibredOriented (Op x)

instance FibredOriented f => Dualisable (Sheaf f) where
  toDual :: Sheaf f -> Dual (Sheaf f)
toDual (Sheaf Root f
r [f]
fs)     = Root (Op f) -> [Op f] -> Sheaf (Op f)
forall f. Root f -> [f] -> Sheaf f
Sheaf (Orientation (Point f) -> Orientation (Point f)
forall x. Transposable x => x -> x
transpose Orientation (Point f)
Root f
r) ((f -> Op f) -> [f] -> [Op f]
forall a b. (a -> b) -> [a] -> [b]
map f -> Op f
forall x. x -> Op x
Op [f]
fs)
  fromDual :: Dual (Sheaf f) -> Sheaf f
fromDual (Sheaf Root (Op f)
r' [Op f]
fs') = Root f -> [f] -> Sheaf f
forall f. Root f -> [f] -> Sheaf f
Sheaf (Orientation (Point f) -> Orientation (Point f)
forall x. Transposable x => x -> x
transpose Orientation (Point f)
Root (Op f)
r') ((Op f -> f) -> [Op f] -> [f]
forall a b. (a -> b) -> [a] -> [b]
map Op f -> f
forall x. Op x -> x
fromOp [Op f]
fs')

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

-- FbrOrt -

  
-- | type representing the class of 'FibredOriented' structures.

data FbrOrt

type instance Structure FbrOrt x = FibredOriented x

instance Transformable FbrOrt Typ where tau :: forall x. Struct FbrOrt x -> Struct Typ x
tau Struct FbrOrt x
Struct = Struct Typ x
forall s x. Structure s x => Struct s x
Struct
instance Transformable FbrOrt Ent where tau :: forall x. Struct FbrOrt x -> Struct Ent x
tau Struct FbrOrt x
Struct = Struct Ent x
forall s x. Structure s x => Struct s x
Struct
instance Transformable FbrOrt Fbr where tau :: forall x. Struct FbrOrt x -> Struct Fbr x
tau Struct FbrOrt x
Struct = Struct Fbr x
forall s x. Structure s x => Struct s x
Struct
instance Transformable FbrOrt Ort where tau :: forall x. Struct FbrOrt x -> Struct Ort x
tau Struct FbrOrt x
Struct = Struct Ort x
forall s x. Structure s x => Struct s x
Struct
instance Transformable FbrOrt Type where tau :: forall x. Struct FbrOrt x -> Struct (*) x
tau Struct FbrOrt x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct

instance TransformableOp FbrOrt

instance TransformableG Op FbrOrt FbrOrt where tauG :: forall x. Struct FbrOrt x -> Struct FbrOrt (Op x)
tauG Struct FbrOrt x
Struct = Struct FbrOrt (Op x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableGRefl Op FbrOrt

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

-- TransformableFbrOrt -


-- | helper class to avoid undecidable instances.

class ( TransformableFbr s, TransformableOrt s
      , Transformable s FbrOrt
      ) => TransformableFbrOrt s

instance TransformableTyp FbrOrt
instance TransformableOrt FbrOrt
instance TransformableFbr FbrOrt
instance TransformableFbrOrt FbrOrt

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

-- tauFbrOrt -


-- | 'tau' for 'FbrOrt'.

tauFbrOrt :: Transformable s FbrOrt => Struct s x -> Struct FbrOrt x
tauFbrOrt :: forall s x. Transformable s FbrOrt => Struct s x -> Struct FbrOrt x
tauFbrOrt = Struct s x -> Struct FbrOrt x
forall x. Struct s x -> Struct FbrOrt x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau

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

-- XFbrOrt -


-- | random variable type for validating 'FibredOriented' structures. 

type XFbrOrt = X

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

-- xFbrOrtOrnt -


-- | random variable for the 'FibredOriented' structure of @'Orientation' p@.

xFbrOrtOrnt :: X p -> XFbrOrt (Orientation p)
xFbrOrtOrnt :: forall p. X p -> XFbrOrt (Orientation p)
xFbrOrtOrnt = X p -> XFbr (Orientation p)
forall p. X p -> XFbrOrt (Orientation p)
xFbrOrnt

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

-- xoFbrOrt -


-- | the associated random variable for validation 'FibredOriented' structures.

xoFbrOrt :: XOrtOrientation f -> XFbrOrt f
xoFbrOrt :: forall f. XOrtOrientation f -> XFbrOrt f
xoFbrOrt = XOrtOrientation f -> XOrt f
forall f. XOrtOrientation f -> XFbrOrt f
xoOrt

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

-- FbrOrtX -


-- | type representing the class 'FibredOriented' equipped with standard random variables.

data FbrOrtX

type instance Structure FbrOrtX x = (FibredOriented x, XStandard x, XStandardPoint x)

instance Transformable FbrOrtX Ort where tau :: forall x. Struct FbrOrtX x -> Struct Ort x
tau Struct FbrOrtX x
Struct = Struct Ort x
forall s x. Structure s x => Struct s x
Struct
instance TransformableOrt FbrOrtX

instance TransformableG Op FbrOrtX FbrOrtX where tauG :: forall x. Struct FbrOrtX x -> Struct FbrOrtX (Op x)
tauG Struct FbrOrtX x
Struct = Struct FbrOrtX (Op x)
forall s x. Structure s x => Struct s x
Struct
instance TransformableOp FbrOrtX

instance Transformable FbrOrtX Fbr where tau :: forall x. Struct FbrOrtX x -> Struct Fbr x
tau Struct FbrOrtX x
Struct = Struct Fbr x
forall s x. Structure s x => Struct s x
Struct
instance TransformableFbr FbrOrtX
instance Transformable FbrOrtX FbrOrt where tau :: forall x. Struct FbrOrtX x -> Struct FbrOrt x
tau Struct FbrOrtX x
Struct = Struct FbrOrt x
forall s x. Structure s x => Struct s x
Struct
instance TransformableFbrOrt FbrOrtX

instance Transformable FbrOrtX Typ where tau :: forall x. Struct FbrOrtX x -> Struct Typ x
tau Struct FbrOrtX x
Struct = Struct Typ x
forall s x. Structure s x => Struct s x
Struct

instance Transformable FbrOrtX Type where tau :: forall x. Struct FbrOrtX x -> Struct (*) x
tau Struct FbrOrtX x
_ = Struct (*) x
forall s x. Structure s x => Struct s x
Struct
instance TransformableType FbrOrtX

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

-- prpFbrOrt -


-- | validity for 'FibredOriented' structures.

prpFbrOrt :: FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt :: forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt XFbrOrt f
xs = String -> Label
Prp String
"FbrOrt" Label -> Statement -> Statement
:<=>:
  String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: f -> Orientation (Point f)
f -> Root f
forall f. Fibred f => f -> Root f
root (f -> Orientation (Point f))
-> (f -> Orientation (Point f)) -> Statement
.=. f -> Orientation (Point f)
forall q. Oriented q => q -> Orientation (Point q)
orientation where .=. :: (f -> Orientation (Point f))
-> (f -> Orientation (Point f)) -> Statement
(.=.) = XFbrOrt f
-> (f -> Orientation (Point f))
-> (f -> Orientation (Point f))
-> Statement
forall x y.
(Show x, Eq y) =>
X x -> (x -> y) -> (x -> y) -> Statement
prpEqualExt XFbrOrt f
xs