{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Hom.Proposition
-- Description : propositions on homomorphisms between algerbaic structure
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on homomorphisms between algerbaic structure.
module OAlg.Hom.Proposition
  (
    prpIdHom, prpHomOp, prpIsoOpOrt


  , module Ort
  , module Mlt
  )
  where

import OAlg.Prelude

import OAlg.Hom.Oriented as Ort
import OAlg.Hom.Multiplicative as Mlt

--------------------------------------------------------------------------------
-- prpIdHom -

-- | validity of @'IdHom' __s__@ according to 'Category' and 'HomOriented'.
prpIdHom :: Statement
prpIdHom :: Statement
prpIdHom = String -> Label
Prp String
"IdHom"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement
prpIdHomOrt
            ]

--------------------------------------------------------------------------------
-- prpHomOp -

-- | validity of @'HomOp' __s__@ according to 'Category', 'HomOriented' and 'HomMultiplicative'. 
prpHomOp :: Statement
prpHomOp :: Statement
prpHomOp = String -> Label
Prp String
"HomOp"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement
prpHomOpOrt
            , Statement
prpHomOpMlt
            ]

--------------------------------------------------------------------------------
-- prpIsoOpOrt -

-- | validity of @'IsoOp' 'OAlg.Structure.Oriented.Definition.Ort'@ according to 'Category'
-- and 'Functorial'.
prpIsoOpOrt :: Statement
prpIsoOpOrt :: Statement
prpIsoOpOrt = String -> Label
Prp String
"IsoOpOrt"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement
prpIsoOpOrtCategory
            , Statement
prpIsoOpOrtFunctorial
            ]