Mild progress on cumulative inductives

Author: jdchristensen

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

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

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

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