From 7cb257c495f0864179b91597a34ddf26bd93cefa Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 6 Nov 2024 20:58:27 -0500
Subject: [PATCH 1/6] Fix comments and indentation

---
 theories/Algebra/Rings/Ideal.v |  2 +-
 theories/Truncations/Core.v    | 24 ++++++++++++------------
 theories/Types/Empty.v         | 11 ++++-------
 3 files changed, 17 insertions(+), 20 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index 827ca182ab..5bbc244db8 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -456,7 +456,7 @@ Proof.
     nrapply igt_mul_r.
 Defined. 
 
-(** *** Finitely gnerated ideal. *)
+(** *** Finitely generated ideal *)
 
 (** Finitely generated ideals *)
 Definition ideal_generated_finite {R : Ring} {n : nat} (X : Fin n -> R) : Ideal R.
diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
index de019b590a..995be86c6c 100644
--- a/theories/Truncations/Core.v
+++ b/theories/Truncations/Core.v
@@ -1,9 +1,9 @@
 Require Import Basics Types WildCat.Core WildCat.Universe HFiber.
 Require Import Modalities.Modality.
-(* Users of this file almost always want to be able to write [Tr n] for both a [Modality] and a [ReflectiveSubuniverse], so they want the coercion [modality_to_reflective_subuniverse]: *)
+(** Users of this file almost always want to be able to write [Tr n] for both a [Modality] and a [ReflectiveSubuniverse], so they want the coercion [modality_to_reflective_subuniverse]: *)
 Require Export (coercions) Modalities.Modality.
 
-(** * Truncations of types, in all dimensions *)
+(** * Truncations of types *)
 
 Local Open Scope path_scope.
 Generalizable Variables A X n.
@@ -12,7 +12,7 @@ Generalizable Variables A X n.
 
 (** The definition of [Trunc n], the n-truncation of a type.
 
-If Coq supported higher inductive types natively, we would construct this as somthing like:
+If Coq supported higher inductive types natively, we would construct this as something like:
 
    Inductive Trunc n (A : Type) : Type :=
    | tr : A -> Trunc n A
@@ -30,15 +30,15 @@ Cumulative Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
 Bind Scope trunc_scope with Trunc.
 Arguments tr {n A} a.
 
-(** Without explicit universe parameters, this instance is insufficiently polymorphic. *)
-Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
-: IsTrunc@{j} n (Trunc@{i} n A).
-Admitted.
+  (** Without explicit universe parameters, this instance is insufficiently polymorphic. *)
+  Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
+    : IsTrunc@{j} n (Trunc@{i} n A).
+  Admitted.
 
-Definition Trunc_ind {n A}
-  (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
-  : (forall a, P (tr a)) -> (forall aa, P aa)
-:= (fun f aa => match aa with tr a => fun _ => f a end Pt).
+  Definition Trunc_ind {n A}
+    (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
+    : (forall a, P (tr a)) -> (forall aa, P aa)
+    := fun f aa => match aa with tr a => fun _ => f a end Pt.
 
 End Trunc.
 
@@ -46,7 +46,7 @@ End Trunc.
 
 Definition Trunc_rec {n A X} `{IsTrunc n X}
   : (A -> X) -> (Trunc n A -> X)
-:= Trunc_ind (fun _ => X).
+  := Trunc_ind (fun _ => X).
 
 Definition Trunc_rec_tr n {A : Type}
   : Trunc_rec (A:=A) (tr (n:=n)) == idmap
diff --git a/theories/Types/Empty.v b/theories/Types/Empty.v
index dcbd8d37fc..64663b0950 100644
--- a/theories/Types/Empty.v
+++ b/theories/Types/Empty.v
@@ -47,9 +47,9 @@ Defined.
 Global Instance isequiv_all_to_empty (T : Type) (f : T -> Empty) : IsEquiv f.
 Proof.
   refine (Build_IsEquiv _ _ _ 
-    (Empty_ind (fun _ => T))                (* := equiv_inf *)
-    (fun fals:Empty => match fals with end) (* : f o equiv_inf == idmap *)
-    (fun t:T => match (f t) with end)       (* : equiv_inf o f == idmap *)
+    (Empty_ind (fun _ => T))                (* := equiv_inv *)
+    (fun fals:Empty => match fals with end) (* : f o equiv_inv == idmap *)
+    (fun t:T => match (f t) with end)       (* : equiv_inv o f == idmap *)
     (_)                                     (* adjointify part *)  ).
   intro t. 
   exact (Empty_rec (f t)).
@@ -60,7 +60,4 @@ Definition equiv_to_empty {T : Type} (f : T -> Empty) : T <~> Empty
 
 (** ** Paths *)
 
-(** We could probably prove some theorems about non-existing paths in
-   [Empty], but this is really quite useless. As soon as an element
-   of [Empty] is hypothesized, we can prove whatever we like with
-   a simple elimination. *)
+(** We could probably prove some theorems about non-existing paths in [Empty], but this is really quite useless. As soon as an element of [Empty] is hypothesized, we can prove whatever we like with a simple elimination. *)

From f04481c5f0447fda924d921bde495851196f77d3 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 6 Nov 2024 20:59:20 -0500
Subject: [PATCH 2/6] Truncations/Core: remove redundant isequiv_Trunc_functor

---
 theories/Truncations/Core.v | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
index 995be86c6c..04e9b67b33 100644
--- a/theories/Truncations/Core.v
+++ b/theories/Truncations/Core.v
@@ -117,10 +117,6 @@ Section TruncationModality.
     : @Trunc_functor X X idmap == idmap
     := O_functor_idmap (Tr n) X.
 
-  Definition isequiv_Trunc_functor {X Y} (f : X -> Y) `{IsEquiv _ _ f}
-    : IsEquiv (Trunc_functor f)
-    := isequiv_O_functor (Tr n) f.
-
   Definition equiv_Trunc_prod_cmp {X Y}
     : Tr n (X * Y) <~> Tr n X * Tr n Y
     := equiv_O_prod_cmp (Tr n) X Y.

From 11f54144d6c537a1d78e0de5472bcdeb79b75c03 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 6 Nov 2024 21:00:29 -0500
Subject: [PATCH 3/6] Truncations/Core: remove redundant Delimit and unused
 Bind

---
 theories/Truncations/Core.v | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
index 04e9b67b33..639471bcad 100644
--- a/theories/Truncations/Core.v
+++ b/theories/Truncations/Core.v
@@ -23,12 +23,10 @@ However, while we are faking our higher-inductives anyway, we can take some shor
 *)
 
 Module Export Trunc.
-Delimit Scope trunc_scope with trunc.
 
-Cumulative Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
-  tr : A -> Trunc n A.
-Bind Scope trunc_scope with Trunc.
-Arguments tr {n A} a.
+  Cumulative Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+    tr : A -> Trunc n A.
+  Arguments tr {n A} a.
 
   (** Without explicit universe parameters, this instance is insufficiently polymorphic. *)
   Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})

From 77fcd7728210cb815882d6f3450cd223a39fe989 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 6 Nov 2024 21:01:13 -0500
Subject: [PATCH 4/6] Truncations/Core: update comments around
 strip_truncations

---
 theories/Truncations/Core.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
index 639471bcad..f7090b549d 100644
--- a/theories/Truncations/Core.v
+++ b/theories/Truncations/Core.v
@@ -323,9 +323,8 @@ Proof.
     reflexivity.
 Defined.
 
-(** ** Tactic to remove truncations in hypotheses if possible
+(** ** Tactic to remove truncations in hypotheses if possible *)
 
-  See [strip_reflections] and [strip_modalities] for generalizations to other reflective subuniverses and modalities. *)
 Ltac strip_truncations :=
   (** search for truncated hypotheses *)
   progress repeat
@@ -337,8 +336,8 @@ Ltac strip_truncations :=
         [];
         intro T
   end.
-(** We would like to define this in terms of the [strip_modalities] tactic, however [O_ind] uses more universes than [Trunc_ind] which causes some problems down the line. *)
-(* Ltac strip_truncations := strip_modalities. *)
+
+(** See [strip_reflections] and [strip_modalities] for generalizations to other reflective subuniverses and modalities.  We provide this version because it sometimes needs fewer universes (due to the cumulativity of [Trunc]).  However, that same cumulativity sometimes causes free universe variables.  For a hypothesis of type [Trunc@{i} X], we can use [Trunc_ind@{i j}], but sometimes Coq uses [Trunc_ind@{k j}] with [i <= k] and [k] otherwise free.  In these cases, [strip_reflections] and/or [strip_modalities] may generate fewer universe variables. *)
 
 (** ** Iterated truncations *)
 

From ce97ca80acc3c87cc8ebda031922b6c99cd8c308 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 6 Nov 2024 21:03:58 -0500
Subject: [PATCH 5/6] Rings/Ideal: reduce universe variables

---
 theories/Algebra/Rings/Ideal.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Algebra/Rings/Ideal.v b/theories/Algebra/Rings/Ideal.v
index 5bbc244db8..725bea0625 100644
--- a/theories/Algebra/Rings/Ideal.v
+++ b/theories/Algebra/Rings/Ideal.v
@@ -396,7 +396,7 @@ Arguments ligt_add_neg {R X r s}.
 Arguments ligt_mul {R X r s}.
 
 (** Left ideal generated by a subset. *)
-Definition leftideal_generated {R : Ring} (X : R -> Type) : LeftIdeal R.
+Definition leftideal_generated@{u v} {R : Ring@{u}} (X : R -> Type@{v}) : LeftIdeal@{u v} R.
 Proof.
   snrapply Build_LeftIdeal.
   - snrapply Build_Subgroup'.
@@ -410,7 +410,7 @@ Proof.
 Defined.
 
 (** Right ideal generated by a subset. *)
-Definition rightideal_generated {R : Ring} (X : R -> Type) : RightIdeal R
+Definition rightideal_generated@{u v} {R : Ring@{u}} (X : R -> Type@{v}) : RightIdeal@{u v} R
   := Build_RightIdeal R (leftideal_generated (R:=rng_op R) X) _.
 
 (** Underlying type family of a two-sided ideal generated by subset. *)

From ead1620795293a2d5c8d6906101f1be620da8910 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 6 Nov 2024 21:04:32 -0500
Subject: [PATCH 6/6] Simplify/annotate a few things

---
 theories/Truncations/Core.v | 2 +-
 theories/Types/Bool.v       | 5 +----
 theories/Types/Empty.v      | 2 +-
 3 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
index f7090b549d..1527dbfb92 100644
--- a/theories/Truncations/Core.v
+++ b/theories/Truncations/Core.v
@@ -91,7 +91,7 @@ Section TruncationModality.
   (** ** Functoriality *)
 
   (** Since a modality lives on a single universe, by default if we simply define [Trunc_functor] to be [O_functor] then it would force [X] and [Y] to live in the same universe.  But since we defined [Trunc] as a cumulative inductive, if we add universe annotations we can make [Trunc_functor] more universe-polymorphic than [O_functor] is.  This is sometimes useful.  *)
-  Definition Trunc_functor@{i j k} {X : Type@{i}} {Y : Type@{j}} (f : X -> Y)
+  Definition Trunc_functor@{i j k | i <= k, j <= k} {X : Type@{i}} {Y : Type@{j}} (f : X -> Y)
     : Tr@{i} n X -> Tr@{j} n Y
     := O_functor@{k k k} (Tr n) f.
 
diff --git a/theories/Types/Bool.v b/theories/Types/Bool.v
index b27e833f21..f24cd297a8 100644
--- a/theories/Types/Bool.v
+++ b/theories/Types/Bool.v
@@ -67,10 +67,7 @@ Section BoolDecidable.
                     | false, true => inr false_ne_true
                   end.
 
-  Corollary hset_bool : IsHSet Bool.
-  Proof.
-    exact _.
-  Defined.
+  Definition hset_bool : IsHSet Bool := _.
 End BoolDecidable.
 
 (** In particular, [negb] has no fixed points *)
diff --git a/theories/Types/Empty.v b/theories/Types/Empty.v
index 64663b0950..ef66e13922 100644
--- a/theories/Types/Empty.v
+++ b/theories/Types/Empty.v
@@ -39,7 +39,7 @@ Definition equiv_empty_rec@{u} `{Funext} (A : Type@{u})
 
 Global Instance istrunc_Empty@{} (n : trunc_index) : IsTrunc n.+1 Empty.
 Proof.
-  refine (@istrunc_leq (-1)%trunc n.+1 tt _ _).
+  refine (@istrunc_leq (-1) n.+1 tt _ _).
   apply istrunc_S.
   intros [].
 Defined.