From de84aa6d0f75f3a1358c36f3160b6a2b1c235cc0 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 6 Feb 2023 17:24:31 -0500
Subject: [PATCH 1/3] Make entire library Cumulative (build fails)

---
 theories/Algebra/Universal/Homomorphism.v | 3 ++-
 theories/Basics/Logic.v                   | 1 +
 theories/Modalities/Descent.v             | 2 ++
 3 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/theories/Algebra/Universal/Homomorphism.v b/theories/Algebra/Universal/Homomorphism.v
index 4a05d4f462b..2edf6947600 100644
--- a/theories/Algebra/Universal/Homomorphism.v
+++ b/theories/Algebra/Universal/Homomorphism.v
@@ -36,7 +36,8 @@ Section is_homomorphism.
   Qed.
 End is_homomorphism.
 
-Record Homomorphism {σ} {A B : Algebra σ} : Type := Build_Homomorphism
+(* We make this NonCumulative so that the proof of [homomorphism_id] goes through smoothly. *)
+NonCumulative Record Homomorphism {σ} {A B : Algebra σ} : Type := Build_Homomorphism
   { def_homomorphism : forall (s : Sort σ), A s -> B s
   ; is_homomorphism : IsHomomorphism def_homomorphism }.
 
diff --git a/theories/Basics/Logic.v b/theories/Basics/Logic.v
index e6956522a71..6f447480ca0 100644
--- a/theories/Basics/Logic.v
+++ b/theories/Basics/Logic.v
@@ -15,6 +15,7 @@ Set Implicit Arguments.
 Require Export Basics.Notations.
 
 Global Set Universe Polymorphism.
+Global Set Polymorphic Inductive Cumulativity.
 Global Set Asymmetric Patterns.
 
 Notation "A -> B" := (forall (_ : A), B) : type_scope.
diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v
index a6c6bdba951..7e70d4b473c 100644
--- a/theories/Modalities/Descent.v
+++ b/theories/Modalities/Descent.v
@@ -142,6 +142,8 @@ Proof.
 Defined.
 
 (** We can also state it in terms of belonging to a subuniverse if we lift [O'] accessibly (an analogue of Theorem 3.11(iii) of RSS). *)
+(* *** TODO: With Cumulativity turned on globally, this produces a universe error.
+   It doesn't help to make the two Classes defined in this file NonCumulative. *)
 Global Instance inO_TypeO_lex_leq `{Univalence} `{IsAccRSU O'}
   : In (lift_accrsu O') (Type_ O)
   := fun i => ooextendable_TypeO_lex_leq (acc_lgen O' i).

From 9161725a31c497065ea06aad291dbfc5acb18c8f Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Mon, 6 Feb 2023 17:26:57 -0500
Subject: [PATCH 2/3] Remove redundant Cumulative keywords

---
 theories/Algebra/AbGroups/AbelianGroup.v       | 2 --
 theories/Algebra/Groups/Group.v                | 2 --
 theories/Basics/Datatypes.v                    | 2 --
 theories/Basics/Overture.v                     | 2 --
 theories/Classes/interfaces/abstract_algebra.v | 2 --
 theories/Cubical/PathCube.v                    | 2 +-
 theories/Cubical/PathSquare.v                  | 2 +-
 theories/Modalities/Localization.v             | 2 +-
 theories/Pointed/Core.v                        | 2 --
 theories/Truncations/Core.v                    | 2 +-
 10 files changed, 4 insertions(+), 16 deletions(-)

diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index 485e69938e9..55a3267525e 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -6,8 +6,6 @@ Require Export Algebra.Groups.Subgroup.
 Require Import Algebra.Groups.QuotientGroup.
 Require Import WildCat.
 
-Local Set Polymorphic Inductive Cumulativity.
-
 Local Open Scope mc_scope.
 Local Open Scope mc_add_scope.
 
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index e4789ffc04b..03d3c993a43 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -20,8 +20,6 @@ Require Import WildCat.
 Require Import Spaces.Nat.Core.
 Require Import Truncations.Core.
 
-Local Set Polymorphic Inductive Cumulativity.
-
 Generalizable Variables G H A B C f g.
 
 Declare Scope group_scope.
diff --git a/theories/Basics/Datatypes.v b/theories/Basics/Datatypes.v
index 4830b363ac8..b8b1a066730 100644
--- a/theories/Basics/Datatypes.v
+++ b/theories/Basics/Datatypes.v
@@ -18,8 +18,6 @@ Global Set Primitive Projections.
 Global Set Nonrecursive Elimination Schemes.
 Local Unset Elimination Schemes.
 
-Local Set Polymorphic Inductive Cumulativity.
-
 (** [option A] is the extension of [A] with an extra element [None] *)
 
 Inductive option (A : Type) : Type :=
diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index 5d7d7d4ae65..da2a4cedcf1 100644
--- a/theories/Basics/Overture.v
+++ b/theories/Basics/Overture.v
@@ -13,8 +13,6 @@ Create HintDb rewrite discriminated.
 #[export] Hint Variables Opaque : rewrite.
 Create HintDb typeclass_instances discriminated.
 
-Local Set Polymorphic Inductive Cumulativity.
-
 (** ** Type classes *)
 
 (** This command prevents Coq from trying to guess the values of existential variables while doing typeclass resolution.  If you don't know what that means, ignore it. *)
diff --git a/theories/Classes/interfaces/abstract_algebra.v b/theories/Classes/interfaces/abstract_algebra.v
index 99a9b4d564d..049cc74bcc3 100644
--- a/theories/Classes/interfaces/abstract_algebra.v
+++ b/theories/Classes/interfaces/abstract_algebra.v
@@ -2,8 +2,6 @@ Require Import Spaces.Nat.Core.
 Require Export HoTT.Classes.interfaces.canonical_names.
 Require Import Modalities.ReflectiveSubuniverse.
 
-Local Set Polymorphic Inductive Cumulativity.
-
 Generalizable Variables A B f g x y.
 
 (* 
diff --git a/theories/Cubical/PathCube.v b/theories/Cubical/PathCube.v
index 936cf1ea55f..79de992e55c 100644
--- a/theories/Cubical/PathCube.v
+++ b/theories/Cubical/PathCube.v
@@ -40,7 +40,7 @@ x011   |               |          x011----pi11----x111   |
 
 (* Homogeneous cubes *)
 (* PathCube left right top bottom front back *)
-Cumulative Inductive PathCube {A}
+Inductive PathCube {A}
   : forall x000 {x010 x100 x110 x001 x011 x101 x111 : A}
   {p0i0 : x000 = x010} {p1i0 : x100 = x110} {pi00 : x000 = x100}
   {pi10 : x010 = x110} {p0i1 : x001 = x011} {p1i1 : x101 = x111}
diff --git a/theories/Cubical/PathSquare.v b/theories/Cubical/PathSquare.v
index 8d8896c80f2..752f0434d0f 100644
--- a/theories/Cubical/PathSquare.v
+++ b/theories/Cubical/PathSquare.v
@@ -36,7 +36,7 @@ Local Unset Elimination Schemes.
 
 (* Definition of PathSquare *)
 (* PathSquare left right up down *)
-Cumulative Inductive PathSquare {A} : forall a00 {a10 a01 a11 : A},
+Inductive PathSquare {A} : forall a00 {a10 a01 a11 : A},
   a00 = a10 -> a01 = a11 -> a00 = a01 -> a10 = a11 -> Type
   := sq_id : forall {x : A},
     PathSquare x 1 1 1 1.
diff --git a/theories/Modalities/Localization.v b/theories/Modalities/Localization.v
index ee7edc0f1a8..885cb846426 100644
--- a/theories/Modalities/Localization.v
+++ b/theories/Modalities/Localization.v
@@ -267,7 +267,7 @@ Defined.
 
 Module Export LocalizationHIT.
 
-  Cumulative Private Inductive Localize (f : LocalGenerators@{a}) (X : Type@{i})
+  Private Inductive Localize (f : LocalGenerators@{a}) (X : Type@{i})
   : Type@{max(a,i)} :=
   | loc : X -> Localize f X.
 
diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index ccc4d84ac5c..a64316e1dc4 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -6,8 +6,6 @@ Require Import Truncations.Core.
 Require Import ReflectiveSubuniverse.
 Require Import Extensions.
 
-Local Set Polymorphic Inductive Cumulativity.
-
 Declare Scope pointed_scope.
 
 Local Open Scope pointed_scope.
diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
index 9a7a637c6b0..83b4cc01d2a 100644
--- a/theories/Truncations/Core.v
+++ b/theories/Truncations/Core.v
@@ -27,7 +27,7 @@ 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 :=
+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.

From 4666c4bbff87c7761b865cbb2cc6bd378ee955fe Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Fri, 16 Feb 2024 11:52:33 -0500
Subject: [PATCH 3/3] Mild progress on cumulative inductives

---
 theories/Algebra/Universal/Homomorphism.v | 2 +-
 theories/HIT/quotient.v                   | 1 +
 theories/Modalities/Accessible.v          | 3 ++-
 theories/Modalities/Localization.v        | 4 ++--
 theories/TruncType.v                      | 9 +++++----
 5 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/theories/Algebra/Universal/Homomorphism.v b/theories/Algebra/Universal/Homomorphism.v
index 2edf6947600..68675966962 100644
--- a/theories/Algebra/Universal/Homomorphism.v
+++ b/theories/Algebra/Universal/Homomorphism.v
@@ -36,7 +36,7 @@ Section is_homomorphism.
   Qed.
 End is_homomorphism.
 
-(* We make this NonCumulative so that the proof of [homomorphism_id] goes through smoothly. *)
+(* We make this NonCumulative so that the proof of [homomorphism_id] goes through smoothly. TODO: remove this. *)
 NonCumulative Record Homomorphism {σ} {A B : Algebra σ} : Type := Build_Homomorphism
   { def_homomorphism : forall (s : Sort σ), A s -> B s
   ; is_homomorphism : IsHomomorphism def_homomorphism }.
diff --git a/theories/HIT/quotient.v b/theories/HIT/quotient.v
index b42e68a37d9..dad60841220 100644
--- a/theories/HIT/quotient.v
+++ b/theories/HIT/quotient.v
@@ -84,6 +84,7 @@ Section Equiv.
     intros. eapply concat;[apply transport_const|].
     apply path_forall. intro z. apply path_hprop; simpl.
     apply @equiv_iff_hprop; eauto.
+    (** Some universe annotations needed above for typeclass instance istrunc_trunctype. *)
   Defined.
 
   Context {Hrefl : Reflexive R}.
diff --git a/theories/Modalities/Accessible.v b/theories/Modalities/Accessible.v
index 582a358a17f..fcfc14aa854 100644
--- a/theories/Modalities/Accessible.v
+++ b/theories/Modalities/Accessible.v
@@ -27,7 +27,8 @@ Coercion lgenerator : LocalGenerators >-> Funclass.
 
 (** We put this definition in a module so that no one outside of this file will use it accidentally.  It will be redefined in [Localization] to refer to the localization reflective subuniverse, which is judgmentally the same but will also pick up typeclass inference for [In]. *)
 Module Import IsLocal_Internal.
-  Definition IsLocal f X :=
+  (* TODO: reorder these universe variables; make it land in v. Currently done this way for backwards compatibility, to keep diff small. *)
+  Definition IsLocal@{u v a | u <= v, a <= v} (f : LocalGenerators@{a}) (X : Type@{u}) :=
     (forall (i : lgen_indices f), ooExtendableAlong (f i) (fun _ => X)).
 End IsLocal_Internal.
 
diff --git a/theories/Modalities/Localization.v b/theories/Modalities/Localization.v
index 885cb846426..2a2f9933b9d 100644
--- a/theories/Modalities/Localization.v
+++ b/theories/Modalities/Localization.v
@@ -337,7 +337,7 @@ Section Localization.
 
 End Localization.
 
-Definition Loc@{a i} (f : LocalGenerators@{a}) : ReflectiveSubuniverse@{i}.
+Definition Loc@{a i | a <= i} (f : LocalGenerators@{a}) : ReflectiveSubuniverse@{i}.
 Proof.
   snrefine (Build_ReflectiveSubuniverse
                                  (Build_Subuniverse (IsLocal f) _ _)
@@ -422,7 +422,7 @@ Proof.
 Defined.
 
 (** Conversely, if a subuniverse is accessible, then the corresponding localization subuniverse is equivalent to it, and moreover exists at every universe level and satisfies its computation rules judgmentally.  This is called [lift_accrsu] but in fact it works equally well to *lower* the universe level, as long as both levels are no smaller than the size [a] of the generators. *)
-Definition lift_accrsu@{a i j} (O : Subuniverse@{i}) `{IsAccRSU@{a i} O}
+Definition lift_accrsu@{a i j | a <= i, a <= j} (O : Subuniverse@{i}) `{IsAccRSU@{a i} O}
   : ReflectiveSubuniverse@{j}
   := Loc@{a j} (acc_lgen O).
 
diff --git a/theories/TruncType.v b/theories/TruncType.v
index 4a273775d18..499785302fa 100644
--- a/theories/TruncType.v
+++ b/theories/TruncType.v
@@ -38,9 +38,9 @@ Section TruncType.
     : (A <~> B) <~> (A = B :> TruncType n)
     := equiv_path_trunctype' _ _ oE equiv_path_universe _ _.
 
-  Definition path_trunctype@{a b} {n : trunc_index} {A B : TruncType n}
+  Definition path_trunctype {n : trunc_index} {A B : TruncType n}
     : A <~> B -> (A = B :> TruncType n)
-  := equiv_path_trunctype@{a b} A B.
+  := equiv_path_trunctype A B.
 
   Global Instance isequiv_path_trunctype {n : trunc_index} {A B : TruncType n}
     : IsEquiv (@path_trunctype n A B) := _.
@@ -99,7 +99,7 @@ Section TruncType.
   Proof.
     apply istrunc_S.
     intros A B.
-    refine (istrunc_equiv_istrunc _ (equiv_path_trunctype@{i j} A B)).
+    refine (istrunc_equiv_istrunc _ (equiv_path_trunctype A B)).
     case n as [ | n'].
     - apply contr_equiv_contr_contr. (* The reason is different in this case. *)
     - apply istrunc_equiv.
@@ -110,7 +110,8 @@ Section TruncType.
   Global Instance istrunc_sig_istrunc : forall n, IsTrunc n.+1 { A : Type & IsTrunc n A } | 0.
   Proof.
     intro n.
-    apply (istrunc_equiv_istrunc _ issig_trunctype^-1).
+    nrefine (istrunc_equiv_istrunc _ issig_trunctype^-1).
+    exact istrunc_trunctype. (* To get universe variables to match, we do this as a separate step. *)
   Defined.
 
   (** ** Some standard inhabitants *)