{-# 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
  ( prpHomDisjOp
  )
  where

import OAlg.Prelude

import OAlg.Hom.Oriented
import OAlg.Hom.Multiplicative
import OAlg.Hom.Fibred
import OAlg.Hom.FibredOriented
import OAlg.Hom.Additive
import OAlg.Hom.Vectorial

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

-- prpHomDisjOp -


-- | validity of @'OAlg.Hom.Definition.HomDisj' __s__ 'OAlg.Structure.Oriented.Opposite.Op'@ as

-- homomorphisms between @__s__@-structured types.

prpHomDisjOp :: Statement
prpHomDisjOp :: Statement
prpHomDisjOp = String -> Label
Prp String
"HomDisjOp" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ Statement
prpHomDisjOpOrt
      , Statement
prpHomDisjOpFbr
      , Statement
prpHomDisjOpFbrOrt
      , Statement
prpHomDisjOpMlt
      , Statement
prpHomDisjOpAdd
      , Statement
prpHomDisjOpVecZ
      ]