From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- .../mathcomp.ssreflect.generic_quotient.html | 308 ++++++++++----------- 1 file changed, 153 insertions(+), 155 deletions(-) (limited to 'docs/htmldoc/mathcomp.ssreflect.generic_quotient.html') diff --git a/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html b/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html index 0faf773..f7138b1 100644 --- a/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html +++ b/docs/htmldoc/mathcomp.ssreflect.generic_quotient.html @@ -20,11 +20,7 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
- Distributed under the terms of CeCILL-B.                                  
- -*- coding : utf-8 -*- *)
- -
-Require Import mathcomp.ssreflect.ssreflect.
+ Distributed under the terms of CeCILL-B.                                  *)

@@ -167,9 +163,9 @@
Record quot_mixin_of qT := QuotClass {
-  quot_repr : qT → T;
-  quot_pi : T → qT;
-  _ : cancel quot_repr quot_pi
+  quot_repr : qT → T;
+  quot_pi : T → qT;
+  _ : cancel quot_repr quot_pi
}.

@@ -178,28 +174,26 @@
Record quotType := QuotTypePack {
  quot_sort :> Type;
-  quot_class : quot_class_of quot_sort;
-  _ : Type
+  quot_class : quot_class_of quot_sort
}.
-
-Definition QuotType_pack qT m := @QuotTypePack qT m qT.
-
Variable qT : quotType.
-Definition pi_phant of phant qT := quot_pi (quot_class qT).
+Definition pi_phant of phant qT := quot_pi (quot_class qT).
Definition repr_of := quot_repr (quot_class qT).

-Lemma repr_ofK : cancel repr_of \pi.
+Lemma repr_ofK : cancel repr_of \pi.

Definition QuotType_clone (Q : Type) qT cT
-  of phant_id (quot_class qT) cT := @QuotTypePack Q cT Q.
+  of phant_id (quot_class qT) cT := @QuotTypePack Q cT.

End QuotientDef.
+
+
@@ -210,32 +204,32 @@
Module Type PiSig.
-Parameter f : ∀ (T : Type) (qT : quotType T), phant qT → T → qT.
-Axiom E : f = pi_phant.
+Parameter f : ∀ (T : Type) (qT : quotType T), phant qT → T → qT.
+Axiom E : f = pi_phant.
End PiSig.

Module Pi : PiSig.
Definition f := pi_phant.
-Definition E := erefl f.
+Definition E := erefl f.
End Pi.

Module MPi : PiSig.
Definition f := pi_phant.
-Definition E := erefl f.
+Definition E := erefl f.
End MPi.

Module Type ReprSig.
-Parameter f : ∀ (T : Type) (qT : quotType T), qT → T.
-Axiom E : f = repr_of.
+Parameter f : ∀ (T : Type) (qT : quotType T), qT → T.
+Axiom E : f = repr_of.
End ReprSig.

Module Repr : ReprSig.
Definition f := repr_of.
-Definition E := erefl f.
+Definition E := erefl f.
End Repr.

@@ -248,22 +242,22 @@
Notation repr := Repr.f.
-Notation "\pi_ Q" := (@Pi.f _ _ (Phant Q)) : quotient_scope.
-Notation "\pi" := (@Pi.f _ _ (Phant _)) (only parsing) : quotient_scope.
-Notation "x == y %[mod Q ]" := (\pi_Q x == \pi_Q y) : quotient_scope.
-Notation "x = y %[mod Q ]" := (\pi_Q x = \pi_Q y) : quotient_scope.
-Notation "x != y %[mod Q ]" := (\pi_Q x != \pi_Q y) : quotient_scope.
-Notation "x <> y %[mod Q ]" := (\pi_Q x ≠ \pi_Q y) : quotient_scope.
+Notation "\pi_ Q" := (@Pi.f _ _ (Phant Q)) : quotient_scope.
+Notation "\pi" := (@Pi.f _ _ (Phant _)) (only parsing) : quotient_scope.
+Notation "x == y %[mod Q ]" := (\pi_Q x == \pi_Q y) : quotient_scope.
+Notation "x = y %[mod Q ]" := (\pi_Q x = \pi_Q y) : quotient_scope.
+Notation "x != y %[mod Q ]" := (\pi_Q x != \pi_Q y) : quotient_scope.
+Notation "x <> y %[mod Q ]" := (\pi_Q x ≠ \pi_Q y) : quotient_scope.

-Canonical mpi_unlock := Unlockable MPi.E.
-Canonical pi_unlock := Unlockable Pi.E.
-Canonical repr_unlock := Unlockable Repr.E.
+Canonical mpi_unlock := Unlockable MPi.E.
+Canonical pi_unlock := Unlockable Pi.E.
+Canonical repr_unlock := Unlockable Repr.E.

Notation quot_class_of := quot_mixin_of.
-Notation QuotType Q m := (@QuotType_pack _ Q m).
-Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id)
+Notation QuotType Q m := (@QuotTypePack _ Q m).
+Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id)
 (at level 0, format "[ 'quotType' 'of' Q ]") : form_scope.

@@ -284,28 +278,30 @@ Variable qT : quotType T.

-Lemma reprK : cancel repr \pi_qT.
+Lemma reprK : cancel repr \pi_qT.

-CoInductive pi_spec (x : T) : T → Type :=
-  PiSpec y of x = y %[mod qT] : pi_spec x y.
+Variant pi_spec (x : T) : T → Type :=
+  PiSpec y of x = y %[mod qT] : pi_spec x y.

-Lemma piP (x : T) : pi_spec x (repr (\pi_qT x)).
+Lemma piP (x : T) : pi_spec x (repr (\pi_qT x)).

-Lemma mpiE : \mpi =1 \pi_qT.
+Lemma mpiE : \mpi =1 \pi_qT.

-Lemma quotW P : (∀ y : T, P (\pi_qT y)) → ∀ x : qT, P x.
+Lemma quotW P : (∀ y : T, P (\pi_qT y)) → ∀ x : qT, P x.

-Lemma quotP P : (∀ y : T, repr (\pi_qT y) = y → P (\pi_qT y))
-  → ∀ x : qT, P x.
+Lemma quotP P : (∀ y : T, repr (\pi_qT y) = y → P (\pi_qT y))
+  → ∀ x : qT, P x.

End QuotTypeTheory.
+
+
@@ -318,16 +314,16 @@
Structure equal_to T (x : T) := EqualTo {
   equal_val : T;
-   _ : x = equal_val
+   _ : x = equal_val
}.
-Lemma equal_toE (T : Type) (x : T) (m : equal_to x) : equal_val m = x.
+Lemma equal_toE (T : Type) (x : T) (m : equal_to x) : equal_val m = x.

Notation piE := (@equal_toE _ _).

Canonical equal_to_pi T (qT : quotType T) (x : T) :=
-  @EqualTo _ (\pi_qT x) (\pi x) (erefl _).
+  @EqualTo _ (\pi_qT x) (\pi x) (erefl _).

@@ -340,15 +336,15 @@ Variable (qU : quotType U).

-Variable (f : T → T) (g : T → T → T) (p : T → U) (r : T → T → U).
-Variable (fq : qT → qT) (gq : qT → qT → qT) (pq : qT → U) (rq : qT → qT → U).
-Variable (h : T → U) (hq : qT → qU).
-Hypothesis pi_f : {morph \pi : x / f x >-> fq x}.
-Hypothesis pi_g : {morph \pi : x y / g x y >-> gq x y}.
-Hypothesis pi_p : {mono \pi : x / p x >-> pq x}.
-Hypothesis pi_r : {mono \pi : x y / r x y >-> rq x y}.
-Hypothesis pi_h : ∀ (x : T), \pi_qU (h x) = hq (\pi_qT x).
-Variables (a b : T) (x : equal_to (\pi_qT a)) (y : equal_to (\pi_qT b)).
+Variable (f : T → T) (g : T → T → T) (p : T → U) (r : T → T → U).
+Variable (fq : qT → qT) (gq : qT → qT → qT) (pq : qT → U) (rq : qT → qT → U).
+Variable (h : T → U) (hq : qT → qU).
+Hypothesis pi_f : {morph \pi : x / f x >-> fq x}.
+Hypothesis pi_g : {morph \pi : x y / g x y >-> gq x y}.
+Hypothesis pi_p : {mono \pi : x / p x >-> pq x}.
+Hypothesis pi_r : {mono \pi : x y / r x y >-> rq x y}.
+Hypothesis pi_h : ∀ (x : T), \pi_qU (h x) = hq (\pi_qT x).
+Variables (a b : T) (x : equal_to (\pi_qT a)) (y : equal_to (\pi_qT b)).

@@ -357,11 +353,11 @@ Internal Lemmmas : do not use directly
-Lemma pi_morph1 : \pi (f a) = fq (equal_val x).
-Lemma pi_morph2 : \pi (g a b) = gq (equal_val x) (equal_val y).
-Lemma pi_mono1 : p a = pq (equal_val x).
-Lemma pi_mono2 : r a b = rq (equal_val x) (equal_val y).
-Lemma pi_morph11 : \pi (h a) = hq (equal_val x).
+Lemma pi_morph1 : \pi (f a) = fq (equal_val x).
+Lemma pi_morph2 : \pi (g a b) = gq (equal_val x) (equal_val y).
+Lemma pi_mono1 : p a = pq (equal_val x).
+Lemma pi_mono2 : r a b = rq (equal_val x) (equal_val y).
+Lemma pi_morph11 : \pi (h a) = hq (equal_val x).

End Morphism.
@@ -369,8 +365,8 @@

-Notation "{pi_ Q a }" := (equal_to (\pi_Q a)) : quotient_scope.
-Notation "{pi a }" := (equal_to (\pi a)) : quotient_scope.
+Notation "{pi_ Q a }" := (equal_to (\pi_Q a)) : quotient_scope.
+Notation "{pi a }" := (equal_to (\pi a)) : quotient_scope.

@@ -381,15 +377,15 @@
Notation PiMorph pi_x := (EqualTo pi_x).
Notation PiMorph1 pi_f :=
-  (fun a (x : {pi a}) ⇒ EqualTo (pi_morph1 pi_f a x)).
+  (fun a (x : {pi a}) ⇒ EqualTo (pi_morph1 pi_f a x)).
Notation PiMorph2 pi_g :=
-  (fun a b (x : {pi a}) (y : {pi b}) ⇒ EqualTo (pi_morph2 pi_g a b x y)).
+  (fun a b (x : {pi a}) (y : {pi b}) ⇒ EqualTo (pi_morph2 pi_g a b x y)).
Notation PiMono1 pi_p :=
-  (fun a (x : {pi a}) ⇒ EqualTo (pi_mono1 pi_p a x)).
+  (fun a (x : {pi a}) ⇒ EqualTo (pi_mono1 pi_p a x)).
Notation PiMono2 pi_r :=
-  (fun a b (x : {pi a}) (y : {pi b}) ⇒ EqualTo (pi_mono2 pi_r a b x y)).
+  (fun a b (x : {pi a}) (y : {pi b}) ⇒ EqualTo (pi_mono2 pi_r a b x y)).
Notation PiMorph11 pi_f :=
-  (fun a (x : {pi a}) ⇒ EqualTo (pi_morph11 pi_f a x)).
+  (fun a (x : {pi a}) ⇒ EqualTo (pi_morph11 pi_f a x)).

@@ -398,12 +394,12 @@ lifiting helpers
-Notation lift_op1 Q f := (locked (fun x : Q ⇒ \pi_Q (f (repr x)) : Q)).
+Notation lift_op1 Q f := (locked (fun x : Q ⇒ \pi_Q (f (repr x)) : Q)).
Notation lift_op2 Q g :=
-  (locked (fun x y : Q ⇒ \pi_Q (g (repr x) (repr y)) : Q)).
-Notation lift_fun1 Q f := (locked (fun x : Q ⇒ f (repr x))).
-Notation lift_fun2 Q g := (locked (fun x y : Q ⇒ g (repr x) (repr y))).
-Notation lift_op11 Q Q' f := (locked (fun x : Q ⇒ \pi_Q' (f (repr x)) : Q')).
+  (locked (fun x y : Q ⇒ \pi_Q (g (repr x) (repr y)) : Q)).
+Notation lift_fun1 Q f := (locked (fun x : Q ⇒ f (repr x))).
+Notation lift_fun2 Q g := (locked (fun x y : Q ⇒ g (repr x) (repr y))).
+Notation lift_op11 Q Q' f := (locked (fun x : Q ⇒ \pi_Q' (f (repr x)) : Q')).

@@ -412,8 +408,8 @@ constant declaration
-Notation lift_cst Q x := (locked (\pi_Q x : Q)).
-Notation PiConst a := (@EqualTo _ _ a (lock _)).
+Notation lift_cst Q x := (locked (\pi_Q x : Q)).
+Notation PiConst a := (@EqualTo _ _ a (lock _)).

@@ -422,14 +418,14 @@ embedding declaration, please don't redefine \pi
-Notation lift_embed qT e := (locked (fun x ⇒ \pi_qT (e x) : qT)).
+Notation lift_embed qT e := (locked (fun x ⇒ \pi_qT (e x) : qT)).

-Lemma eq_lock T T' e : e =1 (@locked (T → T') (fun x : T ⇒ e x)).
+Lemma eq_lock T T' e : e =1 (@locked (T → T') (fun x : T ⇒ e x)).

Notation PiEmbed e :=
-  (fun x ⇒ @EqualTo _ _ (e x) (eq_lock (fun _ ⇒ \pi _) _)).
+  (fun x ⇒ @EqualTo _ _ (e x) (eq_lock (fun _ ⇒ \pi _) _)).

@@ -444,13 +440,13 @@
Variable T : Type.
-Variable eq_quot_op : rel T.
+Variable eq_quot_op : rel T.

Definition eq_quot_mixin_of (Q : Type) (qc : quot_class_of T Q)
  (ec : Equality.class_of Q) :=
-  {mono \pi_(QuotTypePack qc Q) : x y /
-   eq_quot_op x y >-> @eq_op (Equality.Pack ec Q) x y}.
+  {mono \pi_(QuotTypePack qc) : x y /
+   eq_quot_op x y >-> @eq_op (Equality.Pack ec) x y}.

Record eq_quot_class_of (Q : Type) : Type := EqQuotClass {
@@ -463,7 +459,7 @@ Record eqQuotType : Type := EqQuotTypePack {
  eq_quot_sort :> Type;
  _ : eq_quot_class_of eq_quot_sort;
-  _ : Type
+ 
}.

@@ -471,7 +467,7 @@
Definition eq_quot_class eqT : eq_quot_class_of eqT :=
-  let: EqQuotTypePack _ cT _ as qT' := eqT return eq_quot_class_of qT' in cT.
+  let: EqQuotTypePack _ cT as qT' := eqT return eq_quot_class_of qT' in cT.

Canonical eqQuotType_eqType eqT := EqType eqT (eq_quot_class eqT).
@@ -484,15 +480,15 @@
Definition EqQuotType_pack Q :=
  fun (qT : quotType T) (eT : eqType) qc ec
-  of phant_id (quot_class qT) qc & phant_id (Equality.class eT) ec ⇒
-    fun m ⇒ EqQuotTypePack (@EqQuotClass Q qc ec m) Q.
+  of phant_id (quot_class qT) qc & phant_id (Equality.class eT) ec ⇒
+    fun m ⇒ EqQuotTypePack (@EqQuotClass Q qc ec m).

Definition EqQuotType_clone (Q : Type) eqT cT
-  of phant_id (eq_quot_class eqT) cT := @EqQuotTypePack Q cT Q.
+  of phant_id (eq_quot_class eqT) cT := @EqQuotTypePack Q cT.

-Lemma pi_eq_quot eqT : {mono \pi_eqT : x y / eq_quot_op x y >-> x == y}.
+Lemma pi_eq_quot eqT : {mono \pi_eqT : x y / eq_quot_op x y >-> x == y}.

Canonical pi_eq_quot_mono eqT := PiMono2 (pi_eq_quot eqT).
@@ -501,8 +497,8 @@ End EqQuotTypeStructure.

-Notation EqQuotType e Q m := (@EqQuotType_pack _ e Q _ _ _ _ id id m).
-Notation "[ 'eqQuotType' e 'of' Q ]" := (@EqQuotType_clone _ e Q _ _ id)
+Notation EqQuotType e Q m := (@EqQuotType_pack _ e Q _ _ _ _ id id m).
+Notation "[ 'eqQuotType' e 'of' Q ]" := (@EqQuotType_clone _ e Q _ _ id)
 (at level 0, format "[ 'eqQuotType' e 'of' Q ]") : form_scope.

@@ -532,23 +528,23 @@ Variable qT : quotType T.

-Definition Sub x (px : repr (\pi_qT x) == x) := \pi_qT x.
+Definition Sub x (px : repr (\pi_qT x) == x) := \pi_qT x.

-Lemma qreprK x Px : repr (@Sub x Px) = x.
+Lemma qreprK x Px : repr (@Sub x Px) = x.

-Lemma sortPx (x : qT) : repr (\pi_qT (repr x)) == repr x.
+Lemma sortPx (x : qT) : repr (\pi_qT (repr x)) == repr x.

-Lemma sort_Sub (x : qT) : x = Sub (sortPx x).
+Lemma sort_Sub (x : qT) : x = Sub (sortPx x).

Lemma reprP K (PK : ∀ x Px, K (@Sub x Px)) u : K u.

Canonical subType := SubType _ _ _ reprP qreprK.
-Definition eqMixin := Eval hnf in [eqMixin of qT by <:].
+Definition eqMixin := Eval hnf in [eqMixin of qT by <:].

Canonical eqType := EqType qT eqMixin.
@@ -558,49 +554,49 @@
Definition choiceMixin (T : choiceType) (qT : quotType T) :=
-  Eval hnf in [choiceMixin of qT by <:].
+  Eval hnf in [choiceMixin of qT by <:].
Canonical choiceType (T : choiceType) (qT : quotType T) :=
  ChoiceType qT (@choiceMixin T qT).

Definition countMixin (T : countType) (qT : quotType T) :=
-  Eval hnf in [countMixin of qT by <:].
+  Eval hnf in [countMixin of qT by <:].
Canonical countType (T : countType) (qT : quotType T) :=
  CountType qT (@countMixin T qT).

Section finType.
Variables (T : finType) (qT : quotType T).
-Canonical subCountType := [subCountType of qT].
-Definition finMixin := Eval hnf in [finMixin of qT by <:].
+Canonical subCountType := [subCountType of qT].
+Definition finMixin := Eval hnf in [finMixin of qT by <:].
End finType.

End QuotSubType.

-Notation "[ 'subType' Q 'of' T 'by' %/ ]" :=
+Notation "[ 'subType' Q 'of' T 'by' %/ ]" :=
(@SubType T _ Q _ _ (@QuotSubType.reprP _ _) (@QuotSubType.qreprK _ _))
(at level 0, format "[ 'subType' Q 'of' T 'by' %/ ]") : form_scope.

-Notation "[ 'eqMixin' 'of' Q 'by' <:%/ ]" :=
-  (@QuotSubType.eqMixin _ _: Equality.class_of Q)
+Notation "[ 'eqMixin' 'of' Q 'by' <:%/ ]" :=
+  (@QuotSubType.eqMixin _ _: Equality.class_of Q)
  (at level 0, format "[ 'eqMixin' 'of' Q 'by' <:%/ ]") : form_scope.

-Notation "[ 'choiceMixin' 'of' Q 'by' <:%/ ]" :=
-  (@QuotSubType.choiceMixin _ _: Choice.mixin_of Q)
+Notation "[ 'choiceMixin' 'of' Q 'by' <:%/ ]" :=
+  (@QuotSubType.choiceMixin _ _: Choice.mixin_of Q)
  (at level 0, format "[ 'choiceMixin' 'of' Q 'by' <:%/ ]") : form_scope.

-Notation "[ 'countMixin' 'of' Q 'by' <:%/ ]" :=
-  (@QuotSubType.countMixin _ _: Countable.mixin_of Q)
+Notation "[ 'countMixin' 'of' Q 'by' <:%/ ]" :=
+  (@QuotSubType.countMixin _ _: Countable.mixin_of Q)
  (at level 0, format "[ 'countMixin' 'of' Q 'by' <:%/ ]") : form_scope.

-Notation "[ 'finMixin' 'of' Q 'by' <:%/ ]" :=
-  (@QuotSubType.finMixin _ _: Finite.mixin_of Q)
+Notation "[ 'finMixin' 'of' Q 'by' <:%/ ]" :=
+  (@QuotSubType.finMixin _ _: Finite.mixin_of Q)
  (at level 0, format "[ 'finMixin' 'of' Q 'by' <:%/ ]") : form_scope.

@@ -618,20 +614,20 @@ Variable T : Type.

-Lemma left_trans (e : rel T) :
-  symmetric e → transitive e → left_transitive e.
+Lemma left_trans (e : rel T) :
+  symmetric e → transitive e → left_transitive e.

-Lemma right_trans (e : rel T) :
-  symmetric e → transitive e → right_transitive e.
+Lemma right_trans (e : rel T) :
+  symmetric e → transitive e → right_transitive e.

-CoInductive equiv_class_of (equiv : rel T) :=
-  EquivClass of reflexive equiv & symmetric equiv & transitive equiv.
+Variant equiv_class_of (equiv : rel T) :=
+  EquivClass of reflexive equiv & symmetric equiv & transitive equiv.

Record equiv_rel := EquivRelPack {
-  equiv :> rel T;
+  equiv :> rel T;
  _ : equiv_class_of equiv
}.
@@ -643,32 +639,32 @@   let: EquivRelPack _ ce as e' := e return equiv_class_of e' in ce.

-Definition equiv_pack (r : rel T) ce of phant_id ce equiv_class :=
+Definition equiv_pack (r : rel T) ce of phant_id ce equiv_class :=
  @EquivRelPack r ce.

Lemma equiv_refl x : e x x.
-Lemma equiv_sym : symmetric e.
-Lemma equiv_trans : transitive e.
+Lemma equiv_sym : symmetric e.
+Lemma equiv_trans : transitive e.

-Lemma eq_op_trans (T' : eqType) : transitive (@eq_op T').
+Lemma eq_op_trans (T' : eqType) : transitive (@eq_op T').

-Lemma equiv_ltrans: left_transitive e.
+Lemma equiv_ltrans: left_transitive e.

-Lemma equiv_rtrans: right_transitive e.
+Lemma equiv_rtrans: right_transitive e.

End EquivRel.

-Hint Resolve equiv_refl.
+Hint Resolve equiv_refl : core.

Notation EquivRel r er es et := (@EquivRelPack _ r (EquivClass er es et)).
-Notation "[ 'equiv_rel' 'of' e ]" := (@equiv_pack _ _ e _ id)
+Notation "[ 'equiv_rel' 'of' e ]" := (@equiv_pack _ _ e _ id)
 (at level 0, format "[ 'equiv_rel' 'of' e ]") : form_scope.

@@ -683,15 +679,15 @@ Section EncodingModuloRel.

-Variables (D E : Type) (ED : E → D) (DE : D → E) (e : rel D).
+Variables (D E : Type) (ED : E → D) (DE : D → E) (e : rel D).

-CoInductive encModRel_class_of (r : rel D) :=
-  EncModRelClassPack of (∀ x, r x x → r (ED (DE x)) x) & (r =2 e).
+Variant encModRel_class_of (r : rel D) :=
+  EncModRelClassPack of (∀ x, r x x → r (ED (DE x)) x) & (r =2 e).

Record encModRel := EncModRelPack {
-  enc_mod_rel :> rel D;
+  enc_mod_rel :> rel D;
  _ : encModRel_class_of enc_mod_rel
}.
@@ -703,27 +699,27 @@   let: EncModRelPack _ c as r' := r return encModRel_class_of r' in c.

-Definition encModRelP (x : D) : r x x → r (ED (DE x)) x.
+Definition encModRelP (x : D) : r x x → r (ED (DE x)) x.

-Definition encModRelE : r =2 e.
+Definition encModRelE : r =2 e.

-Definition encoded_equiv : rel E := [rel x y | r (ED x) (ED y)].
+Definition encoded_equiv : rel E := [rel x y | r (ED x) (ED y)].

End EncodingModuloRel.

Notation EncModRelClass m :=
-  (EncModRelClassPack (fun x _ ⇒ m x) (fun _ _ ⇒ erefl _)).
+  (EncModRelClassPack (fun x _ ⇒ m x) (fun _ _ ⇒ erefl _)).
Notation EncModRel r m := (@EncModRelPack _ _ _ _ _ r (EncModRelClass m)).

Section EncodingModuloEquiv.

-Variables (D E : Type) (ED : E → D) (DE : D → E) (e : equiv_rel D).
+Variables (D E : Type) (ED : E → D) (DE : D → E) (e : equiv_rel D).
Variable (r : encModRel ED DE e).

@@ -738,7 +734,7 @@

-Lemma encoded_equivE : e' =2 [rel x y | e (ED x) (ED y)].
+Lemma encoded_equivE : e' =2 [rel x y | e (ED x) (ED y)].

Lemma encoded_equiv_is_equiv : equiv_class_of e'.
@@ -765,7 +761,7 @@ Section EquivQuot.

-Variables (D : Type) (C : choiceType) (CD : C → D) (DC : D → C).
+Variables (D : Type) (C : choiceType) (CD : C → D) (DC : D → C).
Variables (eD : equiv_rel D) (encD : encModRel CD DC eD).
Notation eC := (encoded_equiv encD).
@@ -779,36 +775,36 @@ }.

-Definition type_of of (phantom (rel _) encD) := equivQuotient.
+Definition type_of of (phantom (rel _) encD) := equivQuotient.

Lemma canon_id : ∀ x, (invariant canon canon) x.

-Definition pi := locked (fun x ⇒ EquivQuotient (canon_id x)).
+Definition pi := locked (fun x ⇒ EquivQuotient (canon_id x)).

-Lemma ereprK : cancel erepr pi.
+Lemma ereprK : cancel erepr pi.

Canonical encD_equiv_rel := EquivRelPack (enc_mod_rel_is_equiv encD).

-Lemma pi_CD (x y : C) : reflect (pi x = pi y) (eC x y).
+Lemma pi_CD (x y : C) : reflect (pi x = pi y) (eC x y).

Lemma pi_DC (x y : D) :
-  reflect (pi (DC x) = pi (DC y)) (eD x y).
+  reflect (pi (DC x) = pi (DC y)) (eD x y).

-Lemma equivQTP : cancel (CD \o erepr) (pi \o DC).
+Lemma equivQTP : cancel (CD \o erepr) (pi \o DC).

Definition quotClass := QuotClass equivQTP.
Canonical quotType := QuotType qT quotClass.

-Lemma eqmodP x y : reflect (x = y %[mod qT]) (eD x y).
+Lemma eqmodP x y : reflect (x = y %[mod qT]) (eD x y).

Fact eqMixin : Equality.mixin_of qT.
@@ -817,7 +813,7 @@ Canonical choiceType := ChoiceType qT choiceMixin.

-Lemma eqmodE x y : x == y %[mod qT] = eD x y.
+Lemma eqmodE x y : x == y %[mod qT] = eD x y.

Canonical eqQuotType := EqQuotType eD qT eqmodE.
@@ -833,12 +829,14 @@ Canonical EquivQuot.eqQuotType.

-Notation "{eq_quot e }" :=
-(@EquivQuot.type_of _ _ _ _ _ _ (Phantom (rel _) e)) : quotient_scope.
-Notation "x == y %[mod_eq r ]" := (x == y %[mod {eq_quot r}]) : quotient_scope.
-Notation "x = y %[mod_eq r ]" := (x = y %[mod {eq_quot r}]) : quotient_scope.
-Notation "x != y %[mod_eq r ]" := (x != y %[mod {eq_quot r}]) : quotient_scope.
-Notation "x <> y %[mod_eq r ]" := (x ≠ y %[mod {eq_quot r}]) : quotient_scope.
+ +
+Notation "{eq_quot e }" :=
+(@EquivQuot.type_of _ _ _ _ _ _ (Phantom (rel _) e)) : quotient_scope.
+Notation "x == y %[mod_eq r ]" := (x == y %[mod {eq_quot r}]) : quotient_scope.
+Notation "x = y %[mod_eq r ]" := (x = y %[mod {eq_quot r}]) : quotient_scope.
+Notation "x != y %[mod_eq r ]" := (x != y %[mod {eq_quot r}]) : quotient_scope.
+Notation "x <> y %[mod_eq r ]" := (x ≠ y %[mod {eq_quot r}]) : quotient_scope.

@@ -852,11 +850,11 @@ Section DefaultEncodingModuloRel.

-Variables (D : choiceType) (r : rel D).
+Variables (D : choiceType) (r : rel D).

Definition defaultEncModRelClass :=
-  @EncModRelClassPack D D id id r r (fun _ rxx ⇒ rxx) (fun _ _ ⇒ erefl _).
+  @EncModRelClassPack D D id id r r (fun _ rxx ⇒ rxx) (fun _ _ ⇒ erefl _).

Canonical defaultEncModRel := EncModRelPack defaultEncModRelClass.
@@ -876,13 +874,13 @@ Section CountEncodingModuloRel.

-Variables (D : Type) (C : countType) (CD : C → D) (DC : D → C).
+Variables (D : Type) (C : countType) (CD : C → D) (DC : D → C).
Variables (eD : equiv_rel D) (encD : encModRel CD DC eD).
Notation eC := (encoded_equiv encD).

-Fact eq_quot_countMixin : Countable.mixin_of {eq_quot encD}.
- Canonical eq_quot_countType := CountType {eq_quot encD} eq_quot_countMixin.
+Fact eq_quot_countMixin : Countable.mixin_of {eq_quot encD}.
+ Canonical eq_quot_countType := CountType {eq_quot encD} eq_quot_countMixin.

End CountEncodingModuloRel.
@@ -894,10 +892,10 @@ Variables (T : choiceType) (e : equiv_rel T) (Q : eqQuotType e).

-Lemma eqmodE x y : x == y %[mod_eq e] = e x y.
+Lemma eqmodE x y : x == y %[mod_eq e] = e x y.

-Lemma eqmodP x y : reflect (x = y %[mod_eq e]) (e x y).
+Lemma eqmodP x y : reflect (x = y %[mod_eq e]) (e x y).

End EquivQuotTheory.
@@ -908,13 +906,13 @@ Section EqQuotTheory.

-Variables (T : Type) (e : rel T) (Q : eqQuotType e).
+Variables (T : Type) (e : rel T) (Q : eqQuotType e).

-Lemma eqquotE x y : x == y %[mod Q] = e x y.
+Lemma eqquotE x y : x == y %[mod Q] = e x y.

-Lemma eqquotP x y : reflect (x = y %[mod Q]) (e x y).
+Lemma eqquotP x y : reflect (x = y %[mod Q]) (e x y).

End EqQuotTheory.
-- cgit v1.2.3