diff options
Diffstat (limited to 'theories/Classes/Functions.v')
| -rw-r--r-- | theories/Classes/Functions.v | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v new file mode 100644 index 00000000..49fc4f89 --- /dev/null +++ b/theories/Classes/Functions.v @@ -0,0 +1,42 @@ +(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Functional morphisms. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud + 91405 Orsay, France *) + +(* $Id: Functions.v 10739 2008-04-01 14:45:20Z herbelin $ *) + +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. + +Set Implicit Arguments. +Unset Strict Implicit. + +Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop := + injective : forall x y : A, RB (f x) (f y) -> RA x y. + +Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop := + surjective : forall y, exists x : A, RB y (f x). + +Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] := + Injective m /\ Surjective m. + +Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism := + monic :> Injective m. + +Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism := + epic :> Surjective m. + +Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism := + monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m. + +Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism. |