From 4a0c7b61931c8f2d37c963167858a52f5483ed46 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 9 Jan 2024 15:12:54 -0500
Subject: [PATCH 1/7] Reduce universe variables and other clean-ups

---
 theories/Algebra/AbGroups/Z.v          |   8 +-
 theories/Algebra/Groups/Group.v        |   1 +
 theories/Homotopy/SuccessorStructure.v |  30 +++---
 theories/Spaces/Finite/Fin.v           | 139 ++++++++++++-------------
 theories/Spaces/Int/Core.v             |   2 +
 theories/Spaces/Int/LoopExp.v          |  26 +----
 theories/Spaces/Int/Spec.v             |  35 ++++++-
 theories/Spaces/Pos/Core.v             |   4 +-
 theories/Spaces/Pos/Spec.v             |   2 +
 9 files changed, 133 insertions(+), 114 deletions(-)

diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index edf5b2e0eac..520b2388621 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -8,7 +8,11 @@ Require Import Algebra.AbGroups.AbelianGroup.
 
 Local Open Scope int_scope.
 
-Definition abgroup_Z : AbGroup.
+Section MinimizationToSet.
+
+Local Set Universe Minimization ToSet.
+
+Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
   snrapply Build_AbGroup.
   - refine (Build_Group Int int_add 0 int_negation _); repeat split.
@@ -20,6 +24,8 @@ Proof.
   - exact int_add_comm.
 Defined.
 
+End MinimizationToSet.
+
 (** We can multiply by [n : Int] in any abelian group. *)
 Definition ab_mul (n : Int) {A : AbGroup} : GroupHomomorphism A A.
 Proof.
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 4831eae893d..972abc7ad6d 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -252,6 +252,7 @@ Definition pequiv_groupisomorphism {A B : Group}
   := fun f => Build_pEquiv _ _ f _.
 
 Coercion equiv_groupisomorphism : GroupIsomorphism >-> Equiv.
+Coercion pequiv_groupisomorphism : GroupIsomorphism >-> pEquiv.
 
 Definition equiv_path_groupisomorphism `{F : Funext} {G H : Group}
   (f g : GroupIsomorphism G H)
diff --git a/theories/Homotopy/SuccessorStructure.v b/theories/Homotopy/SuccessorStructure.v
index df78bec0247..f2b381f85f6 100644
--- a/theories/Homotopy/SuccessorStructure.v
+++ b/theories/Homotopy/SuccessorStructure.v
@@ -1,8 +1,11 @@
 Require Import Basics.
+Require Import Nat.Core.
 Require Import Spaces.Int.
 Require Import Spaces.Finite.Fin.
 Require Import WildCat.
 
+Local Set Universe Minimization ToSet.
+
 (** * Successor Structures. *)
 
 (** A successor structure is just a type with a endofunctor on it, called 'successor'. Typical examples include either the integers or natural numbers with the successor (or predecessor) operation. *)
@@ -15,6 +18,7 @@ Record SuccStr : Type := {
 Declare Scope succ_scope.
 
 Local Open Scope nat_scope.
+Local Open Scope type_scope.
 Local Open Scope succ_scope.
 
 Delimit Scope succ_scope with succ.
@@ -33,14 +37,16 @@ Notation "'+Z'" := IntSucc : succ_scope.
 
 (** Stratified successor structures *)
 
-Definition StratifiedType (N : SuccStr) (n : nat) : Type := N * Fin n.
+(** If [N] has a successor structure, then so does the product [N * Fin n].  The successor operation increases the second factor, and if it wraps around, it also increases the first factor. *)
+
+Definition StratifiedType (N : SuccStr) (n : nat) := N * Fin n.
 
 Definition stratified_succ (N : SuccStr) (n : nat) (x : StratifiedType N n)
   : StratifiedType N n.
 Proof.
   constructor.
-  + induction n.
-    - induction (snd x).
+  + destruct n.
+    - exact (Empty_rec _ (snd x)).
     - destruct (dec (snd x = inr tt)).
       * exact (ss_succ (fst x)).
       * exact (fst x).
@@ -51,21 +57,17 @@ Definition Stratified (N : SuccStr) (n : nat) : SuccStr
   := Build_SuccStr (StratifiedType N n) (stratified_succ N n).
 
 (** Addition in successor structures *)
-Fixpoint ss_add {N : SuccStr} (n : N) (k : nat) : N :=
-  match k with
-  | O   => n
-  | S k => (ss_add n k).+1
-  end.
+Definition ss_add {N : SuccStr} (n : N) (k : nat) : N := nat_iter k ss_succ n.
 
 Infix "+" := ss_add : succ_scope.
 
 Definition ss_add_succ {N : SuccStr} (n : N) (k : nat)
-  : (n + k.+1) = n.+1 + k.
-Proof.
-  induction k.
-  + reflexivity.
-  + exact (ap ss_succ IHk).
-Defined.
+  : n + k.+1 = n.+1 + k
+  := nat_iter_succ_r k ss_succ n.
+
+Definition ss_add_sum {N : SuccStr} (n : N) (k l : nat)
+  : n + (k + l) = (n + l) + k
+  := nat_iter_add k l ss_succ n.
 
 (** Nat and Int segmented by triples *)
 Notation "'N3'" := (Stratified (+N) 3) : succ_scope.
diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
index 740767355bc..b81e7e0236a 100644
--- a/theories/Spaces/Finite/Fin.v
+++ b/theories/Spaces/Finite/Fin.v
@@ -5,6 +5,9 @@ Require Import HSet.
 Require Import Spaces.Nat.
 Require Import Equiv.PathSplit.
 
+(** By setting this, using [simple_induction] instead of [induction], and specifying universe variables in a couple of places, we can avoid all universe variables in this file.  Several results are confirmed to use no universe variables with an @{} annotation. *)
+Local Set Universe Minimization ToSet.
+
 Local Open Scope path_scope.
 Local Open Scope nat_scope.
 
@@ -38,10 +41,10 @@ Proof.
   exact (inl (inr tt)).
 Defined.
 
-Global Instance decidablepaths_fin (n : nat)
+Global Instance decidablepaths_fin@{} (n : nat)
 : DecidablePaths (Fin n).
 Proof.
-  induction n as [|n IHn]; simpl; exact _.
+  simple_induction n n IHn; simpl; exact _.
 Defined.
 
 Global Instance contr_fin1 : Contr (Fin 1).
@@ -81,31 +84,30 @@ Fixpoint fsucc {n : nat} : Fin n -> Fin n.+1 :=
   end.
 
 (** This injection is an injection/embedding *)
-Lemma isembedding_fsucc {n : nat} : IsEmbedding (@fsucc n).
+Lemma isembedding_fsucc@{} {n : nat} : IsEmbedding (@fsucc n).
 Proof.
   apply isembedding_isinj_hset.
-  induction n.
+  simple_induction n n IHn.
   - intro i. elim i.
   - intros [] []; intro p.
     + f_ap. apply IHn. eapply path_sum_inl. exact p.
     + destruct u. elim (inl_ne_inr _ _ p).
     + destruct u. elim (inr_ne_inl _ _ p).
     + destruct u, u0; reflexivity.
-Qed.
+Defined.
 
 Lemma path_fin_fsucc_incl {n : nat} : forall k : Fin n, fsucc (fin_incl k) = fin_incl (fsucc k).
 Proof.
   trivial.
-Qed.
+Defined.
 
-Lemma path_nat_fin_incl {n : nat} : forall k : Fin n, fin_to_nat (fin_incl k) = fin_to_nat k.
-Proof.
-  reflexivity.
-Qed.
+Definition path_nat_fin_incl {n : nat} (k : Fin n)
+  : fin_to_nat (fin_incl k) = fin_to_nat k
+  := 1.
 
-Lemma path_nat_fsucc {n : nat} : forall k : Fin n, fin_to_nat (fsucc k) = S (fin_to_nat k).
+Lemma path_nat_fsucc@{} {n : nat} : forall k : Fin n, fin_to_nat (fsucc k) = S (fin_to_nat k).
 Proof.
-  induction n as [|n' IHn].
+  simple_induction n n IHn.
   - intros [].
   - intros [k'|[]].
     + rewrite path_fin_fsucc_incl, path_nat_fin_incl.
@@ -113,17 +115,15 @@ Proof.
     + reflexivity.
 Defined.
 
-Lemma path_nat_fin_zero {n} : fin_to_nat (@fin_zero n) = 0.
+Lemma path_nat_fin_zero@{} {n} : fin_to_nat (@fin_zero n) = 0.
 Proof.
-  induction n as [|n' IHn].
+  simple_induction n n IHn.
   - reflexivity.
   - trivial.
 Defined.
 
-Lemma path_nat_fin_last {n} : fin_to_nat (@fin_last n) = n.
-Proof.
-  reflexivity.
-Qed.
+Definition path_nat_fin_last {n} : fin_to_nat (@fin_last n) = n
+  := 1.
 
 (** ** Transposition equivalences *)
 
@@ -132,7 +132,7 @@ Qed.
 (** *** Swap the last two elements. *)
 
 Definition fin_transpose_last_two (n : nat)
-: Fin n.+2 <~> Fin n.+2
+  : Fin n.+2 <~> Fin n.+2
   := ((equiv_sum_assoc _ _ _)^-1)
        oE (1 +E (equiv_sum_symm _ _))
        oE (equiv_sum_assoc _ _ _).
@@ -140,21 +140,21 @@ Definition fin_transpose_last_two (n : nat)
 Arguments fin_transpose_last_two : simpl nomatch.
 
 Definition fin_transpose_last_two_last (n : nat)
-: fin_transpose_last_two n (inr tt) = (inl (inr tt))
+  : fin_transpose_last_two n (inr tt) = (inl (inr tt))
   := 1.
 
 Definition fin_transpose_last_two_nextlast (n : nat)
-: fin_transpose_last_two n (inl (inr tt)) = (inr tt)
+  : fin_transpose_last_two n (inl (inr tt)) = (inr tt)
   := 1.
 
 Definition fin_transpose_last_two_rest (n : nat) (k : Fin n)
-: fin_transpose_last_two n (inl (inl k)) = (inl (inl k))
+  : fin_transpose_last_two n (inl (inl k)) = (inl (inl k))
   := 1.
 
 (** *** Swap the last element with [k]. *)
 
 Fixpoint fin_transpose_last_with (n : nat) (k : Fin n.+1)
-: Fin n.+1 <~> Fin n.+1.
+  : Fin n.+1 <~> Fin n.+1.
 Proof.
   destruct k as [k|].
   - destruct n as [|n].
@@ -170,44 +170,44 @@ Defined.
 
 Arguments fin_transpose_last_with : simpl nomatch.
 
-Definition fin_transpose_last_with_last (n : nat) (k : Fin n.+1)
-: fin_transpose_last_with n k (inr tt) = k.
+Definition fin_transpose_last_with_last@{} (n : nat) (k : Fin n.+1)
+  : fin_transpose_last_with n k (inr tt) = k.
 Proof.
   destruct k as [k|].
-  - induction n as [|n IH]; simpl.
+  - simple_induction n n IHn; intro k; simpl.
     + elim k.
     + destruct k as [k|].
-      * simpl. rewrite IH; reflexivity.
+      * simpl. rewrite IHn; reflexivity.
       * simpl. apply ap, ap, path_contr.
   - (** We have to destruct [n] since fixpoints don't reduce unless their argument is a constructor. *)
     destruct n; simpl.
     all:apply ap, path_contr.
 Qed.
 
-Definition fin_transpose_last_with_with (n : nat) (k : Fin n.+1)
-: fin_transpose_last_with n k k = inr tt.
+Definition fin_transpose_last_with_with@{} (n : nat) (k : Fin n.+1)
+  : fin_transpose_last_with n k k = inr tt.
 Proof.
   destruct k as [k|].
-  - induction n as [|n IH]; simpl.
+  - simple_induction n n IHn; intro k; simpl.
     + elim k.
     + destruct k as [|k]; simpl.
-      * rewrite IH; reflexivity.
+      * rewrite IHn; reflexivity.
       * apply ap, path_contr.
   - destruct n; simpl.
     all:apply ap, path_contr.
 Qed.
 
-Definition fin_transpose_last_with_rest (n : nat)
-           (k : Fin n.+1) (l : Fin n)
-           (notk : k <> inl l)
-: fin_transpose_last_with n k (inl l) = (inl l).
+Definition fin_transpose_last_with_rest@{} (n : nat)
+  (k : Fin n.+1) (l : Fin n)
+  (notk : k <> inl l)
+  : fin_transpose_last_with n k (inl l) = (inl l).
 Proof.
   destruct k as [k|].
-  - induction n as [|n IH]; simpl.
-    1:elim k.
+  - simple_induction n n IHn; intros k l notk; simpl.
+    1: elim k.
     destruct k as [k|]; simpl.
     { destruct l as [l|]; simpl.
-      - rewrite IH.
+      - rewrite IHn.
         + reflexivity.
         + exact (fun p => notk (ap inl p)).
       - reflexivity. }
@@ -215,16 +215,16 @@ Proof.
       - reflexivity.
       - elim (notk (ap inl (ap inr (path_unit _ _)))). }
   - destruct n; reflexivity.
-Qed.
+Defined.
 
 Definition fin_transpose_last_with_last_other (n : nat) (k : Fin n.+1)
-: fin_transpose_last_with n (inr tt) k = k.
+  : fin_transpose_last_with n (inr tt) k = k.
 Proof.
   destruct n; reflexivity.
-Qed.
+Defined.
 
 Definition fin_transpose_last_with_invol (n : nat) (k : Fin n.+1)
-: fin_transpose_last_with n k o fin_transpose_last_with n k == idmap.
+  : fin_transpose_last_with n k o fin_transpose_last_with n k == idmap.
 Proof.
   intros l.
   destruct l as [l|[]].
@@ -240,7 +240,7 @@ Proof.
       apply fin_transpose_last_with_last_other.
   - rewrite fin_transpose_last_with_last.
     apply fin_transpose_last_with_with.
-Qed.
+Defined.
 
 (** ** Equivalences between canonical finite sets *)
 
@@ -248,19 +248,18 @@ Qed.
 
 (** Here is the uncurried map that constructs an equivalence [Fin n.+1 <~> Fin m.+1]. *)
 Definition fin_equiv (n m : nat)
-           (k : Fin m.+1) (e : Fin n <~> Fin m)
-: Fin n.+1 <~> Fin m.+1
-  := (fin_transpose_last_with m k)
-       oE (e +E 1).
+  (k : Fin m.+1) (e : Fin n <~> Fin m)
+  : Fin n.+1 <~> Fin m.+1
+  := (fin_transpose_last_with m k) oE (e +E 1).
 
 (** Here is the curried version that we will prove to be an equivalence. *)
 Definition fin_equiv' (n m : nat)
-: ((Fin m.+1) * (Fin n <~> Fin m)) -> (Fin n.+1 <~> Fin m.+1)
+  : ((Fin m.+1) * (Fin n <~> Fin m)) -> (Fin n.+1 <~> Fin m.+1)
   := fun ke => fin_equiv n m (fst ke) (snd ke).
 
 (** We construct its inverse and the two homotopies first as versions using homotopies without funext (similar to [ExtendableAlong]), then apply funext at the end. *)
-Definition fin_equiv_hfiber (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
-: { kf : (Fin m.+1) * (Fin n <~> Fin m) & fin_equiv' n m kf == e }.
+Definition fin_equiv_hfiber@{} (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
+  : { kf : (Fin m.+1) * (Fin n <~> Fin m) & fin_equiv' n m kf == e }.
 Proof.
   simpl in e.
   refine (equiv_sigma_prod _ _).
@@ -268,7 +267,7 @@ Proof.
   assert (p' := (moveL_equiv_V _ _ p)^).
   exists y.
   destruct y as [y|[]].
-  + simple refine (equiv_unfunctor_sum_l
+  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set}
               (fin_transpose_last_with m (inl y) oE e)
               _ _ ; _).
     { intros a. ev_equiv.
@@ -287,7 +286,7 @@ Proof.
     * rewrite unfunctor_sum_l_beta.
       apply fin_transpose_last_with_invol.
     * refine (fin_transpose_last_with_last _ _ @ p^).
-  + simple refine (equiv_unfunctor_sum_l e _ _ ; _).
+  + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set} e _ _ ; _).
     { intros a.
       destruct (is_inl_or_is_inr (e (inl a))) as [l|r].
       - exact l.
@@ -306,16 +305,16 @@ Proof.
 Qed.
 
 Definition fin_equiv_inv (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
-: (Fin m.+1) * (Fin n <~> Fin m)
+  : (Fin m.+1) * (Fin n <~> Fin m)
   := (fin_equiv_hfiber n m e).1.
 
 Definition fin_equiv_issect (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
-: fin_equiv' n m (fin_equiv_inv n m e) == e
+  : fin_equiv' n m (fin_equiv_inv n m e) == e
   := (fin_equiv_hfiber n m e).2.
 
 Definition fin_equiv_inj_fst (n m : nat)
            (k l : Fin m.+1) (e f : Fin n <~> Fin m)
-: (fin_equiv n m k e == fin_equiv n m l f) -> (k = l).
+  : (fin_equiv n m k e == fin_equiv n m l f) -> (k = l).
 Proof.
   intros p.
   refine (_ @ p (inr tt) @ _); simpl;
@@ -324,7 +323,7 @@ Qed.
 
 Definition fin_equiv_inj_snd (n m : nat)
            (k l : Fin m.+1) (e f : Fin n <~> Fin m)
-: (fin_equiv n m k e == fin_equiv n m l f) -> (e == f).
+  : (fin_equiv n m k e == fin_equiv n m l f) -> (e == f).
 Proof.
   intros p.
   intros x. assert (q := p (inr tt)); simpl in q.
@@ -336,7 +335,7 @@ Qed.
 
 (** Now it's time for funext. *)
 Global Instance isequiv_fin_equiv `{Funext} (n m : nat)
-: IsEquiv (fin_equiv' n m).
+  : IsEquiv (fin_equiv' n m).
 Proof.
   refine (isequiv_pathsplit 0 _); split.
   - intros e; exists (fin_equiv_inv n m e).
@@ -350,29 +349,29 @@ Proof.
     + refine (fin_equiv_inj_fst n m k l e f p).
     + apply path_equiv, path_arrow.
       refine (fin_equiv_inj_snd n m k l e f p).
-Qed.
+Defined.
 
 Definition equiv_fin_equiv `{Funext} (n m : nat)
-: ((Fin m.+1) * (Fin n <~> Fin m)) <~> (Fin n.+1 <~> Fin m.+1)
+  : ((Fin m.+1) * (Fin n <~> Fin m)) <~> (Fin n.+1 <~> Fin m.+1)
   := Build_Equiv _ _ (fin_equiv' n m) _.
 
 (** In particular, this implies that if two canonical finite sets are equivalent, then their cardinalities are equal. *)
 Definition nat_eq_fin_equiv (n m : nat)
 : (Fin n <~> Fin m) -> (n = m).
 Proof.
-  revert m; induction n as [|n IHn]; induction m as [|m IHm]; intros e.
+  revert m; simple_induction n n IHn; intro m; simple_induction m m IHm; intros e.
   - exact idpath.
   - elim (e^-1 (inr tt)).
   - elim (e (inr tt)).
   - refine (ap S (IHn m _)).
     exact (snd (fin_equiv_inv n m e)).
-Qed.
+Defined.
 
 (** ** Initial segments of [nat] *)
 
 Definition nat_fin (n : nat) (k : Fin n) : nat.
 Proof.
-  induction n as [|n nf].
+  simple_induction n n nf; intro k.
   - contradiction.
   - destruct k as [k|_].
     + exact (nf k).
@@ -380,12 +379,12 @@ Proof.
 Defined.
 
 Definition nat_fin_inl (n : nat) (k : Fin n)
-: nat_fin n.+1 (inl k) = nat_fin n k
+  : nat_fin n.+1 (inl k) = nat_fin n k
   := 1.
 
 Definition nat_fin_compl (n : nat) (k : Fin n) : nat.
 Proof.
-  induction n as [|n nfc].
+  simple_induction n n nfc; intro k.
   - contradiction.
   - destruct k as [k|_].
     + exact (nfc k).+1.
@@ -393,20 +392,20 @@ Proof.
 Defined.
 
 Definition nat_fin_compl_compl n k
-: (nat_fin n k + nat_fin_compl n k).+1 = n.
+  : (nat_fin n k + nat_fin_compl n k).+1 = n.
 Proof.
-  induction n as [|n IH].
+  simple_induction n n IHn; intro k.
   - contradiction.
   - destruct k as [k|?]; simpl.
     + rewrite nat_add_comm.
-      specialize (IH k).
-      rewrite nat_add_comm in IH.
-      exact (ap S IH).
+      specialize (IHn k).
+      rewrite nat_add_comm in IHn.
+      exact (ap S IHn).
     + rewrite nat_add_comm; reflexivity.
 Qed.
 
 (** [fsucc_mod] is the successor function mod n *)
-Definition fsucc_mod {n : nat} : Fin n -> Fin n.
+Definition fsucc_mod@{} {n : nat} : Fin n -> Fin n.
 Proof.
   destruct n.
   1: exact idmap.
diff --git a/theories/Spaces/Int/Core.v b/theories/Spaces/Int/Core.v
index 2979c859063..4b90aba6d6a 100644
--- a/theories/Spaces/Int/Core.v
+++ b/theories/Spaces/Int/Core.v
@@ -1,6 +1,8 @@
 Require Import Basics.
 Require Import Spaces.Pos.
 
+Local Set Universe Minimization ToSet.
+
 (** * The Integers. *)
 
 Local Close Scope trunc_scope.
diff --git a/theories/Spaces/Int/LoopExp.v b/theories/Spaces/Int/LoopExp.v
index 0ede5e253df..d32efdf650d 100644
--- a/theories/Spaces/Int/LoopExp.v
+++ b/theories/Spaces/Int/LoopExp.v
@@ -26,6 +26,8 @@ Definition loopexp {A : Type} {x : A} (p : x = x) (z : Int) : (x = x)
        | pos n => loopexp_pos p n
      end.
 
+(** TODO: One can also define [loopexp] as [int_iter (equiv_concat_r p x) z idpath].  This has slightly different computational behaviour, e.g., it sends [1 : int] to [1 @ p] rather than [p].  But with this definition, some of the results below become special cases of results in Int.Equiv, and others could be generalized to results belonging in Int.Equiv.  It's probably worth investigating this. *)
+
 Lemma loopexp_pos_inv {A : Type} {x : A} (p : x = x) (n : Pos)
   : loopexp_pos p^ n = (loopexp_pos p n)^.
 Proof.
@@ -65,28 +67,6 @@ Proof.
   + apply ap_loopexp_pos.
 Qed.
 
-Lemma int_add_succ_l a b : int_succ a + b = int_succ (a + b).
-Proof.
-  rewrite <- int_add_assoc, (int_add_comm 1 b).
-  apply int_add_assoc.
-Qed.
-
-Lemma int_add_succ_r a b : a + int_succ b = int_succ (a + b).
-Proof.
-  apply int_add_assoc.
-Qed.
-
-Lemma int_add_pred_l a b : int_pred a + b = int_pred (a + b).
-Proof.
-  rewrite <- int_add_assoc, (int_add_comm (-1) b).
-  apply int_add_assoc.
-Qed.
-
-Lemma int_add_pred_r a b : a + int_pred b = int_pred (a + b).
-Proof.
-  apply int_add_assoc.
-Qed.
-
 Lemma loopexp_pos_concat {A : Type} {x : A} (p : x = x) (a : Pos)
   : loopexp_pos p a @ p = p @ loopexp_pos p a.
 Proof.
@@ -215,4 +195,4 @@ Proof.
   refine (_ @ equiv_path_loopexp p z a).
   refine (ap (fun q => equiv_path A A (loopexp q z) a) _).
   apply eissect.
-Defined.
\ No newline at end of file
+Defined.
diff --git a/theories/Spaces/Int/Spec.v b/theories/Spaces/Int/Spec.v
index 677d137c2ba..cb1dc6b975b 100644
--- a/theories/Spaces/Int/Spec.v
+++ b/theories/Spaces/Int/Spec.v
@@ -2,6 +2,8 @@ Require Import Basics.
 Require Import Spaces.Pos.
 Require Import Spaces.Int.Core.
 
+Local Set Universe Minimization ToSet.
+
 Local Open Scope int_scope.
 
 (** ** Addition is commutative *)
@@ -133,6 +135,13 @@ Proof.
   apply pos_pred_double_succ.
 Qed.
 
+(* ** The successor autoequivalence. *)
+Global Instance isequiv_int_succ : IsEquiv int_succ | 0
+  := isequiv_adjointify int_succ _ int_succ_pred int_pred_succ.
+
+Definition equiv_int_succ : Int <~> Int
+  := Build_Equiv _ _ _ isequiv_int_succ.
+
 (** ** Negation distributes over addition *)
 Lemma int_negation_add_distr n m : - (n + m) = - n + - m.
 Proof.
@@ -347,12 +356,28 @@ Proof.
   - apply int_add_assoc_pos.
 Qed.
 
-(* ** The successor autoequivalence. *)
-Global Instance isequiv_int_succ : IsEquiv int_succ | 0
-  := isequiv_adjointify int_succ _ int_succ_pred int_pred_succ.
+(** ** Relationship between [int_succ], [int_pred] and addition. *)
+Lemma int_add_succ_l a b : int_succ a + b = int_succ (a + b).
+Proof.
+  rewrite <- int_add_assoc, (int_add_comm 1 b).
+  apply int_add_assoc.
+Qed.
 
-Definition equiv_int_succ : Int <~> Int
-  := Build_Equiv _ _ _ isequiv_int_succ.
+Lemma int_add_succ_r a b : a + int_succ b = int_succ (a + b).
+Proof.
+  apply int_add_assoc.
+Qed.
+
+Lemma int_add_pred_l a b : int_pred a + b = int_pred (a + b).
+Proof.
+  rewrite <- int_add_assoc, (int_add_comm (-1) b).
+  apply int_add_assoc.
+Qed.
+
+Lemma int_add_pred_r a b : a + int_pred b = int_pred (a + b).
+Proof.
+  apply int_add_assoc.
+Qed.
 
 (** ** Commutativity of multiplication *)
 Lemma int_mul_comm n m : n * m = m * n.
diff --git a/theories/Spaces/Pos/Core.v b/theories/Spaces/Pos/Core.v
index 24ffd6b8138..a76ffe22853 100644
--- a/theories/Spaces/Pos/Core.v
+++ b/theories/Spaces/Pos/Core.v
@@ -1,6 +1,8 @@
 Require Import Basics.Overture Basics.Tactics Basics.Decidable
   Spaces.Nat.Core.
 
+Local Set Universe Minimization ToSet.
+
 (** * Binary Positive Integers *)
 
 (** Most of this file has been adapted from the coq standard library for positive binary integers. *)
@@ -14,7 +16,7 @@ Inductive Pos : Type0 :=
 Declare Scope positive_scope.
 Delimit Scope positive_scope with pos.
 
-(** Here are some notations that let us right binary positive integers more easily. *)
+(** Here are some notations that let us write binary positive integers more easily. *)
 Notation "1" := xH : positive_scope.
 Notation "p ~ 1" := (x1 p) : positive_scope.
 Notation "p ~ 0" := (x0 p) : positive_scope.
diff --git a/theories/Spaces/Pos/Spec.v b/theories/Spaces/Pos/Spec.v
index 6feab6eb797..0df011990d4 100644
--- a/theories/Spaces/Pos/Spec.v
+++ b/theories/Spaces/Pos/Spec.v
@@ -1,6 +1,8 @@
 Require Import Basics.Overture Basics.Tactics.
 Require Import Pos.Core.
 
+Local Set Universe Minimization ToSet.
+
 Local Open Scope positive_scope.
 
 (** ** Specification of [succ] in term of [add] *)

From a53efef370bcd166562e1cbf4a2974dc6c154e5e Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 10 Jan 2024 09:00:16 -0500
Subject: [PATCH 2/7] Free up universe in proofs of IsHSet, Decidable and
 DecidablePaths

---
 theories/Spaces/Finite/Fin.v | 8 ++++----
 theories/Spaces/Int/Core.v   | 4 ++--
 theories/Spaces/Pos/Core.v   | 4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
index b81e7e0236a..9d3d5b537b2 100644
--- a/theories/Spaces/Finite/Fin.v
+++ b/theories/Spaces/Finite/Fin.v
@@ -34,15 +34,15 @@ Fixpoint fin_to_nat {n} : Fin n -> nat
          end
      end.
 
-Global Instance decidable_fin (n : nat)
-: Decidable (Fin n).
+Global Instance decidable_fin@{u} (n : nat)
+: Decidable@{u} (Fin n).
 Proof.
   destruct n as [|n]; try exact _.
   exact (inl (inr tt)).
 Defined.
 
-Global Instance decidablepaths_fin@{} (n : nat)
-: DecidablePaths (Fin n).
+Global Instance decidablepaths_fin@{u} (n : nat)
+: DecidablePaths@{u} (Fin n).
 Proof.
   simple_induction n n IHn; simpl; exact _.
 Defined.
diff --git a/theories/Spaces/Int/Core.v b/theories/Spaces/Int/Core.v
index 4b90aba6d6a..6c65173b406 100644
--- a/theories/Spaces/Int/Core.v
+++ b/theories/Spaces/Int/Core.v
@@ -228,7 +228,7 @@ Definition sgn z :=
 
 (* ** Decidable paths and truncation. *)
 
-Global Instance decpaths_int : DecidablePaths Int.
+Global Instance decpaths_int : DecidablePaths@{u} Int.
 Proof.
   intros [n | | n] [m | | m].
   + destruct (dec (n = m)) as [p | q].
@@ -247,4 +247,4 @@ Proof.
 Defined.
 
 (** Since integers have decidable paths they are a hset *)
-Global Instance hset_int : IsHSet Int | 0 := _.
+Global Instance hset_int : IsHSet@{u} Int | 0 := _.
diff --git a/theories/Spaces/Pos/Core.v b/theories/Spaces/Pos/Core.v
index a76ffe22853..9cffead5505 100644
--- a/theories/Spaces/Pos/Core.v
+++ b/theories/Spaces/Pos/Core.v
@@ -99,7 +99,7 @@ Definition x1_neq_x0 {z w : Pos} : x1 z <> x0 w
 
 (** * Positive binary integers have decidable paths *)
 
-Global Instance decpaths_pos : DecidablePaths Pos.
+Global Instance decpaths_pos : DecidablePaths@{u} Pos.
 Proof.
   intros n; induction n as [|zn|on];
   intros m; induction m as [|zm|om].
@@ -121,7 +121,7 @@ Proof.
 Defined.
 
 (** Decidable paths imply Pos is a hSet *)
-Global Instance ishset_pos : IsHSet Pos := _.
+Global Instance ishset_pos : IsHSet@{u} Pos := _.
 
 (** * Operations over positive numbers *)
 

From ee629bc603a85d9a5fd6e489bb4d1d1e5d320521 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 16 Jan 2024 10:26:41 -0500
Subject: [PATCH 3/7] Revert "Free up universe in proofs of IsHSet, Decidable
 and DecidablePaths"

This reverts commit a53efef370bcd166562e1cbf4a2974dc6c154e5e.
---
 theories/Spaces/Finite/Fin.v | 8 ++++----
 theories/Spaces/Int/Core.v   | 4 ++--
 theories/Spaces/Pos/Core.v   | 4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
index 9d3d5b537b2..b81e7e0236a 100644
--- a/theories/Spaces/Finite/Fin.v
+++ b/theories/Spaces/Finite/Fin.v
@@ -34,15 +34,15 @@ Fixpoint fin_to_nat {n} : Fin n -> nat
          end
      end.
 
-Global Instance decidable_fin@{u} (n : nat)
-: Decidable@{u} (Fin n).
+Global Instance decidable_fin (n : nat)
+: Decidable (Fin n).
 Proof.
   destruct n as [|n]; try exact _.
   exact (inl (inr tt)).
 Defined.
 
-Global Instance decidablepaths_fin@{u} (n : nat)
-: DecidablePaths@{u} (Fin n).
+Global Instance decidablepaths_fin@{} (n : nat)
+: DecidablePaths (Fin n).
 Proof.
   simple_induction n n IHn; simpl; exact _.
 Defined.
diff --git a/theories/Spaces/Int/Core.v b/theories/Spaces/Int/Core.v
index 6c65173b406..4b90aba6d6a 100644
--- a/theories/Spaces/Int/Core.v
+++ b/theories/Spaces/Int/Core.v
@@ -228,7 +228,7 @@ Definition sgn z :=
 
 (* ** Decidable paths and truncation. *)
 
-Global Instance decpaths_int : DecidablePaths@{u} Int.
+Global Instance decpaths_int : DecidablePaths Int.
 Proof.
   intros [n | | n] [m | | m].
   + destruct (dec (n = m)) as [p | q].
@@ -247,4 +247,4 @@ Proof.
 Defined.
 
 (** Since integers have decidable paths they are a hset *)
-Global Instance hset_int : IsHSet@{u} Int | 0 := _.
+Global Instance hset_int : IsHSet Int | 0 := _.
diff --git a/theories/Spaces/Pos/Core.v b/theories/Spaces/Pos/Core.v
index 9cffead5505..a76ffe22853 100644
--- a/theories/Spaces/Pos/Core.v
+++ b/theories/Spaces/Pos/Core.v
@@ -99,7 +99,7 @@ Definition x1_neq_x0 {z w : Pos} : x1 z <> x0 w
 
 (** * Positive binary integers have decidable paths *)
 
-Global Instance decpaths_pos : DecidablePaths@{u} Pos.
+Global Instance decpaths_pos : DecidablePaths Pos.
 Proof.
   intros n; induction n as [|zn|on];
   intros m; induction m as [|zm|om].
@@ -121,7 +121,7 @@ Proof.
 Defined.
 
 (** Decidable paths imply Pos is a hSet *)
-Global Instance ishset_pos : IsHSet@{u} Pos := _.
+Global Instance ishset_pos : IsHSet Pos := _.
 
 (** * Operations over positive numbers *)
 

From 8fbf18c4503340dcbbbba6721f1006c65d0169d8 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 16 Jan 2024 10:27:32 -0500
Subject: [PATCH 4/7] Empty.v: Local Set Universe Minimization ToSet

---
 theories/Types/Empty.v | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/theories/Types/Empty.v b/theories/Types/Empty.v
index f573317c3e3..d7862754815 100644
--- a/theories/Types/Empty.v
+++ b/theories/Types/Empty.v
@@ -2,6 +2,9 @@
 (** * Theorems about the empty type *)
 
 Require Import Basics.Overture Basics.Equivalences Basics.Trunc.
+
+Local Set Universe Minimization ToSet.
+
 Local Open Scope path_scope.
 
 (** ** Unpacking *)
@@ -12,37 +15,37 @@ Local Open Scope path_scope.
 (** ** Equivalences *)
 (** ** Universal mapping properties *)
 
-Global Instance contr_from_Empty {_ : Funext} (A : Empty -> Type) :
-  Contr (forall x:Empty, A x).
+Global Instance contr_from_Empty@{u} {_ : Funext} (A : Empty -> Type@{u})
+  : Contr@{u} (forall x:Empty, A x).
 Proof.
-  refine (Build_Contr _ (Empty_ind A) _).
-  intros f; apply path_forall; intros x; elim x.
+  refine (Build_Contr@{u} _ (Empty_ind A) _).
+  intros f; apply path_forall@{Set u u}; intros x; elim x.
 Defined.
 
 Lemma Empty_rec {T : Type} (falso: Empty) : T.
 Proof. case falso. Defined.
 
-Global Instance isequiv_empty_rec `{Funext} (A : Type)
-: IsEquiv (fun (_ : Unit) => @Empty_rec A) | 0
-  := isequiv_adjointify _
+Global Instance isequiv_empty_rec@{u} `{Funext} (A : Type@{u})
+  : IsEquiv@{Set u} (fun (_ : Unit) => @Empty_rec A) | 0
+  := isequiv_adjointify@{Set u} _
   (fun _ => tt)
-  (fun f => path_forall _ _ (fun x => Empty_rec x))
+  (fun f => path_forall@{Set u u} _ _ (fun x => Empty_rec x))
   (fun x => match x with tt => idpath end).
 
-Definition equiv_empty_rec `{Funext} (A : Type)
-  : Unit <~> (Empty -> A)
-  := (Build_Equiv _ _ (fun (_ : Unit) => @Empty_rec A) _).
+Definition equiv_empty_rec@{u} `{Funext} (A : Type@{u})
+  : Unit <~> ((Empty -> A) : Type@{u})
+  := (Build_Equiv@{Set u} _ _ (fun (_ : Unit) => @Empty_rec A) _).
 
 (** ** Behavior with respect to truncation *)
 
-Global Instance istrunc_Empty (n : trunc_index) : IsTrunc n.+1 Empty.
+Global Instance istrunc_Empty@{} (n : trunc_index) : IsTrunc n.+1 Empty.
 Proof.
   refine (@istrunc_leq (-1)%trunc n.+1 tt _ _).
   apply istrunc_S.
   intros [].
 Defined.
 
-Global Instance all_to_empty_isequiv (T : Type) (f : T -> Empty) : IsEquiv f.
+Global Instance isequiv_all_to_empty (T : Type) (f : T -> Empty) : IsEquiv f.
 Proof.
   refine (Build_IsEquiv _ _ _ 
     (Empty_ind (fun _ => T))                (* := equiv_inf *)

From 6d7d21881efda8a1950f2839ab3b5fca4e8f8303 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 16 Jan 2024 13:46:33 -0500
Subject: [PATCH 5/7] Basics/Tactics: improve simple_induction, add
 simple_induction'

---
 theories/Basics/Tactics.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/Basics/Tactics.v b/theories/Basics/Tactics.v
index 94fee39f684..45d8fe60eda 100644
--- a/theories/Basics/Tactics.v
+++ b/theories/Basics/Tactics.v
@@ -6,13 +6,17 @@ Require Import Basics.Overture.
 
 (** This module implements various tactics used in the library. *)
 
-(** The following tactic is designed to be more or less interchangeable with [induction n as [ | n' IH ]] whenever [n] is a [nat] or a [trunc_index].  The difference is that it produces proof terms involving [fix] explicitly rather than [nat_ind] or [trunc_index_ind], and therefore does not introduce higher universe parameters. *)
+(** The following tactic is designed to be more or less interchangeable with [induction n as [ | n' IH ]] whenever [n] is a [nat] or a [trunc_index].  The difference is that it produces proof terms involving [fix] explicitly rather than [nat_ind] or [trunc_index_ind], and therefore does not introduce higher universe parameters. It works if [n] is in the context or in the goal. *)
 Ltac simple_induction n n' IH :=
-  generalize dependent n;
+  try generalize dependent n;
   fix IH 1;
   intros [| n'];
   [ clear IH | specialize (IH n') ].
 
+Ltac simple_induction' n :=
+  let IH := fresh "IH" in
+  simple_induction n n IH.
+
 (** Debugging tactics to show the goal during evaluation. *)
 
 Ltac show_goal := match goal with [ |- ?T ] => idtac T end.

From 052fdbc9ca3289bf3d35b6db553b9432f2907d97 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 16 Jan 2024 13:47:08 -0500
Subject: [PATCH 6/7] Spaces.Nat: get rid of lots of universe variables; adjust
 Classes

---
 .../implementations/natpair_integers.v        |  5 +-
 .../Classes/implementations/peano_naturals.v  |  3 +-
 theories/Spaces/Nat/Arithmetic.v              | 89 ++++++++++---------
 theories/Spaces/Nat/Core.v                    | 64 ++++++-------
 4 files changed, 81 insertions(+), 80 deletions(-)

diff --git a/theories/Classes/implementations/natpair_integers.v b/theories/Classes/implementations/natpair_integers.v
index 955c55a4c2d..1c7efea54da 100644
--- a/theories/Classes/implementations/natpair_integers.v
+++ b/theories/Classes/implementations/natpair_integers.v
@@ -1049,10 +1049,7 @@ Global Instance Z_abs@{} : IntAbs@{UN UN UN UN UN
   UN UN UN UN UN
   UN UN UN UN UN
   UN UN} Z N
-  := ltac:(first [exact Z_abs'@{Ularge Ularge Ularge Ularge Ularge
-                                Ularge Ularge}|
-                  exact Z_abs'@{Ularge Ularge Ularge Ularge Ularge
-                                Ularge}]).
+  := Z_abs'.
 
 Notation n_to_z := (naturals_to_semiring N Z).
 
diff --git a/theories/Classes/implementations/peano_naturals.v b/theories/Classes/implementations/peano_naturals.v
index 4737e3b7211..563eea22c9d 100644
--- a/theories/Classes/implementations/peano_naturals.v
+++ b/theories/Classes/implementations/peano_naturals.v
@@ -15,6 +15,7 @@ Local Set Universe Minimization ToSet.
 Section nat_lift.
 
 Universe N.
+(* It's important that the universe [N] be free.  Occasionally, Coq will choose universe variables in proofs that force [N] to be [Set].  To pinpoint where this happens, you can add the line [Constraint Set < N.] here, and see what fails below. *)
 
 Let natpaths := @paths@{N} nat.
 Infix "=N=" := natpaths.
@@ -425,7 +426,7 @@ Qed.
 
 Instance decidable_nat_apart x y : Decidable (nat_apart x y).
 Proof.
-  rapply decidable_sum; apply Nat.Core.decidable_lt.
+  rapply decidable_sum@{N N N}; apply Nat.Core.decidable_lt.
 Defined.
 
 Global Instance nat_trivial_apart : TrivialApart nat.
diff --git a/theories/Spaces/Nat/Arithmetic.v b/theories/Spaces/Nat/Arithmetic.v
index 6c4a124f4c0..8ee89b24a98 100644
--- a/theories/Spaces/Nat/Arithmetic.v
+++ b/theories/Spaces/Nat/Arithmetic.v
@@ -1,7 +1,9 @@
 Require Import Basics.
 Require Import Spaces.Nat.Core.
-Local Close Scope trunc_scope.
   
+Local Set Universe Minimization ToSet.
+
+Local Close Scope trunc_scope.
 Local Open Scope nat_scope.
 
 Ltac nat_absurd_trivial :=
@@ -37,7 +39,7 @@ Local Definition transitive_paths_nat (n m k : nat)
 Proposition assoc_nat_add (n m k : nat)
   : n + (m + k) = (n + m) + k.
 Proof.
-  revert m k; induction n.
+  revert m k; simple_induction n n IHn.
   - reflexivity.
   - intros m k. change (n.+1 + (m + k)) with (n + (m + k)).+1.
     apply (transitive_paths _ _ _ (nat_add_n_Sm _ _)).
@@ -167,7 +169,7 @@ Defined.
 
 Proposition sub_n_n (n : nat) : n - n = 0.
 Proof.
-  induction n.
+  simple_induction n n IHn.
   - reflexivity.
   - simpl; exact IHn.
 Defined.
@@ -194,10 +196,10 @@ Ltac rewrite_subnn :=
 Proposition add_n_sub_n_eq (m n : nat) : m + n - n = m.
 Proof.
   destruct m.
-  - induction n.
+  - simple_induction' n.
     + reflexivity.
     + assumption.
-  - induction n.
+  - simple_induction' n.
     + simpl. destruct (add_n_O m); reflexivity.
     + simpl. destruct (add_n_Sm m n). assumption.
 Defined.
@@ -226,17 +228,17 @@ Defined.
 
 Proposition n_leq_add_n_k (n m : nat) : n <= n + m.
 Proof.
-  induction n.
+  simple_induction n n IHn.
   - apply leq_0_n.
   - simpl; apply leq_S_n', IHn.
 Defined.
 
 Proposition n_leq_add_n_k' (n m : nat) : n <= m + n.
 Proof.
-  induction m.
+  simple_induction' m.
   - exact(leq_n n).
   - simpl. apply leq_S. assumption.
-Defined.    
+Defined.
 
 Proposition natineq0eq0 {n : nat} : n <= 0 -> n = 0.
 Proof.
@@ -247,9 +249,9 @@ Defined.
 
 Proposition subsubadd (n m k : nat) : n - (m + k) = n - m - k.
 Proof.
-  revert m k; induction n.
+  revert m k; simple_induction n n IHn.
   - reflexivity.
-  - intro m; induction m; intro k.
+  - intro m; destruct m; intro k.
     + change (0 + k) with k; reflexivity.
     + change (m.+1 + k) with (m + k).+1; apply IHn.
 Defined.
@@ -264,12 +266,12 @@ Defined.
 Definition nleqSm_dichot {n m : nat}
   : (n <= m.+1) -> sum (n <= m) (n = m.+1).
 Proof.
-  revert m; induction n.
+  revert m; simple_induction n n IHn.
   - intro. left. exact (leq_0_n m).
-  - induction m.
+  - destruct m.
     + intro l. apply leq_S_n, natineq0eq0 in l.
       right; apply ap; exact l.
-    + intro l. apply leq_S_n, IHn in l; induction l as [a | b].
+    + intro l. apply leq_S_n, IHn in l; destruct l as [a | b].
       * left. apply leq_S_n'; exact a.
       * right. apply ap; exact b.
 Defined.
@@ -288,7 +290,7 @@ Defined.
 
 Proposition sub_leq_0_converse (n m : nat) : n - m = 0 -> n <= m.
 Proof.
-  revert m; induction n.
+  revert m; simple_induction n n IHn.
   - auto with nat.
   - intros m eq. destruct m.
     + simpl in eq. apply symmetric_paths in eq.
@@ -306,9 +308,9 @@ Defined.
 
 Proposition lt_sub_gt_0 (n m : nat) : m < n -> 0 < n - m.
 Proof.
-  revert m; induction n.
+  revert m; simple_induction n n IHn.
   - intros m ineq. contradiction (not_lt_n_0 m).
-  - induction m.
+  - destruct m.
     + simpl. easy.
     + simpl. intro ineq. apply leq_S_n in ineq.
       now apply IHn in ineq.
@@ -317,10 +319,10 @@ Defined.
 Proposition natminuspluseq (n m : nat)
   : n <= m -> (m - n) + n = m.
 Proof.
-  revert m; induction n.
+  revert m; simple_induction n n IHn.
   - intros. destruct m; [reflexivity |]. simpl.
     apply (ap S), symmetric_paths, add_n_O.
-  - intros m l. induction m.
+  - intros m l. destruct m.
     + contradiction (not_leq_Sn_0 n).
     + simpl. apply leq_S_n, IHn in l.
       destruct (nat_add_n_Sm (m - n) n).
@@ -336,7 +338,7 @@ Proof.
   - apply n_lt_m_n_leq_m in g.
     now destruct (symmetric_paths _ _ (sub_leq_0 n m _)).
 Defined.
-    
+
 Proposition natminuspluseq' (n m : nat)
   : n <= m -> n + (m - n) = m.
 Proof.
@@ -363,7 +365,7 @@ Proposition nataddpreservesleq { n m k : nat }
   : n <= m -> n + k <= m + k.
 Proof.
   intro l.
-  induction k.
+  simple_induction k k IHk.
   - destruct (add_n_O n), (add_n_O m); exact l.
   - destruct (nat_add_n_Sm n k), (nat_add_n_Sm m k);
       apply leq_S_n'; exact IHk.
@@ -387,7 +389,7 @@ Proof.
   unfold "<".
   change (n + k).+1 with (n.+1 + k).
   generalize (n.+1). intros n' l.
-  induction k.
+  simple_induction k k IHk.
   - destruct (add_n_O n'), (add_n_O m); exact l.
   - destruct (nat_add_n_Sm n' k), (nat_add_n_Sm m k);
       apply leq_S_n'; exact IHk.
@@ -404,7 +406,7 @@ Defined.
 Proposition nataddreflectslt { n m k : nat }
   : n + k < m + k -> n < m.
 Proof.
-  induction k.
+  simple_induction k k IHk.
   - destruct (add_n_O n), (add_n_O m); trivial.
   - intro l. destruct (nat_add_n_Sm n k), (nat_add_n_Sm m k) in l.
     apply leq_S_n, IHk in l; exact l.
@@ -448,9 +450,9 @@ Defined.
 Proposition nataddsub_assoc_lemma {k m : nat}
   : (k <= m) -> m.+1 - k = (m - k).+1.
 Proof.
-  revert m; induction k.
+  revert m; simple_induction k k IHk.
   - intros m l; simpl. destruct m; reflexivity.
-  - induction m.
+  - destruct m.
     + simpl; intro g; contradiction (not_leq_Sn_0 _ g).
     + intro l; apply leq_S_n in l.
       change (m.+2 - k.+1) with (m.+1 - k).
@@ -461,7 +463,7 @@ Defined.
 Proposition nataddsub_assoc (n : nat) {m k : nat}
   : (k <= m) -> n + (m - k) = n + m - k.
 Proof.
-  revert m k. induction n.
+  revert m k. simple_induction n n IHn.
   - reflexivity.
   - intros m k l.
     change (n.+1 + (m - k)) with (n + (m - k)).+1;
@@ -492,9 +494,9 @@ Proposition nataddsub_comm_ineq_lemma (n m : nat)
   : n.+1 - m <= (n - m).+1.
 Proof.
   revert m.
-  induction n.
-  - induction m; [ apply leq_n | apply leq_S; apply leq_n ]. 
-  - intro m; induction m.
+  simple_induction n n IHn.
+  - simple_induction m m IHm; [ apply leq_n | apply leq_S; apply leq_n ]. 
+  - intro m; simple_induction m m IHm.
     + apply leq_n.
     + apply IHn.
 Defined.
@@ -502,7 +504,7 @@ Defined.
 Proposition nataddsub_comm_ineq (n m k : nat)
   : (n + k) - m <= (n - m) + k.
 Proof. 
-  induction k.
+  simple_induction k k IHk.
   - destruct (add_n_O n), (add_n_O (n - m)); constructor.
   - destruct (add_n_Sm n k).
     refine (leq_trans (nataddsub_comm_ineq_lemma (n+k) m) _).
@@ -524,9 +526,9 @@ Defined.
 Proposition i_lt_n_sum_m (n m i : nat)
   : i < n - m -> m <= n.
 Proof.
-  revert m i; induction n.
+  revert m i; simple_induction n n IHn.
   - intros m i l. simpl in l. contradiction (not_lt_n_0 _ _).
-  - intros m i l. induction m.
+  - intros m i l. destruct m.
     + apply leq_0_n.
     + apply leq_S_n'. simpl in l. apply (IHn m i l).
 Defined.
@@ -552,7 +554,7 @@ Defined.
 
 Proposition predeqminus1 { n : nat } : n - 1 = pred n.
 Proof.
-  induction n.
+  simple_induction' n.
   - reflexivity.
   - apply sub_n_0.
 Defined.
@@ -566,8 +568,7 @@ Defined.
 
 Proposition S_predn (n i: nat) : (i < n) -> S(pred n) = n.
 Proof.
-  intros l.
-  induction n.
+  simple_induction' n; intros l.
   - contradiction (not_lt_n_0 i).
   - reflexivity.
 Defined.
@@ -649,7 +650,7 @@ Defined.
 Proposition natsubpreservesleq { n m k : nat }
   : n <= m -> n - k <= m - k.
 Proof.
-  induction k.
+  simple_induction k k IHk.
   - destruct (symmetric_paths _ _ (sub_n_0 n)),
       (symmetric_paths _ _ (sub_n_0 m)); done.
   - intro l. change (k.+1) with (1 + k).
@@ -666,9 +667,9 @@ Defined.
 Proposition sub_less { n k : nat } : n - k <= n.
 Proof.
   revert k.
-  induction n.
+  simple_induction n n IHn.
   - intros; apply leq_0_n.
-  - induction k.
+  - destruct k.
     + apply leq_n.
     + simpl; apply (@leq_trans _ n _);
         [ apply IHn | apply leq_S, leq_n].
@@ -744,10 +745,10 @@ Defined.
 Proposition nat_add_bifunctor (n n' m m' : nat)
   : n <= m -> n' <= m' -> n + n' <= m + m'.
 Proof.
-  revert n' m m'; induction n.
+  revert n' m m'; simple_induction n n IHn.
   - intros n' m m' l l'. simpl.
     apply (leq_trans l'). exact (n_leq_add_n_k' m' m).
-  - intros n' m; induction m.
+  - intros n' m; destruct m.
     + intros. contradiction (not_leq_Sn_0 n).
     + intros m' l l'. apply leq_S_n in l. simpl.
       apply leq_S_n', IHn.
@@ -782,7 +783,7 @@ Proposition strong_induction (P : nat -> Type)
 Proof.
   intro a.
   assert (forall n m: nat, m < n -> P m) as X. {
-    induction n.
+    simple_induction n n IHn.
     - intros m l. contradiction (not_lt_n_0 m).
     - intros m l. apply leq_S_n in l.
       destruct l as [ | n].
@@ -816,9 +817,9 @@ Proof.
   - now constructor.
 Defined.
 
-Proposition increasing_geq_n_0 (n :nat) : increasing_geq n 0.
+Proposition increasing_geq_n_0 (n : nat) : increasing_geq n 0.
 Proof.
-  induction n.
+  simple_induction n n IHn.
   - constructor.
   - induction IHn.
     + constructor; now constructor.
@@ -828,7 +829,7 @@ Defined.
 Lemma increasing_geq_minus (n k : nat)
   : increasing_geq n (n - k).
 Proof.
-  induction k.
+  simple_induction k k IHk.
   - destruct (symmetric_paths _ _ (sub_n_0 n)); constructor.
   - destruct (@leq_dichot n k) as [l | g].
     + destruct (symmetric_paths _ _ (sub_leq_0 _ _ _)) in IHk.
@@ -854,7 +855,7 @@ Defined.
   
 Lemma ineq_sub (n m : nat) : n <= m -> m - (m - n) = n.
 Proof.
-  revert m; induction n.
+  revert m; simple_induction n n IHn.
   - intros. destruct (symmetric_paths _ _ (sub_n_0 m)),
       (symmetric_paths _ _ (sub_n_n m));
       reflexivity.
diff --git a/theories/Spaces/Nat/Core.v b/theories/Spaces/Nat/Core.v
index c3004256adc..e2171a9b00e 100644
--- a/theories/Spaces/Nat/Core.v
+++ b/theories/Spaces/Nat/Core.v
@@ -3,6 +3,8 @@ Require Import Basics Types.
 Require Export Basics.Nat.
 Require Export HoTT.DProp.
 
+Local Set Universe Minimization ToSet.
+
 Local Unset Elimination Schemes.
 
 Scheme nat_ind := Induction for nat Sort Type.
@@ -220,10 +222,10 @@ Defined.
 #[export] Hint Resolve not_eq_S : core.
 
 (** TODO: keep or remove? *)
-Definition IsSucc (n: nat) : Type :=
+Definition IsSucc (n: nat) : Type0 :=
   match n with
-  | O => False
-  | S p => True
+  | O => Empty
+  | S p => Unit
   end.
 
 (** Zero is not the successor of a number *)
@@ -236,7 +238,7 @@ Defined.
 
 Theorem not_eq_n_Sn : forall n:nat, n <> S n.
 Proof.
-  induction n; auto.
+  simple_induction' n; auto.
 Defined.
 #[export] Hint Resolve not_eq_n_Sn : core.
 
@@ -247,7 +249,7 @@ Local Definition ap011_nat := @ap011 nat nat.
 
 Lemma add_n_O : forall (n : nat), n = n + 0.
 Proof.
-  induction n; simpl; auto.
+  simple_induction' n; simpl; auto.
 Defined.
 #[export] Hint Resolve add_n_O : core.
 
@@ -258,7 +260,7 @@ Defined.
 
 Lemma add_n_Sm : forall n m:nat, S (n + m) = n + S m.
 Proof.
-  intros n m; induction n; simpl; auto.
+  simple_induction' n; simpl; auto.
 Defined.
 #[export] Hint Resolve add_n_Sm: core.
 
@@ -274,13 +276,13 @@ Local Definition ap011_mul := @ap011 _ _ _  mul.
 
 Lemma mul_n_O : forall n:nat, 0 = n * 0.
 Proof.
-  induction n; simpl; auto.
+  simple_induction' n; simpl; auto.
 Defined.
 #[export] Hint Resolve mul_n_O : core.
 
 Lemma mul_n_Sm : forall n m:nat, n * m + n = n * S m.
 Proof.
-  intros; induction n as [| p H]; simpl; auto.
+  intros; simple_induction n p H; simpl; auto.
   destruct H; rewrite <- add_n_Sm; apply ap.
   pattern m at 1 3; elim m; simpl; auto.
 Defined.
@@ -295,7 +297,7 @@ Notation mul_succ_r_reverse := mul_n_Sm (only parsing).
 
 (** *** Boolean equality and its properties *)
 
-Fixpoint code_nat (m n : nat) {struct m} : DHProp :=
+Fixpoint code_nat (m n : nat) {struct m} : DHProp@{Set} :=
   match m, n with
   | 0, 0 => True
   | m'.+1, n'.+1 => code_nat m' n'
@@ -341,7 +343,7 @@ Global Instance hset_nat : IsHSet nat := _.
 
 (** ** Inequality of natural numbers *)
 
-Inductive leq (n : nat) : nat -> Type0 :=
+Cumulative Inductive leq (n : nat) : nat -> Type0 :=
 | leq_n : leq n n
 | leq_S : forall m, leq n m -> leq n (S m).
 
@@ -385,7 +387,7 @@ Global Existing Instance leq_S_n' | 100.
 
 Lemma not_leq_Sn_n n : ~ (n.+1 <= n).
 Proof.
-  induction n.
+  simple_induction n n IHn.
   { intro p.
     inversion p. }
   intros p.
@@ -395,7 +397,7 @@ Defined.
 (** A general form for injectivity of this constructor *)
 Definition leq_n_inj_gen n k (p : n <= k) (r : n = k) : p = r # leq_n n.
 Proof.
-  induction p.
+  destruct p.
   + assert (c : idpath = r) by apply path_ishprop.
     destruct c.
     reflexivity.
@@ -411,7 +413,7 @@ Fixpoint leq_S_inj_gen n m k (p : n <= k) (q : n <= m) (r : m.+1 = k)
   : p = r # leq_S n m q.
 Proof.
   revert m q r.
-  induction p.
+  destruct p.
   + intros k p r.
     destruct r.
     contradiction (not_leq_Sn_n _ p).
@@ -442,7 +444,7 @@ Defined.
 
 Global Instance leq_0_n n : 0 <= n | 10.
 Proof.
-  induction n; auto.
+  simple_induction' n; auto.
 Defined.
 
 Lemma not_leq_Sn_0 n : ~ (n.+1 <= 0).
@@ -461,7 +463,7 @@ Defined.
 Global Instance decidable_leq n m : Decidable (n <= m).
 Proof.
   revert n.
-  induction m; intros n.
+  simple_induction' m; intros n.
   - destruct n.
     + left; exact _.
     + right; apply not_leq_Sn_0.
@@ -511,7 +513,7 @@ Defined.
 
 (** We define the less-than relation [lt] in terms of [leq] *)
 Definition lt n m : Type0 := leq (S n) m.
-             
+
 (** We declare it as an existing class so typeclass search is performed on its goals. *)
 Existing Class lt.
 #[export] Hint Unfold lt : core typeclass_instances.
@@ -561,7 +563,7 @@ Theorem nat_double_ind (R : nat -> nat -> Type)
   (H3 : forall n m, R n m -> R (S n) (S m))
   : forall n m:nat, R n m.
 Proof.
-  induction n; auto.
+  simple_induction' n; auto.
   destruct m; auto.
 Defined.
 
@@ -569,19 +571,19 @@ Defined.
 
 Lemma max_n_n n : max n n = n.
 Proof.
-  induction n; cbn; auto.
+  simple_induction' n; cbn; auto.
 Defined.
 #[export] Hint Resolve max_n_n : core.
 
 Lemma max_Sn_n n : max (S n) n = S n.
 Proof.
-  induction n; cbn; auto.
+  simple_induction' n; cbn; auto.
 Defined.
 #[export] Hint Resolve max_Sn_n : core.
 
 Lemma max_comm n m : max n m = max m n.
 Proof.
-  revert m; induction n; destruct m; cbn; auto.
+  revert m; simple_induction' n; destruct m; cbn; auto.
 Defined.
 
 Lemma max_0_n n : max 0 n = n.
@@ -598,7 +600,7 @@ Defined.
 
 Theorem max_l : forall n m, m <= n -> max n m = n.
 Proof.
-  intros n m; revert n; induction m; auto.
+  intros n m; revert n; simple_induction m m IHm; auto.
   intros [] p.
   1: inversion p.
   cbn; by apply ap_S, IHm, leq_S_n.
@@ -611,12 +613,12 @@ Defined.
 
 Lemma min_comm : forall n m, min n m = min m n.
 Proof.
-  induction n; destruct m; cbn; auto.
-Defined. 
+  simple_induction' n; destruct m; cbn; auto.
+Defined.
 
 Theorem min_l : forall n m : nat, n <= m -> min n m = n.
 Proof.
-  intros n m; revert m; induction n; auto.
+  simple_induction n n IHn; auto.
   intros [] p.
   1: inversion p.
   cbn; by apply ap_S, IHn, leq_S_n.
@@ -638,14 +640,14 @@ Notation nat_iter n f x
 Lemma nat_iter_succ_r n {A} (f : A -> A) (x : A)
   : nat_iter (S n) f x = nat_iter n f (f x).
 Proof.
-  induction n as [|n IHn]; simpl; trivial.
+  simple_induction n n IHn; simpl; trivial.
   exact (ap f IHn).
 Defined.
 
 Theorem nat_iter_add (n m : nat) {A} (f : A -> A) (x : A)
   : nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).
 Proof.
-  induction n as [|n IHn]; simpl; trivial.
+  simple_induction n n IHn; simpl; trivial.
   exact (ap f IHn).
 Defined.
 
@@ -653,7 +655,7 @@ Defined.
 Theorem nat_iter_invariant (n : nat) {A} (f : A -> A) (P : A -> Type)
   : (forall x, P x -> P (f x)) -> forall x, P x -> P (nat_iter n f x).
 Proof.
-  induction n as [|n IHn]; simpl; trivial.
+  simple_induction n n IHn; simpl; trivial.
   intros Hf x Hx.
   apply Hf, IHn; trivial.
 Defined.
@@ -662,14 +664,14 @@ Defined.
 
 Lemma nat_add_n_Sm (n m : nat) : (n + m).+1 = n + m.+1.
 Proof.
-  induction n; simpl.
+  simple_induction' n; simpl.
   - reflexivity.
   - apply ap; assumption.
 Defined.
 
 Definition nat_add_comm (n m : nat) : n + m = m + n.
 Proof.
-  induction n as [|n IHn]; simpl.
+  simple_induction n n IHn; simpl.
   - exact (add_n_O m).
   - transitivity (m + n).+1.
     + apply ap, IHn.
@@ -713,12 +715,12 @@ Definition leq_1_Sn {n} : 1 <= n.+1 := leq_S_n' 0 n (leq_0_n _).
 
 Fixpoint leq_dichot {m} {n} : (m <= n) + (m > n).
 Proof.
-  induction m, n.
+  simple_induction' m; simple_induction' n.
   - left; reflexivity.
   - left; apply leq_0_n.
   - right; unfold lt; apply leq_1_Sn.
   - assert ((m <= n) + (n < m)) as X by apply leq_dichot.
-    induction X as [leqmn|ltnm].
+    destruct X as [leqmn|ltnm].
     + left; apply leq_S_n'; assumption.
     + right; apply leq_S_n'; assumption.
 Defined.

From 0fe81264303638f732e9c5e7de30064c28693bff Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 16 Jan 2024 15:04:36 -0500
Subject: [PATCH 7/7] Truncations/Connectedness: Universe Min ToSet simplifies
 two results

---
 theories/Truncations/Connectedness.v | 20 +++++++++-----------
 1 file changed, 9 insertions(+), 11 deletions(-)

diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v
index b84d0244e05..8da52663d54 100644
--- a/theories/Truncations/Connectedness.v
+++ b/theories/Truncations/Connectedness.v
@@ -9,6 +9,9 @@ Require Export Modalities.Modality.        (* [Export] since the actual definiti
 Require Import Modalities.Descent.
 Require Import Truncations.Core Truncations.SeparatedTrunc.
 
+(** This reduces universe variables in [conn_pointed_type] and [conn_point_elim], which refer to [Unit]. *)
+Local Set Universe Minimization ToSet.
+
 Local Open Scope path_scope.
 Local Open Scope trunc_scope.
 
@@ -63,25 +66,20 @@ Defined.
 (** The connectivity of a pointed type and (the inclusion of) its point are intimately connected. *)
 
 (** We can't make both of these [Instance]s, as that would result in infinite loops. *)
+
 Global Instance conn_pointed_type@{u} {n : trunc_index} {A : Type@{u}} (a0:A)
-       `{IsConnMap n _ _ (unit_name a0)}
+  `{IsConnMap n _ _ (unit_name a0)}
   : IsConnected n.+1 A | 1000.
 Proof.
   apply isconnected_conn_map_to_unit.
-  (* Coq can find [conn_map_to_unit_isconnected] and [isconnected_contr] via typeclass search, but we manually pose them to get rid of an unneeded universe variable. *)
-  pose conn_map_to_unit_isconnected@{u u}.
-  pose isconnected_contr@{u u}.
-  apply (OO_cancelR_conn_map@{u u u u} (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
+  apply (OO_cancelR_conn_map (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
 Defined.
 
-Definition conn_point_incl `{Univalence} {n : trunc_index} {A : Type@{u}} (a0:A)
-           `{IsConnected n.+1 A}
+Definition conn_point_incl `{Univalence} {n : trunc_index} {A : Type} (a0:A)
+  `{IsConnected n.+1 A}
   : IsConnMap n (unit_name a0).
 Proof.
-  (* Coq can find [conn_map_to_unit_isconnected] and [isconnected_contr] via typeclass search, but we manually pose them to get rid of an unneeded universe variable. *)
-  pose conn_map_to_unit_isconnected@{u u}.
-  pose isconnected_contr@{u u}.
-  rapply (OO_cancelL_conn_map@{u u u u} (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
+  rapply (OO_cancelL_conn_map (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
   apply O_lex_leq_Tr.
 Defined.