diff options
Diffstat (limited to 'theories/Classes/Functions.v')
| -rw-r--r-- | theories/Classes/Functions.v | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v index 4c844911..998f8cb7 100644 --- a/theories/Classes/Functions.v +++ b/theories/Classes/Functions.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -13,7 +12,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: Functions.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: Functions.v 11709 2008-12-20 11:42:15Z msozeau $ *) Require Import Coq.Classes.RelationClasses. Require Import Coq.Classes.Morphisms. @@ -21,22 +20,22 @@ Require Import Coq.Classes.Morphisms. Set Implicit Arguments. Unset Strict Implicit. -Class Injective ((m : Morphism (A -> B) (RA ++> RB) f)) : Prop := +Class Injective `(m : Morphism (A -> B) (RA ++> RB) f) : Prop := injective : forall x y : A, RB (f x) (f y) -> RA x y. -Class ((m : Morphism (A -> B) (RA ++> RB) f)) => Surjective : Prop := +Class Surjective `(m : Morphism (A -> B) (RA ++> RB) f) : Prop := surjective : forall y, exists x : A, RB y (f x). -Definition Bijective ((m : Morphism (A -> B) (RA ++> RB) (f : A -> B))) := +Definition Bijective `(m : Morphism (A -> B) (RA ++> RB) (f : A -> B)) := Injective m /\ Surjective m. -Class MonoMorphism (( m : Morphism (A -> B) (eqA ++> eqB) )) := +Class MonoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) := monic :> Injective m. -Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := +Class EpiMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) := epic :> Surjective m. -Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) := - monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m. +Class IsoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) := + { monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m }. -Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ ! IsoMorphism m ] => AutoMorphism. +Class AutoMorphism `(m : Morphism (A -> A) (eqA ++> eqA)) {I : IsoMorphism m}. |