Overlay for PR#21164

Author: tabareau

theories/Basics/Trunc.v

@@ -420,6 +420,10 @@ Arguments trunctype_istrunc [_] _.
 
 Coercion trunctype_type : TruncType >-> Sortclass.
 
+(* This hint is required to be able to use cumulativity of inductive types together with first-order approximation for polymorphic hints. *)
+Hint Extern 100 (IsTrunc_internal (trunctype_type ?A) _)
+  => (exact (trunctype_istrunc A)) : typeclass_instances.
+
 Notation "n -Type" := (TruncType n) : type_scope.
 Notation HProp := (-1)-Type.
 Notation HSet := 0-Type.

theories/Homotopy/InjectiveTypes/InjectiveTypes.v

@@ -368,8 +368,8 @@ Proof.
   assert (embId : IsEmbedding (fun a : A => a)) by rapply istruncmap_mapinO_tr.
   pose proof (mD := Di (X * A) (Y * A) (functor_prod j equiv_idmap)
     (istruncmap_functor_prod@{u v t t ut vt uvt uvt uv t} _ _ _) (uncurry f)).
-  revert mD.
-  rapply Trunc_rec@{utvw utvw}.
+  pose proof (HP := _ : IsHProp (merely@{utvw} {f' : Y -> A -> D & (fun x : X => f' (j x)) == f})).
+  rapply (Trunc_rec@{utvw utvw} (IsTrunc0 := HP) _ mD).
   intros [g e].
   apply tr.
   refine (fun y a => g (y, a); _).

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.