| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
OAlg.Hom.FibredOriented
Description
definition of homomorphisms between FibredOriented structures.
Synopsis
- class (HomFibred h, HomOrientedDisjunctive h, Transformable (ObjectClass h) FbrOrt) => HomFibredOrientedDisjunctive (h :: Type -> Type -> Type)
- class (DualisableFibred s o, DualisableOriented s o, Transformable s FbrOrt) => DualisableFibredOriented s (o :: Type -> Type)
- class (HomFibred h, HomOriented h, Transformable (ObjectClass h) FbrOrt) => HomFibredOriented (h :: Type -> Type -> Type)
- toDualOpFbrOrt :: FibredOriented x => Variant2 'Contravariant (IsoO FbrOrt Op) x (Op x)
- prpHomFbrOrt :: (HomFibredOriented h, Show2 h) => h x y -> Root x -> Statement
- prpHomFbrOrtDisj :: (HomFibredOrientedDisjunctive h, Show2 h) => h a b -> Root a -> Statement
- prpDualisableFibredOrientedStk :: forall s (o :: Type -> Type) q x. DualisableFibredOriented s o => q o -> Struct s x -> x -> Statement
- prpDualisableFibredOrientedRt :: forall s (o :: Type -> Type) q x. DualisableFibredOriented s o => q o -> Struct s x -> Root x -> Statement
- prpHomDisjOpFbrOrt :: Statement
Disjunctive
class (HomFibred h, HomOrientedDisjunctive h, Transformable (ObjectClass h) FbrOrt) => HomFibredOrientedDisjunctive (h :: Type -> Type -> Type) Source #
type family of homomorphisms between FibredOriented structures where rmap is given by
omapDisj.
Property Let HomFibredOrientedDisjunctive hx, y and
h in h x y holds:
Instances
| (CategoryDisjunctive h, HomFibredOrientedDisjunctive h) => HomFibredOrientedDisjunctive (Inv2 h) Source # | |
Defined in OAlg.Hom.FibredOriented | |
| HomFibredOrientedDisjunctive h => HomFibredOrientedDisjunctive (Path h) Source # | |
Defined in OAlg.Hom.FibredOriented | |
| (TransformableFbrOrt s, HomFibredOrientedDisjunctive h) => HomFibredOrientedDisjunctive (Sub s h) Source # | |
Defined in OAlg.Hom.FibredOriented | |
| (DualisableDistributive s o, TransformableGRefl o s, TransformableGRefl Matrix s, TransformableDst s) => HomFibredOrientedDisjunctive (HomCo Matrix s o) Source # | |
Defined in OAlg.Entity.Matrix.Definition | |
| (HomFibredOriented h, DualisableFibredOriented s o) => HomFibredOrientedDisjunctive (HomDisj s o h) Source # | |
Defined in OAlg.Hom.FibredOriented | |
class (DualisableFibred s o, DualisableOriented s o, Transformable s FbrOrt) => DualisableFibredOriented s (o :: Type -> Type) Source #
duality according to o on FibredOriented-structures.
Property Let DualisableFibredOriented s ox and
s in Struct s x
Instances
| (TransformableType s, TransformableOrt s, TransformableFbrOrt s, TransformableOp s) => DualisableFibredOriented s Op Source # | |
Defined in OAlg.Hom.FibredOriented | |
Covariant
class (HomFibred h, HomOriented h, Transformable (ObjectClass h) FbrOrt) => HomFibredOriented (h :: Type -> Type -> Type) Source #
type family of homomorphisms between FibredOriented structures where rmap is given by
omap.
Property Let HomFibredOriented hx, y and
h in h x y holds:
Instances
| HomFibredOriented h => HomFibredOriented (Inv2 h) Source # | |
Defined in OAlg.Hom.FibredOriented | |
| HomFibredOriented h => HomFibredOriented (Path h) Source # | |
Defined in OAlg.Hom.FibredOriented | |
| TransformableFbrOrt s => HomFibredOriented (Ornt s) Source # | |
Defined in OAlg.Data.Ornt | |
| (TransformableOrt s, TransformableFbr s, TransformableFbrOrt s) => HomFibredOriented (HomEmpty s) Source # | |
Defined in OAlg.Hom.FibredOriented | |
| HomFibredOrientedDisjunctive h => HomFibredOriented (Variant2 'Covariant h) Source # | |
Defined in OAlg.Hom.FibredOriented | |
Iso
toDualOpFbrOrt :: FibredOriented x => Variant2 'Contravariant (IsoO FbrOrt Op) x (Op x) Source #
the canonical Contravariant isomorphism on FibredOriented structures
between x and Op x
Proposition
prpHomFbrOrt :: (HomFibredOriented h, Show2 h) => h x y -> Root x -> Statement Source #
validity accordint to HomFibredOriented.
prpHomFbrOrtDisj :: (HomFibredOrientedDisjunctive h, Show2 h) => h a b -> Root a -> Statement Source #
validity according to HomFibredOrientedDisjunctive.
prpDualisableFibredOrientedStk :: forall s (o :: Type -> Type) q x. DualisableFibredOriented s o => q o -> Struct s x -> x -> Statement Source #
validity according to DualisableFibredOriented.
prpDualisableFibredOrientedRt :: forall s (o :: Type -> Type) q x. DualisableFibredOriented s o => q o -> Struct s x -> Root x -> Statement Source #
validity according to DualisableFibredOriented.
prpHomDisjOpFbrOrt :: Statement Source #
validity of HomDisjEmpty FbrOrt OpHomFibredOrientedDisjunctive.