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.