Quotients |
Require Export equiv.
Implicit Arguments On.
Module Quot.
Export Misc.
Export Equiv.
Quotient by a relation |
Parameter quot : (X:Type; Q:(Equivalence X))Type.
Definition quot_fix_universe : (X:TypeQ; Q:(Equivalence X))TypeQ := quot.
Parameter class : (X:Type; Q:(Equivalence X)) X->(quot Q).
Parameter class_surj : (X:Type; Q:(Equivalence X); s:(quot Q))
(ExT [a:X](class Q a)==s).
Parameter class_eq : (X:Type; Q:(Equivalence X); x,y:X)
(Q x y) -> (class Q x)==(class Q y).
Hints Resolve class_eq : quot.
Parameter class_rel : (X:Type; Q:(Equivalence X); x,y:X)
(class Q x)==(class Q y) -> (Q x y).
Hints Resolve class_rel : quot.
Parameter fact : (X:Type; Q:(Equivalence X))
(Y:Type; f:X->Y; H:(Compatible Q f))
(quot Q)->Y.
Implicits fact [1 3].
Parameter fact_comm : (X:Type; Q:(Equivalence X))
(Y:Type; f:X->Y; H:(Compatible Q f))
([a:X](fact Q f H (class Q a)))==f.
Lemma fact_eq : (X:Type; Q:(Equivalence X))
(Y:Type; f:X->Y; H:(Compatible Q f))
(a:X)(fact Q f H (class Q a))==(f a).
Proof.
Intros.
Pattern 2 f.
Rewrite <- (fact_comm H).
Split.
Qed.
Implicits fact_eq [1 3 4].
Hints Resolve fact_eq : quot.
Lemma class_congr : (X:Type; Q:(Equivalence X); a,b:X)
a==b -> (class Q a)==(class Q b).
Proof.
NewInduction 1; Reflexivity.
Qed.
Hints Resolve class_congr : quot.
Tactic Definition Lift x := Elim (class_surj x); NewDestruct 1.
Definition Compatible2 [
X,Y:Type; Q:(Equivalence X); P:(Equivalence Y); Z:Type; f:X->Y->Z
] : Prop := (x1,x2:X; y1,y2:Y)
(Q x1 x2) -> (P y1 y2) -> (f x1 y1)==(f x2 y2).
Section Compatible2.
Variable X,Y:Type; Q:(Equivalence X); P:(Equivalence Y).
Variable Z:Type; f:X->Y->Z.
Lemma compatible_compatible2 : ((y:Y)(Compatible Q [x:X](f x y)))
-> ((x:X)(Compatible P [y:Y](f x y))) -> (Compatible2 Q P f).
Proof.
Unfold Compatible Compatible2; Intros.
Transitivity (f x1 y2); Auto.
Qed.
Lemma compatible_sx : (Compatible2 Q P f)
-> ((y:Y)(Compatible Q [x:X](f x y))).
Proof.
Auto with quot.
Qed.
Lemma compatible_dx : (Compatible2 Q P f)
-> ((x:X)(Compatible P [y:Y](f x y))).
Proof.
Auto with quot.
Qed.
End Compatible2.
Hints Resolve compatible_sx compatible_dx.
Section Fact2.
Variable X,Y:Type; Q:(Equivalence X); P:(Equivalence Y).
Variable Z:Type; f:X->Y->Z.
Hypothesis Hf : (Compatible2 Q P f).
Local g : (quot Q)->Y->Z.
Proof.
Apply (fact Q f).
Abstract Auto with quot.
Defined.
Definition fact2 : (quot Q)->(quot P)->Z.
Proof.
Intro x; Apply (fact P (g x)).
Abstract Lift x; Unfold g; Intros; Rewrite fact_eq; Auto with quot.
Defined.
Lemma fact2_comm :
([x:X; y:Y](fact2 (class Q x) (class P y)))==f.
Proof.
Unfold fact2 g.
Apply nondep_extensionality; Intro x.
Apply nondep_extensionality; Intro y.
Do 2 Rewrite fact_eq; Split.
Qed.
Lemma fact2_eq : (x:X; y:Y)
(fact2 (class Q x) (class P y))==(f x y).
Proof.
Unfold fact2 g; Intros.
Do 2 Rewrite fact_eq; Split.
Qed.
End Fact2.
Section Quot_law.
Variable X:Type; Q:(Equivalence X).
Variable f:X->X; Hf:(Compatible Q [x:X](class Q (f x))).
Local Y := (quot Q).
Definition quot_law : Y->Y := (fact Q ? Hf).
End Quot_law.
Implicits quot_law [1].
Section Quot_law2.
Variable X:Type; Q:(Equivalence X).
Variable f:X->X->X; Hf:(Compatible2 Q Q [x,y:X](class Q (f x y))).
Local Y := (quot Q).
Definition quot_law2 : Y->Y->Y := (fact2 Hf).
End Quot_law2.
Implicits quot_law2 [1].
End Quot.