Use quotient notation A / R

peterlefanulumsdaine · May 19, 2021 · 65ed8c8 · 65ed8c8
1 parent ffaf917
commit 65ed8c8
Showing 1 changed file with 26 additions and 27 deletions.
diff --git a/theories/Colimits/Quotient/Choice.v b/theories/Colimits/Quotient/Choice.v
@@ -7,7 +7,7 @@ Require Import
   HoTT.Colimits.Quotient
   HoTT.Projective.
 
-(** The following is an alternative (0,-1)-projective predicate. Given a family of quotient sets [forall x : A, quotient (R x)], for [R : forall x : A, Relation (B x)], we merely have a choice function [g : forall x, B x], such that [class_of (g x) = f x]. *)
+(** The following is an alternative (0,-1)-projective predicate. Given a family of quotient sets [forall x : A, B x / R x], for [R : forall x : A, Relation (B x)], we merely have a choice function [g : forall x, B x], such that [class_of (g x) = f x]. *)
 
 Definition IsQuotientChoosable (A : Type) :=
   forall (B : A -> Type), (forall x, IsHSet (B x)) ->
@@ -16,7 +16,7 @@ Definition IsQuotientChoosable (A : Type) :=
          (forall x, Reflexive (R x)) ->
          (forall x, Symmetric (R x)) ->
          (forall x, Transitive (R x)) ->
-  forall (f : forall x : A, Quotient (R x)),
+  forall (f : forall x : A, B x / (R x)),
   hexists (fun g : (forall x : A, B x) =>
                    forall x, class_of (R x) (g x) = f x).
 
@@ -47,7 +47,7 @@ Section choose_isquotientchoosable.
   Qed.
 
   Local Instance hprop_choose_cod (a : A)
-    : IsHProp {c : Quotient (RelClassEquiv a)
+    : IsHProp {c : B a / RelClassEquiv a
                  | forall b, in_class (RelClassEquiv a) c b <~> P a b}.
   Proof.
     apply ishprop_sigma_disjoint.
@@ -62,7 +62,7 @@ Section choose_isquotientchoosable.
   Qed.
 
   Local Definition prechoose (i : forall x, hexists (P x)) (a : A)
-    : {c : Quotient (RelClassEquiv a)
+    : {c : B a / RelClassEquiv a
          | forall b : B a, in_class (RelClassEquiv a) c b <~> P a b}.
   Proof.
     specialize (i a).
@@ -76,7 +76,7 @@ Section choose_isquotientchoosable.
   Defined.
 
   Local Definition choose (i : forall x, hexists (P x)) (a : A)
-    : Quotient (RelClassEquiv a)
+    : B a / RelClassEquiv a
     := (prechoose i a).1.
 
 End choose_isquotientchoosable.
@@ -108,7 +108,7 @@ Section isquotientchoosable_to_istr0choosable.
   Qed.
 
   Local Instance ishprop_quotient_relunit (B : A -> Type) (a : A)
-    : IsHProp (Quotient (RelUnit B a)).
+    : IsHProp (B a / RelUnit B a).
   Proof.
     apply hprop_allpath.
     refine (Quotient_ind_hprop _ _ _).
@@ -121,7 +121,7 @@ Section isquotientchoosable_to_istr0choosable.
   Lemma isquotientchoosable_to_istr0choosable : IsTrChoosable 0 A.
   Proof.
     intros B sB f.
-    transparent assert (g : (forall a, Quotient (RelUnit B a))).
+    transparent assert (g : (forall a, B a / RelUnit B a)).
     - intro a.
       specialize (f a).
       strip_truncations.
@@ -181,7 +181,7 @@ Section choose_quotient_ind.
 
 (** First generalize the [qglue] constructor. *)
 
-  Lemma pointwise_qglue
+  Lemma qglue_forall
     (f g : forall i, A i) (r : forall i, R i (f i) (g i))
     : (fun i => class_of (R i) (f i)) = (fun i => class_of (R i) (g i)).
   Proof.
@@ -192,21 +192,21 @@ Section choose_quotient_ind.
 (** Given suitable preconditions, we will show that [ChooseProp P a g] is inhabited, rather than directly showing [P q]. This turns out to be beneficial because [ChooseProp P a g] is a proposition. *)
 
   Local Definition ChooseProp
-    (P : (forall i, Quotient (R i)) -> Type) `{!forall g, IsHSet (P g)}
+    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
     (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
-    (g : forall i, Quotient (R i))
+    (g : forall i, A i / R i)
     : Type
     := {b : P g
        | merely (exists (f : forall i, A i)
                         (q : g = fun i => class_of (R i) (f i)),
                  forall (f' : forall i, A i)
                         (r : forall i, R i (f i) (f' i)),
-                 pointwise_qglue f f' r # q # b = a f')}.
+                 qglue_forall f f' r # q # b = a f')}.
 
   Local Instance ishprop_choose_quotient_ind_chooseprop
-    (P : (forall i, Quotient (R i)) -> Type) `{!forall g, IsHSet (P g)}
+    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
     (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
-    (g : forall i, Quotient (R i))
+    (g : forall i, A i / R i)
     : IsHProp (ChooseProp P a g).
   Proof.
     apply ishprop_sigma_disjoint.
@@ -228,20 +228,19 @@ Section choose_quotient_ind.
     apply moveR_transport_p.
     rewrite inv_V.
     do 2 rewrite <- transport_pp.
-    set (pa := (pointwise_qglue f2 f1 pR)^
-               @ (q2^ @ q1
-               @ pointwise_qglue f1 f1 _)).
+    set (pa := (qglue_forall f2 f1 pR)^
+               @ (q2^ @ q1 @ qglue_forall f1 f1 _)).
     by induction (hset_path2 idpath pa).
   Qed.
 
 (* Since [ChooseProp P a g] is a proposition, we can apply [istr0choosable_to_isquotientchoosable] and strip its truncation in order to derive [ChooseProp P a g]. *)
 
   Lemma chooseprop_quotient_ind
-    (P : (forall i, Quotient (R i)) -> Type) `{!forall g, IsHSet (P g)}
+    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
     (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
     (E : forall (f f' : forall i, A i) (r : forall i, R i (f i) (f' i)),
-         pointwise_qglue f f' r # a f = a f')
-    (g : forall i, Quotient (R i))
+         qglue_forall f f' r # a f = a f')
+    (g : forall i, A i / R i)
     : ChooseProp P a g.
   Proof.
     pose proof
@@ -260,11 +259,11 @@ Section choose_quotient_ind.
 (** By projecting out of [chooseprop_quotient_ind] we obtain a generalization of [quotient_rec2]. *)
 
   Lemma choose_quotient_ind
-    (P : (forall i, Quotient (R i)) -> Type) `{!forall g, IsHSet (P g)}
+    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
     (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
     (E : forall (f f' : forall i, A i) (r : forall i, R i (f i) (f' i)),
-         pointwise_qglue f f' r # a f = a f')
-    (g : forall i, Quotient (R i))
+         qglue_forall f f' r # a f = a f')
+    (g : forall i, A i / R i)
     : P g.
   Proof.
     exact (chooseprop_quotient_ind P a E g).1.
@@ -273,9 +272,9 @@ Section choose_quotient_ind.
 (** A specialization of [choose_quotient_ind] to the case where [P g] is a proposition. *)
 
   Lemma choose_quotient_ind_prop
-    (P : (forall i, Quotient (R i)) -> Type) `{!forall g, IsHProp (P g)}
+    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHProp (P g)}
     (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
-    (g : forall i, Quotient (R i))
+    (g : forall i, A i / R i)
     : P g.
   Proof.
     refine (choose_quotient_ind P a _ g). intros. apply path_ishprop.
@@ -287,18 +286,18 @@ Section choose_quotient_ind.
     {B : Type} `{!IsHSet B} (a : (forall i, A i) -> B)
     (E : forall (f f' : forall i, A i),
          (forall i, R i (f i) (f' i)) -> a f = a f')
-    (g : forall i, Quotient (R i))
+    (g : forall i, A i / R i)
     : B
     := choose_quotient_ind (fun _ => B) a
         (fun f f' r => transport_const _ _ @ E f f' r) g.
 
 (** The "beta-rule" of [choose_quotient_ind]. *)
 
   Lemma choose_quotient_ind_compute
-    (P : (forall i, Quotient (R i)) -> Type) `{!forall g, IsHSet (P g)}
+    (P : (forall i, A i / R i) -> Type) `{!forall g, IsHSet (P g)}
     (a : forall (f : forall i, A i), P (fun i => class_of (R i) (f i)))
     (E : forall (f f' : forall i, A i) (r : forall i, R i (f i) (f' i)),
-         pointwise_qglue f f' r # a f = a f')
+         qglue_forall f f' r # a f = a f')
     (f : forall i, A i)
     : choose_quotient_ind P a E (fun i => class_of (R i) (f i)) = a f.
   Proof.