Try to make entire library Cumulative

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.
 

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.

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. 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 }.
 

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 :=

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.

theories/Basics/Overture.v

@@ -13,8 +13,6 @@
 #[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. *)
@@ -131,11 +129,11 @@
 
 (** We make the parameters maximally inserted so that we can pass around [pr1] as a function and have it actually mean "first projection" in, e.g., [ap]. *)
 
 Arguments exist {A}%type P%type _ _.
 Arguments proj1 {A P} _ / .
 Arguments proj2 {A P} _ / .
 
 Arguments sig (A P)%type.
 
 Notation "{ x | P }" := (sig (fun x => P)) : type_scope.
 Notation "{ x : A | P }" := (sig (A := A) (fun x => P)) : type_scope.
@@ -192,7 +190,7 @@
 (** Dependent composition of functions. *)
 Definition composeD {A B C} (g : forall b, C b) (f : A -> B) := fun x : A => g (f x).
 
 Global Arguments composeD {A B C}%type_scope (g f)%function_scope x.
 
 #[export] Hint Unfold composeD : core.
 
@@ -322,7 +320,7 @@
   := match p with idpath => u end.
 
 (** See above for the meaning of [simpl nomatch]. *)
 Arguments transport {A}%type_scope P%function_scope {x y} p%path_scope u : simpl nomatch.
 
 (** Transport is very common so it is worth introducing a parsing notation for it.  However, we do not use the notation for output because it hides the fibration, and so makes it very hard to read involved transport expression. *)
 Notation "p # x" := (transport _ p x) (only parsing) : path_scope.
@@ -335,8 +333,8 @@
 Local Lemma define_internal_paths_rew_r A x y P (u : P y) (H : x = y :> A) : P x.
 Proof. rewrite -> H. exact u. Defined.
 
 Arguments internal_paths_rew {A%type_scope} {a} P%function_scope f {a0} p.
 Arguments internal_paths_rew_r {A%type_scope} {a y} P%function_scope HC X.
 
 (** Having defined transport, we can use it to talk about what a homotopy theorist might see as "paths in a fibration over paths in the base"; and what a type theorist might see as "heterogeneous equality in a dependent type".  We will first see this appearing in the type of [apD]. *)
 
@@ -345,7 +343,7 @@
 Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
   := match p with idpath => idpath end.
 
 Global Arguments ap {A B}%type_scope f%function_scope {x y} p%path_scope.
 
 Register ap as core.identity.congr.
 
@@ -379,7 +377,7 @@
   intros ? ? p ?; symmetry; apply p.
 Defined.
 
 Global Arguments pointwise_paths {A}%type_scope {P} (f g)%function_scope.
 Global Arguments reflexive_pointwise_paths /.
 Global Arguments transitive_pointwise_paths /.
 Global Arguments symmetric_pointwise_paths /.
@@ -393,12 +391,12 @@
   : f == g
   := fun x => match h with idpath => 1 end.
 
 Global Arguments apD10 {A%type_scope B} {f g}%function_scope h%path_scope _.
 
 Definition ap10 {A B} {f g:A->B} (h:f=g) : f == g
   := apD10 h.
 
 Global Arguments ap10 {A B}%type_scope {f g}%function_scope h%path_scope _.
 
 (** For the benefit of readers of the HoTT Book: *)
 Notation happly := ap10 (only parsing).
@@ -607,7 +605,7 @@
 (** TODO: Once Coq 8.18 is the minimum, prefix the next line with
 #[warning="-uniform-inheritance"] 
 *)
 Coercion istrunc_fun : IsTrunc >-> Funclass.
 
 (** *** Truncated relations  *)
 

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.
 
 (* 

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}

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.

theories/HIT/quotient.v

@@ -84,7 +84,8 @@
     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}.
 

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.
 

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).

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.
 
@@ -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).
 

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.

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 *)

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.