Merge pull request #2318 from jdchristensen/trunc-universes

Changes for Rocq PR#21164

Author: jdchristensen

contrib/HoTTBookExercises.v

@@ -1109,7 +1109,7 @@ Defined.
 Definition Book_3_10_LEM@{j} := forall A : HProp@{j}, A + ~ A.
 
 Definition Book_3_10_Lift@{i j | i < j} (A : HProp@{i}) : HProp@{j}
-  := Build_HProp A.
+  := @Build_HProp A (trunctype_istrunc A).
 
 Definition Book_3_10_impred@{i j k | i < j, j < k} `{Univalence}
   (LEM : Book_3_10_LEM@{j})

theories/Algebra/Rings/Matrix.v

@@ -667,7 +667,7 @@ Class IsUpperTriangular@{i} {R : Ring@{i}} {n : nat} (M : Matrix@{i} R n n) : Ty
 Instance ishprop_isuppertriangular@{i} {R : Ring@{i}} {n : nat} (M : Matrix R n n)
   : IsHProp (IsUpperTriangular M).
 Proof.
-  apply istrunc_truncation@{i i}.
+  apply istrunc_truncation@{i}.
 Defined.
 
 (** A matrix is lower triangular if all the entries above the diagonal are zero. We define it as the transpose being upper triangular. *)
@@ -678,7 +678,7 @@ Instance ishprop_islowertriangular@{i} {R : Ring@{i}} {n : nat}
   (M : Matrix R n n)
   : IsHProp (IsLowerTriangular M).
 Proof.
-  apply istrunc_truncation@{i i}.
+  apply istrunc_truncation@{i}.
 Defined.
 
 (** The transpose of a matrix is lower triangular if and only if the matrix is upper triangular. *)

theories/Modalities/Meet.v

@@ -296,7 +296,7 @@ Section LexMeet.
     apply mapinO_compose.
     2:rapply mapinO_isequiv.
     apply IHn.
-    - rapply mapinO_diagonal.
+    - apply mapinO_diagonal.
       pose (O_eq_Tr n.+1).
       rapply (mapinO_O_leq _ (Sep (Tr n.+1))).
     - apply plusconnmap_diagonal; assumption.

theories/Truncations/Core.v

@@ -28,9 +28,9 @@ Module Export Trunc.
     tr : A -> Trunc n A.
   Arguments tr {n A} a.
 
-  (** Without explicit universe parameters, this instance is insufficiently polymorphic. *)
-  #[export] Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
-    : IsTrunc@{j} n (Trunc@{i} n A).
+  (** Because [IsTrunc] is cumulative, we can use only one universe variable here. *)
+  #[export] Instance istrunc_truncation@{i} (n : trunc_index) (A : Type@{i})
+    : IsTrunc@{i} n (Trunc@{i} n A).
   Admitted.
 
   Definition Trunc_ind {n A}

theories/Universes/DProp.v

@@ -134,7 +134,7 @@ Proof.
   - intros P; unfold dprop_to_bool.
     destruct (dec P); symmetry; apply path_dprop, path_universe_uncurried.
     + apply if_hprop_then_equiv_Unit; [ exact _ | assumption ].
-    + apply if_not_hprop_then_equiv_Empty; [ exact _ | assumption ].
+    + apply if_not_hprop_then_equiv_Empty; assumption.
 Defined.
 
 Definition equiv_dprop_to_bool `{Univalence}

theories/Universes/HProp.v

@@ -128,12 +128,9 @@ Proof.
   - exact (fun _ => p).
 Defined.
 
-(** If an hprop is not inhabited, then it is equivalent to [Empty]. *)
-Lemma if_not_hprop_then_equiv_Empty (hprop : Type) `{IsHProp hprop} : ~hprop -> hprop <~> Empty.
-Proof.
-  intro np.
-  exact (Build_Equiv _ _ np _).
-Defined.
+(** If an hprop is not inhabited, then it is equivalent to [Empty]. Note that we'd don't need the assumption that the type is an hprop here. *)
+Definition if_not_hprop_then_equiv_Empty (hprop : Type) : ~hprop -> hprop <~> Empty
+  := equiv_to_empty.
 
 (** Thus, a decidable hprop is either equivalent to [Unit] or [Empty]. *)
 Definition equiv_decidable_hprop (hprop : Type)