| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
OAlg.Hom.Multiplicative.Proposition
Contents
Description
propositions on homomorphisms between Multiplicative structures.
Synopsis
- prpHomOpMlt :: Statement
- prpHomMlt :: Hom Mlt h => XHomMlt h -> Statement
- data XHomMlt h = XHomMlt (X (SomeApplPnt h)) (X (SomeApplMltp2 h))
- coXHomMlt :: HomMultiplicative h => XHomMlt h -> Dual (XHomMlt h)
- coXHomMltInv :: HomMultiplicative h => Dual (XHomMlt h) -> XHomMlt h
- data SomeApplPnt h where
- SomeApplPnt :: h a b -> Point a -> SomeApplPnt h
- coSomeApplPnt :: Transformable1 Op (ObjectClass h) => SomeApplPnt h -> Dual (SomeApplPnt h)
- coSomeApplPntInv :: Dual (SomeApplPnt h) -> SomeApplPnt h
- data SomeApplMltp2 h where
- SomeApplMltp2 :: h a b -> Mltp2 a -> SomeApplMltp2 h
- coSomeApplMltp2 :: HomMultiplicative h => SomeApplMltp2 h -> Dual (SomeApplMltp2 h)
- coSomeApplMltp2Inv :: HomMultiplicative h => Dual (SomeApplMltp2 h) -> SomeApplMltp2 h
- prpHomMlt1 :: Hom Mlt h => h a b -> Point a -> Statement
- prpHomMlt2 :: Hom Mlt h => h a b -> Mltp2 a -> Statement
- xHomMlt :: Hom Mlt h => SomeApplMlt d h -> XHomMlt h
- xHomMlt' :: h a b -> XMlt a -> XHomMlt h
- xSomeApplPnt :: SomeApplMlt d h -> X (SomeApplPnt h)
- xSomeApplMltp2 :: Hom Mlt h => SomeApplMlt d h -> X (SomeApplMltp2 h)
Proposition
prpHomOpMlt :: Statement Source #
validity of HomOp MltMultiplicative homomorphisms.
Multiplicative
prpHomMlt :: Hom Mlt h => XHomMlt h -> Statement Source #
validity of homomorphisms between Multiplicative structures according to
OAlg.Hom.Multiplicative.
random variable for validating a type family h according to HomMultiplicative.
Constructors
| XHomMlt (X (SomeApplPnt h)) (X (SomeApplMltp2 h)) |
coXHomMlt :: HomMultiplicative h => XHomMlt h -> Dual (XHomMlt h) Source #
to the dual of XHomMlt hcoXHomMltInv.
coXHomMltInv :: HomMultiplicative h => Dual (XHomMlt h) -> XHomMlt h Source #
data SomeApplPnt h where Source #
some application on a point.
Constructors
| SomeApplPnt :: h a b -> Point a -> SomeApplPnt h |
Instances
| type Dual (SomeApplPnt h :: Type) Source # | |
Defined in OAlg.Hom.Multiplicative.Proposition | |
coSomeApplPnt :: Transformable1 Op (ObjectClass h) => SomeApplPnt h -> Dual (SomeApplPnt h) Source #
to the dual of SomeApplPnt hcoSomeApplPntInv.
coSomeApplPntInv :: Dual (SomeApplPnt h) -> SomeApplPnt h Source #
from the dual of Dual (SomeApplPnt h)coSomeApplPnt.
data SomeApplMltp2 h where Source #
some application on multiplicable factors.
Constructors
| SomeApplMltp2 :: h a b -> Mltp2 a -> SomeApplMltp2 h |
Instances
| type Dual (SomeApplMltp2 h :: Type) Source # | |
Defined in OAlg.Hom.Multiplicative.Proposition | |
coSomeApplMltp2 :: HomMultiplicative h => SomeApplMltp2 h -> Dual (SomeApplMltp2 h) Source #
to the dual of SomeApplMltp2 hcoSomeApplMltp2Inv.
coSomeApplMltp2Inv :: HomMultiplicative h => Dual (SomeApplMltp2 h) -> SomeApplMltp2 h Source #
from the dual of Dual (SomeApplMltp2 h)coSomeApplMltp2.
prpHomMlt1 :: Hom Mlt h => h a b -> Point a -> Statement Source #
validity according to OAlg.Hom.Multiplicative.
prpHomMlt2 :: Hom Mlt h => h a b -> Mltp2 a -> Statement Source #
validity according to OAlg.Hom.Multiplicative.
X
xHomMlt :: Hom Mlt h => SomeApplMlt d h -> XHomMlt h Source #
the induced random variable of XHomMlt, given by SomeApplMlt.
xSomeApplPnt :: SomeApplMlt d h -> X (SomeApplPnt h) Source #
random variable for some application on a point given by a SomeApplMlt.
xSomeApplMltp2 :: Hom Mlt h => SomeApplMlt d h -> X (SomeApplMltp2 h) Source #
random variable for some application on multiplicable factors given by a SomeApplMlt.