{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

-- |

-- Module      : OAlg.Structure.Fibred.Proposition

-- Description : propositions on fibred structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- propositions on 'Fibred' structures.

module OAlg.Structure.Fibred.Proposition
  (
    -- * Fibred

    prpFbr
  )
  where

import OAlg.Prelude

import OAlg.Structure.Fibred.Definition

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

-- prpFbr -


-- | validity for 'Fibred' structures.

prpFbr :: Fibred f => XFbr f -> Statement
prpFbr :: forall f. Fibred f => XFbr f -> Statement
prpFbr XFbr f
xs = String -> Label
Prp String
"Fbr"
  Label -> Statement -> Statement
:<=>: XFbr f -> (f -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall XFbr f
xs (\f
s -> f -> Statement
forall a. Validable a => a -> Statement
valid f
s Statement -> Statement -> Statement
forall b. Boolean b => b -> b -> b
~> Root f -> Statement
forall a. Validable a => a -> Statement
valid (f -> Root f
forall f. Fibred f => f -> Root f
root f
s))