more general quotients

theories/topology.v

@@ -4614,16 +4614,16 @@ End fct_PseudoMetric.
 
 Section quotients. 
 Local Open Scope quotient_scope.
-Context {T : topologicalType} {R : equiv_rel T}.
+Context {T : topologicalType} {Q : quotType T}.
 
-Canonical quotient_eq := EqType {eq_quot R} gen_eqMixin.
-Canonical quotient_choice := ChoiceType {eq_quot R} gen_choiceMixin.
-Canonical quotient_pointed := PointedType {eq_quot R} (\pi_{eq_quot R} point).
+Canonical quotient_eq := EqType Q gen_eqMixin.
+Canonical quotient_choice := ChoiceType Q gen_choiceMixin.
+Canonical quotient_pointed := PointedType Q (\pi_Q point).
 
-Definition quotient_open (U : set {eq_quot R}) := open (\pi_{eq_quot R}@^-1` U).
+Definition quotient_open (U : set Q) := open (\pi_Q@^-1` U).
 
 Program Definition quotient_topologicalType_mixin := 
-  @topologyOfOpenMixin {eq_quot R} quotient_open _ _ _.
+  @topologyOfOpenMixin Q quotient_open _ _ _.
 
 Next Obligation. by rewrite /quotient_open preimage_setT; exact: openT. Qed.
 Next Obligation. by move=> ? ? ? ?; exact: openI. Qed.
@@ -4632,30 +4632,30 @@ Next Obligation. by move=> I f ofi; apply: bigcup_open => i _; exact: ofi. Qed.
 Let quotient_filtered := Filtered.Class (Pointed.class quotient_pointed) 
   (nbhs_of_open quotient_open).
 
-Canonical quotient_topologicalType := @Topological.Pack {eq_quot R}
+Canonical quotient_topologicalType := @Topological.Pack Q
   (@Topological.Class _ quotient_filtered quotient_topologicalType_mixin).
 
-Let Q := quotient_topologicalType.
+Let Q' := quotient_topologicalType.
 
-Lemma pi_continuous : continuous (\pi_Q : T -> Q).
+Lemma pi_continuous : continuous (\pi_Q : T -> Q').
 Proof. exact/continuousP. Qed.
 
-Lemma quotient_continuous {Z : topologicalType} (f : Q -> Z) :
-  continuous f <-> continuous (f \o \pi_{eq_quot R}).
+Lemma quotient_continuous {Z : topologicalType} (f : Q' -> Z) :
+  continuous f <-> continuous (f \o \pi_Q).
 Proof.
 split => /continuousP /= cts; apply/continuousP => A oA.
   by rewrite comp_preimage; move/continuousP: pi_continuous; apply; exact: cts.
 by have := cts _ oA.
 Qed.
 
 Lemma repr_comp_continuous (Z : topologicalType) (g : T -> Z) :
-  continuous g -> {homo g : a b / R a b >-> a = b} -> 
-  continuous (g \o repr : Q -> Z).
+  continuous g -> {homo g : a b / a == b %[mod Q] >-> a == b} -> 
+  continuous (g \o repr : Q' -> Z).
 Proof.
 move=> /continuousP ctsG rgE; apply/continuousP => A oA.
 rewrite /open /= /quotient_open comp_preimage; have := ctsG _ oA.
-have greprE : forall x, g (repr (\pi_{eq_quot R} x)) = g x.
-  by move=> x; apply: rgE; rewrite -eqmodE reprK.
+have greprE : forall x, g (repr (\pi_Q x)) = g x.
+  by move=> x; apply/eqP; apply: rgE; rewrite reprK.
 by congr (open _); rewrite eqEsubset; split => x; rewrite /= greprE.
 Qed.