diff --git a/contrib/HoTTBook.v b/contrib/HoTTBook.v
index 4599dae0d2b..ab653d5904f 100644
--- a/contrib/HoTTBook.v
+++ b/contrib/HoTTBook.v
@@ -330,7 +330,7 @@ Definition Book_2_15_7 := @HoTT.Types.Sigma.isequiv_sig_coind.
 (* ================================================== defn:set *)
 (** Definition 3.1.1 *)
 
-Definition Book_3_1_1 := @HoTT.Basics.Overture.IsTrunc 0.
+Definition Book_3_1_1 := fun A => @HoTT.Basics.Overture.IsTrunc 0 A.
 
 (* ================================================== eg:isset-unit *)
 (** Example 3.1.2 *)
@@ -340,7 +340,7 @@ Definition Book_3_1_2 := @HoTT.Types.Unit.contr_unit.
 (* ================================================== eg:isset-empty *)
 (** Example 3.1.3 *)
 
-Definition Book_3_1_3 := @HoTT.Types.Empty.hprop_Empty.
+Definition Book_3_1_3 := @HoTT.Types.Empty.istrunc_Empty (-2).
 
 (* ================================================== thm:nat-set *)
 (** Example 3.1.4 *)
@@ -355,12 +355,12 @@ Definition Book_3_1_5 := @HoTT.Types.Prod.istrunc_prod.
 (* ================================================== thm:isset-forall *)
 (** Example 3.1.6 *)
 
-Definition Book_3_1_6 := @HoTT.Types.Forall.istrunc_forall.
+Definition Book_3_1_6 `{Funext} A P := @HoTT.Basics.Trunc.istrunc_forall _ A P 0.
 
 (* ================================================== defn:1type *)
 (** Definition 3.1.7 *)
 
-Definition Book_3_1_7 := @HoTT.Basics.Overture.IsTrunc 1.
+Definition Book_3_1_7 := fun A => @HoTT.Basics.Overture.IsTrunc 1 A.
 
 (* ================================================== thm:isset-is1type *)
 (** Lemma 3.1.8 *)
@@ -385,7 +385,7 @@ Definition Book_3_1_9 := @HoTT.Types.Universe.not_hset_Type.
 (* ================================================== defn:isprop *)
 (** Definition 3.3.1 *)
 
-Definition Book_3_3_1 := @HoTT.Basics.Overture.IsTrunc (-1).
+Definition Book_3_3_1 := fun A => @HoTT.Basics.Overture.IsTrunc (-1) A.
 
 (* ================================================== thm:inhabprop-eqvunit *)
 (** Lemma 3.3.2 *)
@@ -433,7 +433,7 @@ Definition Book_3_5_1 := @HoTT.Types.Sigma.path_sigma_hprop.
 (** Example 3.6.2 *)
 
 Definition Book_3_6_2 `{Funext} (A : Type) (B : A -> Type)
-  := @HoTT.Types.Forall.istrunc_forall _ A B (-1).
+  := @HoTT.Basics.Trunc.istrunc_forall _ A B (-1).
 
 (* ================================================== defn:logical-notation *)
 (** Definition 3.7.1 *)
@@ -463,7 +463,7 @@ Definition Book_3_9_2 := @HoTT.HIT.unique_choice.unique_choice.
 (* ================================================== defn:contractible *)
 (** Definition 3.11.1 *)
 
-Definition Book_3_11_1 := @HoTT.Basics.Overture.IsTrunc (-2).
+Definition Book_3_11_1 := fun A => @HoTT.Basics.Overture.IsTrunc (-2) A.
 
 (* ================================================== thm:contr-unit *)
 (** Lemma 3.11.3 *)
@@ -478,12 +478,12 @@ Definition Book_3_11_4 := @HoTT.Basics.Trunc.ishprop_istrunc.
 (* ================================================== thm:contr-contr *)
 (** Corollary 3.11.5 *)
 
-Definition Book_3_11_5 := @HoTT.Basics.Contractible.contr_contr.
+Definition Book_3_11_5 `{Funext} := @HoTT.Basics.Trunc.contr_istrunc _ (-2).
 
 (* ================================================== thm:contr-forall *)
 (** Lemma 3.11.6 *)
 
-Definition Book_3_11_6 := @HoTT.Types.Forall.istrunc_forall.
+Definition Book_3_11_6 `{Funext} A P := @HoTT.Basics.Trunc.istrunc_forall _ A P (-2).
 
 (* ================================================== thm:retract-contr *)
 (** Lemma 3.11.7 *)
@@ -990,7 +990,7 @@ Definition Book_6_12_8 := @HoTT.HIT.Flattening.sWtil_rec_beta_ppt.
 (* ================================================== thm:hlevel-prod *)
 (** Theorem 7.1.9 *)
 
-Definition Book_7_1_9 := @HoTT.Types.Forall.istrunc_forall.
+Definition Book_7_1_9 := @HoTT.Basics.Trunc.istrunc_forall.
 
 (* ================================================== thm:isaprop-isofhlevel *)
 (** Theorem 7.1.10 *)
@@ -1538,7 +1538,7 @@ Proof.
     eapply istrunc_isequiv_istrunc.
     + refine (H' a b).
     + apply H.
-  - intros H' a b.
+  - intros H'; apply istrunc_S; intros a b.
     eapply istrunc_isequiv_istrunc.
     + apply (H' a b).
     + apply (@isequiv_inverse _ _ _ (H _ _)).
diff --git a/contrib/HoTTBookExercises.v b/contrib/HoTTBookExercises.v
index fcf37acc3c5..3dfb3cbff5b 100644
--- a/contrib/HoTTBookExercises.v
+++ b/contrib/HoTTBookExercises.v
@@ -686,7 +686,7 @@ Lemma Book_3_4_solution_1 `{Funext} (A : Type) : IsHProp A <-> Contr (A -> A).
 Proof.
   split.
   - intro isHProp_A.
-    exists idmap.
+    apply (Build_Contr _ idmap).
     apply path_ishprop. (* automagically, from IsHProp A *)
   - intro contr_AA.
     apply hprop_allpath; intros a1 a2.
@@ -823,7 +823,7 @@ Proof.
   {
     intros A.
     apply Book_3_4_solution_1.
-    apply Trunc_is_trunc.
+    apply istrunc_truncation.
   }
 
   (** There are no fixpoints of the fix-point free autoequivalence of 2 (called
@@ -1209,7 +1209,7 @@ End EquivFunctorFunextType.
 
 (** Using the Kraus-Sattler space of loops rather than the version in the book, since it is simpler and avoids use of propositional truncation. *)
 Definition Book_4_6_ii
-           (qua1 qua2 : QInv_Univalence_type)
+  (qua1 qua2 : QInv_Univalence_type) (* Two, since we need them at different universe levels. *)
   : ~ IsHProp (forall A : { X : Type & X = X }, A = A).
 Proof.
   pose (fa := @QInv_Univalence_implies_Funext_type qua2).
@@ -1240,22 +1240,24 @@ Proof.
   exact (true_ne_false (ap10 r true)).
 Defined.
 
+(** Assuming qinv-univalence, every quasi-equivalence automatically satisfies one of the adjoint laws. *)
 Definition allqinv_coherent (qua : QInv_Univalence_type)
            (A B : Type) (f : qinv A B)
   : (fun x => ap f.2.1 (fst f.2.2 x)) = (fun x => snd f.2.2 (f.2.1 x)).
 Proof.
+  (* Every quasi-equivalence is the image of a path, and can therefore be assumed to be the identity equivalence, for which the claim holds immediately. *)
   revert f.
   equiv_intro (equiv_qinv_path qua A B) p.
   destruct p; cbn; reflexivity.
 Defined.
 
+(** Qinv-univalence is inconsistent. *)
 Definition Book_4_6_iii (qua1 qua2 : QInv_Univalence_type) : Empty.
 Proof.
   apply (Book_4_6_ii qua1 qua2).
-  refine (istrunc_succ).
-  exists (fun A => 1); intros u.
-  set (B := {X : Type & X = X}) in *.
-  exact (allqinv_coherent qua2 B B (idmap ; (idmap ; (fun A:B => 1 , u)))).
+  nrapply istrunc_succ.
+  apply (Build_Contr _ (fun A => 1)); intros u.
+  exact (allqinv_coherent qua2 _ _ (idmap; (idmap; (fun A => 1, u)))).
 Defined.
 
 (* ================================================== ex:embedding-cancellable *)
@@ -1470,9 +1472,9 @@ Section Book_6_9.
   Proof.
     intro X.
     pose proof (@LEM (Contr { f : X <~> X & ~(forall x, f x = x) }) _) as contrXEquiv.
-    destruct contrXEquiv as [[f H]|H].
+    destruct contrXEquiv as [C|notC].
     - (** In the case where we have exactly one autoequivalence which is not the identity, use it. *)
-      exact (f.1).
+      exact ((@center _ C).1).
     - (** In the other case, just use the identity. *)
       exact idmap.
   Defined.
@@ -1499,8 +1501,9 @@ Section Book_6_9.
   Proof.
     apply path_forall; intro b.
     unfold Book_6_9.
-    destruct (@LEM (Contr { f : Bool <~> Bool & ~(forall x, f x = x) }) _) as [[f H']|H'].
-    - pose proof (bool_map_equiv_not_idmap f b).
+    destruct (@LEM (Contr { f : Bool <~> Bool & ~(forall x, f x = x) }) _) as [C|H'].
+    - set (f := @center _ C).
+      pose proof (bool_map_equiv_not_idmap f b).
       destruct (f.1 b), b;
       match goal with
         | _ => assumption
@@ -1510,10 +1513,10 @@ Section Book_6_9.
         | [ H : false = true |- _ ] => exact (match false_ne_true H with end)
       end.
     - refine (match H' _ with end).
-      eexists (exist (fun f : Bool <~> Bool =>
+      apply (Build_Contr _ (exist (fun f : Bool <~> Bool =>
                          ~(forall x, f x = x))
                       (Build_Equiv _ _ negb _)
-                      (fun H => false_ne_true (H true)));
+                      (fun H => false_ne_true (H true))));
         simpl.
       intro f.
       apply path_sigma_uncurried; simpl.
@@ -1564,8 +1567,8 @@ Section Book_6_9.
     intro Bad. pose proof ((happly Bad) true) as Ugly.
     assert ((solution_6_9 Bool true) = false) as Good.
     - unfold solution_6_9.
-      destruct (LEM (Contr (AllExistsOther Bool)) _) as [[f C]|C];simpl.
-      + elim (centralAllExOthBool f). reflexivity.
+      destruct (LEM (Contr (AllExistsOther Bool)) _) as [C|C];simpl.
+      + elim (centralAllExOthBool (@center _ C)). reflexivity.
       + elim (C contrAllExOthBool).
     - apply false_ne_true. rewrite (inverse Good). assumption.
   Defined.
diff --git a/theories/Algebra/AbGroups/AbPushout.v b/theories/Algebra/AbGroups/AbPushout.v
index 8e7ce2bd43f..2db3ff2f0ee 100644
--- a/theories/Algebra/AbGroups/AbPushout.v
+++ b/theories/Algebra/AbGroups/AbPushout.v
@@ -1,4 +1,4 @@
-Require Import Basics Types Truncations.Core.
+Require Import Basics Types Truncations.Core Modalities.ReflectiveSubuniverse.
 Require Import WildCat HSet.
 Require Export Algebra.Groups.Image Algebra.Groups.QuotientGroup.
 Require Import AbGroups.AbelianGroup AbGroups.Biproduct.
@@ -177,11 +177,11 @@ Proof.
   rapply contr_inhabited_hprop.
   (* To find a preimage of [x], we may first choose a representative [x']. *)
   assert (x' : merely (hfiber grp_quotient_map x)).
-  1: apply issurj_class_of.
+  1: apply center, issurj_class_of.
   strip_truncations; destruct x' as [[b c] p].
   (* Now [x] = [b + c] in the quotient. We find a preimage of [a]. *)
   assert (a : merely (hfiber f b)).
-  1: apply S.
+  1: apply center, S.
   strip_truncations; destruct a as [a q].
   refine (tr (g a + c; _)).
   refine (grp_homo_op _ _ _ @ _).
diff --git a/theories/Algebra/AbGroups/Biproduct.v b/theories/Algebra/AbGroups/Biproduct.v
index 94caf773b20..57737bb8ebb 100644
--- a/theories/Algebra/AbGroups/Biproduct.v
+++ b/theories/Algebra/AbGroups/Biproduct.v
@@ -167,7 +167,7 @@ Definition functor_ab_biprod_surjection `{Funext} {A A' B B' : AbGroup}
 Proof.
   intros [b b'].
   pose proof (a := S b); pose proof (a' := S' b').
-  destruct a as [a _], a' as [a' _].
+  apply center in a, a'.
   strip_truncations.
   rapply contr_inhabited_hprop.
   apply tr.
diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v
index 9d06068963d..625e0d1327a 100644
--- a/theories/Algebra/AbSES/Core.v
+++ b/theories/Algebra/AbSES/Core.v
@@ -130,6 +130,7 @@ Defined.
 Global Instance istrunc_abses `{Univalence} {B A : AbGroup@{u}}
   : IsTrunc 1 (AbSES B A).
 Proof.
+  apply istrunc_S.
   intros E F.
   refine (istrunc_equiv_istrunc _ equiv_path_abses_iso (n:=0)).
   rapply istrunc_sigma.
@@ -155,7 +156,7 @@ Proof.
     rapply contr_inhabited_hprop.
     (** Since [projection E] is epi, we can pull [projection F f] back to [e0 : E].*)
     assert (e0 : Tr (-1) (hfiber (projection E) (projection F f))).
-    1: apply issurjection_projection.
+    1: apply center, issurjection_projection.
     strip_truncations.
     (** The difference [f - (phi e0.1)] is sent to [0] by [projection F], hence lies in [A]. *)
     assert (a : Tr (-1) (hfiber (inclusion F) (f + (- phi e0.1)))).
diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index 054ad6b919d..5f937264e2a 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -123,7 +123,7 @@ Global Instance contr_abext_projective `{Univalence}
   (P : AbGroup) `{IsAbProjective P} {A : AbGroup}
   : Contr (Ext P A).
 Proof.
-  exists (point _); intro E.
+  apply (Build_Contr _ (point _)); intro E.
   strip_truncations.
   symmetry; by apply abext_trivial_projective.
 Defined.
diff --git a/theories/Algebra/AbSES/Pushout.v b/theories/Algebra/AbSES/Pushout.v
index 59068ea64d0..fabda362812 100644
--- a/theories/Algebra/AbSES/Pushout.v
+++ b/theories/Algebra/AbSES/Pushout.v
@@ -30,7 +30,7 @@ Proof.
       rapply contr_inhabited_hprop.
       (** Pick a preimage under the quotient map. *)
       assert (bc : merely (hfiber grp_quotient_map bc')).
-      1: apply issurj_class_of.
+      1: apply center, issurj_class_of.
       strip_truncations.
       destruct bc as [[b c] q].
       (** The E-component of the preimage is in the kernel of [projection E]. *)
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 0b797e55d20..4831eae893d 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -151,6 +151,7 @@ Defined.
 Global Instance ishset_grouphomomorphism {F : Funext} {G H : Group}
   : IsHSet (GroupHomomorphism G H).
 Proof.
+  apply istrunc_S.
   intros f g; apply (istrunc_equiv_istrunc _ equiv_path_grouphomomorphism).
 Defined.
 
@@ -264,6 +265,7 @@ Defined.
 Definition ishset_groupisomorphism `{F : Funext} {G H : Group}
   : IsHSet (GroupIsomorphism G H).
 Proof.
+  apply istrunc_S.
   intros f g; apply (istrunc_equiv_istrunc _ (equiv_path_groupisomorphism _ _)).
 Defined.
 
diff --git a/theories/Algebra/Universal/Algebra.v b/theories/Algebra/Universal/Algebra.v
index 3bb2e3fc252..6e6f67ed721 100644
--- a/theories/Algebra/Universal/Algebra.v
+++ b/theories/Algebra/Universal/Algebra.v
@@ -125,10 +125,11 @@ Lemma path_ap_carriers_path_algebra `{Funext} {σ} (A B : Algebra σ)
        = operations B)
   : ap carriers (path_algebra A B p q) = p.
 Proof.
+  destruct A as [A a ha], B as [B b hb]; cbn in p, q.
+  destruct p, q.
   unfold path_algebra, path_sigma_hprop, path_sigma_uncurried.
-  destruct A as [A a ha], B as [B b hb]; cbn in *.
-  destruct p, q; cbn.
-  now destruct (apD10^-1).
+  cbn -[center].
+  now destruct (center (ha = hb)).
 Defined.
 
 Arguments path_ap_carriers_path_algebra {_} {_} (A B)%Algebra_scope (p q)%path_scope.
@@ -151,7 +152,7 @@ Proof.
   unshelve eapply path_path_sigma.
   - transitivity (ap carriers p); [by destruct p |].
     transitivity (ap carriers q); [exact r | by destruct q].
-  - apply hprop_allpath. apply hset_path2.
+  - apply path_ishprop.
 Defined.
 
 Arguments path_path_algebra {_} {σ} {A B}%Algebra_scope (p q r)%path_scope.
diff --git a/theories/Basics/Contractible.v b/theories/Basics/Contractible.v
index 48544b942f4..f77f8ea0b4d 100644
--- a/theories/Basics/Contractible.v
+++ b/theories/Basics/Contractible.v
@@ -17,7 +17,7 @@ Definition path_contr `{Contr A} (x y : A) : x = y
 (** Any space of paths in a contractible space is contractible. *)
 Global Instance contr_paths_contr `{Contr A} (x y : A) : Contr (x = y) | 10000.
 Proof.
-  exists (path_contr x y).
+  apply (Build_Contr _ (path_contr x y)).
   intro r; destruct r; apply concat_Vp.
 Defined.
 
@@ -37,7 +37,7 @@ Arguments path_basedpaths {X x y} p : simpl nomatch.
 
 Global Instance contr_basedpaths {X : Type} (x : X) : Contr {y : X & x = y} | 100.
 Proof.
-  exists (x;1).
+  apply (Build_Contr _ (x;1)).
   intros [y p]; apply path_basedpaths.
 Defined.
 
@@ -105,17 +105,21 @@ Definition contr_retract {X Y : Type} `{Contr X}
 Definition contr_change_center {A : Type} (a : A) `{Contr A}
   : Contr A.
 Proof.
-  exists a.
+  apply (Build_Contr _ a).
   intros; apply path_contr.
 Defined.
 
-(** If a type is contractible, then so is its type of contractions. *)
-Global Instance contr_contr `{Funext} (A : Type) `{contrA : Contr A}
-  : Contr (Contr A) | 100.
-Proof.
-  exists contrA; intros [a2 c2].
-  destruct (contr a2).
-  apply (ap (Build_Contr _ (center A))).
-  apply path_forall; intros x.
-  apply path2_contr.
-Defined.
+(** The automatically generated induction principle for [IsTrunc_internal] produces two goals, so we define a custom induction principle for [Contr] that only produces the expected goal. *)
+Definition Contr_ind@{u v|} (A : Type@{u}) (P : Contr A -> Type@{v})
+  (H : forall (center : A) (contr : forall y, center = y), P (Build_Contr A center contr))
+  (C : Contr A)
+  : P C
+  := match C as C0 in IsTrunc n _ return
+          (match n as n0 return IsTrunc n0 _ -> Type@{v} with
+           | minus_two => fun c0 => P c0
+           | trunc_S k => fun _ => Unit
+           end C0)
+    with
+    | Build_Contr center contr => H center contr
+    | istrunc_S _ _ => tt
+    end.
diff --git a/theories/Basics/Decidable.v b/theories/Basics/Decidable.v
index 79114a002a9..fe4d7927216 100644
--- a/theories/Basics/Decidable.v
+++ b/theories/Basics/Decidable.v
@@ -158,6 +158,7 @@ Defined.
 Global Instance hset_pathcoll (A : Type) `{PathCollapsible A}
 : IsHSet A | 1000.
 Proof.
+  apply istrunc_S.
   intros x y.
   assert (h : forall p:x=y, p = (collapse (idpath x))^ @ collapse p).
   { intros []; symmetry; by apply concat_Vp. }
@@ -195,7 +196,8 @@ Global Instance ishprop_decpaths `{Funext} (A : Type)
 Proof.
   apply hprop_inhabited_contr; intros d.
   assert (IsHSet A) by exact _.
-  exists d; intros d'.
+  apply (Build_Contr _ d).
+  intros d'.
   apply path_forall; intros x; apply path_forall; intros y.
   generalize (d x y); clear d; intros d.
   generalize (d' x y); clear d'; intros d'.
diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v
index 5ae798750e2..1034a488773 100644
--- a/theories/Basics/Equivalences.v
+++ b/theories/Basics/Equivalences.v
@@ -214,7 +214,7 @@ Definition moveL_equiv_V' `(f : A <~> B) (x : B) (y : A) (p : f y = x)
 Lemma contr_equiv A {B} (f : A -> B) `{IsEquiv A B f} `{Contr A}
   : Contr B.
 Proof.
-  exists (f (center A)).
+  apply (Build_Contr _ (f (center A))).
   intro y.
   apply moveR_equiv_M.
   apply contr.
@@ -574,13 +574,14 @@ Ltac ev_equiv :=
 
 (** The following tactic [make_equiv] builds an equivalence between two types built out of arbitrarily nested sigma and record types, not necessarily right-associated, as long as they have all the same underyling components.  This is more general than [issig] in that it doesn't just prove equivalences between a single record type and a single right-nested tower of sigma types, but less powerful in that it can't deduce the latter nested tower of sigmas automatically: you have to have both sides of the equivalence known. *)
 
-(* Perform [intros] repeatedly, recursively destructing all possibly-nested record types. *)
+(* Perform [intros] repeatedly, recursively destructing all possibly-nested record types. We use a custom induction principle for [Contr], since [elim] produces two goals. *)
 Ltac decomposing_intros :=
   let x := fresh in
   intros x; cbn in x;
-  try match type of x with
-  | ?a = ?b => fail 1           (** Don't destruct paths *)
-  | forall y:?A, ?B => fail 1   (** Don't apply functions *)
+  try lazymatch type of x with
+  | ?a = ?b => idtac           (** Don't destruct paths *)
+  | forall y:?A, ?B => idtac   (** Don't apply functions *)
+  | Contr ?A => revert x; match goal with |- (forall y, ?P y) => snrefine (Contr_ind A P _) end
   | _ => elim x; clear x
   end;
   try decomposing_intros.
diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v
index 915f7a1e25f..5d7d7d4ae65 100644
--- a/theories/Basics/Overture.v
+++ b/theories/Basics/Overture.v
@@ -494,25 +494,17 @@ In order to achieve moderate coverage and speedy resolution, we currently follow
 - We prefer to reason about syntactically smaller types.  That is, typeclass instances should turn goals of type [IsTrunc n (forall a : A, P a)] into goals of type [forall a : A, IsTrunc n (P a)]; and goals of type [IsTrunc n (A * B)] into the pair of goals of type [IsTrunc n A] and [IsTrunc n B]; rather than the other way around.  Ideally, we would add similar rules to transform hypotheses in the cases where we can do so.  This rule is not always the one we want, but it seems to heuristically capture the shape of most cases that we want the typeclass machinery to automatically infer.  That is, we often want to infer [IsTrunc n (A * B)] from [IsTrunc n A] and [IsTrunc n B], but we (probably) don't often need to do other simple things with [IsTrunc n (A * B)] which are broken by that reduction.
 *)
 
-(** *** Contractibility *)
+(** *** Contractibility and truncation levels *)
 
-(** A space [A] is contractible if there is a point [x : A] and a (pointwise) homotopy connecting the identity on [A] to the constant map at [x].  Thus an element of [contr A] is a pair whose first component is a point [x] and the second component is a pointwise retraction of [A] to [x]. *)
+(** Truncation measures how complicated a type is in terms of higher path types. The (-2)-truncated types are the contractible ones, whose homotopy is completely trivial.  More precisely, a type [A] is contractible if there is a point [x : A] and a (pointwise) homotopy connecting the identity on [A] to the constant map at [x].
 
-(** We use the [Contr_internal] record so as not to pollute typeclass search; we only do truncation typeclass search on the [IsTrunc] datatype, usually.  We will define a notation [Contr] which is equivalent to [Contr_internal], but picked up by typeclass search.  However, we must make [Contr_internal] a class so that we pick up typeclasses on [center] and [contr].  However, the only typeclass rule we register is the one that turns it into a [Contr]/[IsTrunc].  Unfortunately, this means that declaring an instance like [Instance contr_foo : Contr foo := { center := bar }.] will fail with mismatched instances/contexts.  Instead, we must iota expand such definitions to get around Coq's deficiencies, and write [Instance contr_foo : Contr foo := let x := {| center := bar |} in x.] *)
-Class Contr_internal (A : Type) := Build_Contr {
-  center : A ;
-  contr : (forall y : A, center = y)
-}.
-
-Arguments center A {_}.
-
-(** *** Truncation levels *)
+   The (n+1)-truncated types are those whose path types are n-truncated.
 
-(** Truncation measures how complicated a type is in terms of higher path spaces. The (-2)-truncated types are the contractible ones, whose homotopy is completely trivial. The (n+1)-truncated types are those whose path spaces are n-truncated.
+   Thus, (-1)-truncated means "the type of paths between any two points is contractible". Such a type is necessarily a sub-singleton: any two points are connected by a path which is unique up to homotopy. In other words, (-1)-truncated types are truth values.  We call such types "propositions" or "h-propositions".
 
-   Thus, (-1)-truncated means "the space of paths between any two points is contactible". Such a space is necessarily a sub-singleton: any two points are connected by a path which is unique up to homotopy. In other words, (-1)-truncated spaces are truth values (we call them "propositions").
+   Next, 0-truncated means "the type of paths between any two points is a sub-singleton". Thus, two points might not have any paths between them, or they have a unique path. Such a type may have many points but it is discrete in the sense that all paths are trivial. We call such types "sets" or "h-sets".
 
-   Next, 0-truncated means "the space of paths between any two points is a sub-singleton". Thus, two points might not have any paths between them, or they have a unique path. Such a space may have many points but it is discrete in the sense that all paths are trivial. We call such spaces "sets".
+   We begin by defining the type that indexes the truncation levels.
 *)
 
 Inductive trunc_index : Type0 :=
@@ -538,61 +530,84 @@ Notation "n .+4" := (n.+1.+3)%trunc : trunc_scope.
 Notation "n .+5" := (n.+1.+4)%trunc : trunc_scope.
 Local Open Scope trunc_scope.
 
-(** Further notation for truncation levels is introducted in Trunc.v. *)
+(** We define truncatedness using an inductive type [IsTrunc_internal A n].  We use a notation [IsTrunc n A] simply to swap the orders of arguments, and notations [Contr], [IsHProp] and [IsHSet] which specialize to [n] being [-2], [-1] and [0], respectively.  An alternative is to use a [Fixpoint], and that was done in the past.  The advantages of the inductive approach are:  [IsTrunc_internal] is cumulative; typeclass inherence works smoothly; the library builds faster.  Some disadvantages are that we need to manually apply the constructors when proving that something is truncated, and that the induction principle is awkward to work with. *)
 
-(** n-truncatedness is defined by recursion on [n].  We could simply define [IsTrunc] as a fixpoint and an [Existing Class], but we want to also declare [IsTrunc] to be [simpl nomatch], so that when we say [simpl] or [cbn], [IsTrunc n.+1 A] doesn't get unfolded to [forall x y:A, IsTrunc n (x = y)].  But we also want to be able to use this equality, e.g. by proving [IsTrunc n.+1 A] starting with [intros x y], and if [IsTrunc] is a fixpoint declared as [simpl nomatch] then that doesn't work, because [intros] uses [hnf] to expose a [forall] and [hnf] respects [simpl nomatch] on fixpoints.  But we can make it work if we define the fixpoint separately as [IsTrunc_internal] and then take the class [IsTrunc] to be a definitional wrapper around it, since [hnf] is willing to unfold non-fixpoints even if they are defined as [simpl never].  This behavior of [hnf] is arguably questionable (see https://github.com/coq/coq/issues/11619), but it is useful for us here. *)
+Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
+| Build_Contr : forall (center : A) (contr : forall y, center = y), IsTrunc_internal A minus_two
+| istrunc_S : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).
+
+Existing Class IsTrunc_internal.
 
-Fixpoint IsTrunc_internal (n : trunc_index) (A : Type@{u}) : Type@{u} :=
-  match n with
-    | minus_two => Contr_internal A
-    | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
-  end.
+Notation IsTrunc n A := (IsTrunc_internal A n).
 
-Arguments IsTrunc_internal n A : simpl nomatch.
+Scheme IsTrunc_internal_ind := Induction for IsTrunc_internal Sort Type.
+Scheme IsTrunc_internal_rec := Minimality for IsTrunc_internal Sort Type.
+Definition IsTrunc_internal_rect := IsTrunc_internal_ind.
 
-Class IsTrunc (n : trunc_index) (A : Type) : Type :=
-  Trunc_is_trunc : IsTrunc_internal n A.
+Definition IsTrunc_unfolded (n : trunc_index) (A : Type)
+  := match n with
+    | minus_two => { center : A & forall y, center = y }
+    | n.+1 => forall x y : A, IsTrunc n (x = y)
+    end.
 
-(** We use the principle that we should always be doing typeclass resolution on truncation of non-equality types.  We try to change the hypotheses and goals so that they never mention something like [IsTrunc n (_ = _)] and instead say [IsTrunc (S n) _].  If you're evil enough that some of your paths [a = b] are n-truncated, but others are not, then you'll have to either reason manually or add some (local) hints with higher priority than the hint below, or generalize your equality type so that it's not a path anymore. *)
+Definition istrunc_unfold (n : trunc_index) (A : Type)
+  : IsTrunc n A -> IsTrunc_unfolded n A.
+Proof.
+  intros [center contr|k istrunc].
+  - exact (center; contr).
+  - exact istrunc.
+Defined.
 
-#[global] Typeclasses Opaque IsTrunc. (* don't auto-unfold [IsTrunc] in typeclass search *)
+Definition isequiv_istrunc_unfold (n : trunc_index) (A : Type)
+  : IsEquiv (istrunc_unfold n A).
+Proof.
+  simple refine (Build_IsEquiv _ _ (istrunc_unfold n A) _ _ _ _).
+  - destruct n.
+    + intros [center contr]; exact (Build_Contr _ center contr).
+    + intros H. exact (istrunc_S _ H).
+  - destruct n; reflexivity.
+  - intros [center contr|k istrunc]; reflexivity.
+  - intros [center contr|k istrunc]; reflexivity.
+Defined.
 
-Arguments IsTrunc : simpl never. (* don't auto-unfold [IsTrunc] with [simpl] *)
+Definition equiv_istrunc_unfold (n : trunc_index) (A : Type)
+  := Build_Equiv _ _ _  (isequiv_istrunc_unfold n A).
 
+(** A version of [istrunc_unfold] for successors. *)
 Global Instance istrunc_paths (A : Type) n `{H : IsTrunc n.+1 A} (x y : A)
-: IsTrunc n (x = y)
-  := H x y. (* but do fold [IsTrunc] *)
+  : IsTrunc n (x = y)
+  := istrunc_unfold n.+1 A H x y.
 
-Existing Class IsTrunc_internal.
+Notation Contr A := (IsTrunc minus_two A).
+Notation IsHProp A := (IsTrunc minus_two.+1 A).
+Notation IsHSet A := (IsTrunc minus_two.+2 A).
 
-#[export]
-Hint Extern 0 (IsTrunc_internal _ _) => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *)
+Definition center (A : Type) {H : Contr A} : A := pr1 (istrunc_unfold _ _ H).
+Definition contr {A : Type} {H : Contr A} (y : A) : center A = y := pr2 (istrunc_unfold _ _ H) y.
 
-#[export]
-Hint Extern 0 (IsTrunc _ _) => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *)
+(** We define a slight variation of [istrunc_unfold], which differs only it what it does for [n = -2].  It will produce a section of the following type family. *)
+Definition istrunc_codomain_fam {n : trunc_index} {A : Type} (istrunc : IsTrunc n A) : A -> Type.
+Proof.
+  intro y.
+  destruct n.
+  - exact (center A = y).
+  - exact (forall x : A, IsTrunc n (y = x)).
+Defined.
 
-(** Picking up the [forall x y, IsTrunc n (x = y)] instances in the hypotheses is much tricker.  We could do something evil where we declare an empty typeclass like [IsTruncSimplification] and use the typeclass as a proxy for allowing typeclass machinery to factor nested [forall]s into the [IsTrunc] via backward reasoning on the type of the hypothesis... but, that's rather complicated, so we instead explicitly list out a few common cases.  It should be clear how to extend the pattern. *)
-#[export]
-Hint Extern 10 =>
-progress match goal with
-           | [ H : forall x y : ?T, IsTrunc ?n (x = y) |- _ ]
-             => change (IsTrunc n.+1 T) in H
-           | [ H : forall (a : ?A) (x y : @?T a), IsTrunc ?n (x = y) |- _ ]
-             => change (forall a : A, IsTrunc n.+1 (T a)) in H; cbv beta in H
-           | [ H : forall (a : ?A) (b : @?B a) (x y : @?T a b), IsTrunc ?n (x = y) |- _ ]
-             => change (forall (a : A) (b : B a), IsTrunc n.+1 (T a b)) in H; cbv beta in H
-           | [ H : forall (a : ?A) (b : @?B a) (c : @?C a b) (x y : @?T a b c), IsTrunc ?n (x = y) |- _ ]
-             => change (forall (a : A) (b : B a) (c : C a b), IsTrunc n.+1 (T a b c)) in H; cbv beta in H
-           | [ H : forall (a : ?A) (b : @?B a) (c : @?C a b) (d : @?D a b c) (x y : @?T a b c d), IsTrunc ?n (x = y) |- _ ]
-             => change (forall (a : A) (b : B a) (c : C a b) (d : D a b c), IsTrunc n.+1 (T a b c d)) in H; cbv beta in H
-         end : core.
-
-Notation Contr := (IsTrunc minus_two).
-Notation IsHProp := (IsTrunc minus_two.+1).
-Notation IsHSet := (IsTrunc minus_two.+2).
+(** The variant of [istrunc_unfold] lets us treat any proof of truncation as a function.  For [n = -2], it produces the contracting homotopy. *)
+Definition istrunc_fun {n : trunc_index} {A : Type} (istrunc : IsTrunc n A)
+  : forall y : A, istrunc_codomain_fam istrunc y.
+Proof.
+  destruct n.
+  - exact (@contr A istrunc).
+  - exact (istrunc_unfold _ _ istrunc).
+Defined.
 
-#[export]
-Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
+(** We add this as a coercion. *)
+(** TODO: Once Coq 8.18 is the minimum, prefix the next line with
+#[warning="-uniform-inheritance"] 
+*)
+Coercion istrunc_fun : IsTrunc >-> Funclass.
 
 (** *** Truncated relations  *)
 
diff --git a/theories/Basics/Tactics.v b/theories/Basics/Tactics.v
index c5956432fb7..94fee39f684 100644
--- a/theories/Basics/Tactics.v
+++ b/theories/Basics/Tactics.v
@@ -733,12 +733,6 @@ Ltac issig :=
 
 (** We show how the tactic works in a couple of examples. *)
 
-Definition issig_contr (A : Type)
-  : {x : A & forall y, x = y} <~> Contr A.
-Proof.
-  issig.
-Defined.
-
 Definition issig_equiv (A B : Type)
   : {f : A -> B & IsEquiv f} <~> Equiv A B.
 Proof.
diff --git a/theories/Basics/Trunc.v b/theories/Basics/Trunc.v
index 2bc8f4c1ea9..d16b4928d38 100644
--- a/theories/Basics/Trunc.v
+++ b/theories/Basics/Trunc.v
@@ -279,13 +279,20 @@ Definition contr_istrunc_minus_two `{H : IsTrunc (-2) A} : Contr A
   := H.
 
 (** Truncation levels are cumulative. *)
-Global Instance istrunc_succ `{IsTrunc n A}
-  : IsTrunc n.+1 A | 1000.
+Global Instance istrunc_paths' {n : trunc_index} {A : Type} `{IsTrunc n A}
+  : forall x y : A, IsTrunc n (x = y) | 1000.
 Proof.
   generalize dependent A.
   simple_induction n n IH; simpl; intros A H x y.
   - apply contr_paths_contr.
-  - apply IH, H.
+  - apply istrunc_S.  rapply IH.
+Defined.
+
+Global Instance istrunc_succ {n : trunc_index} {A : Type} `{IsTrunc n A}
+  : IsTrunc n.+1 A | 1000.
+Proof.
+  apply istrunc_S.
+  apply istrunc_paths'.
 Defined.
 
 (** This could be an [Instance] (with very high priority, so it doesn't get applied trivially).  However, we haven't given typeclass search any hints allowing it to solve goals like [m <= n], so it would only ever be used trivially.  *)
@@ -298,8 +305,9 @@ Proof.
   - (* -2, -2 *) assumption.
   - (* S m', -2 *) destruct Hmn.
   - (* -2, S n' *) apply @istrunc_succ, (IH (-2)); auto.
-  - (* S m', S n' *) intros x y; apply (IH m');
-                     auto with typeclass_instances.
+  - (* S m', S n' *)
+    apply istrunc_S.
+    intros x y; apply (IH m'); auto with typeclass_instances.
 Defined.
 
 (** In particular, a contractible type, hprop, or hset is truncated at all higher levels.  We don't allow these to be used as idmaps, since there would be no point to it. *)
@@ -327,9 +335,9 @@ Proof.
   generalize dependent B; generalize dependent A.
   simple_induction n n IH; simpl; intros A ? B f ?.
   - exact (contr_equiv _ f).
-  - intros x y.
-    exact (IH (f^-1 x = f^-1 y) (H (f^-1 x) (f^-1 y))
-      (x = y) ((ap (f^-1))^-1) _).
+  - apply istrunc_S.
+    intros x y.
+    refine (IH _ _ _ (ap (f^-1))^-1 _).
 Defined.
 
 Definition istrunc_equiv_istrunc A {B} (f : A <~> B) `{IsTrunc n A}
@@ -377,16 +385,16 @@ Canonical Structure default_TruncType := fun n T P => (@Build_TruncType n T P).
 Lemma contr_inhabited_hprop (A : Type) `{H : IsHProp A} (x : A)
   : Contr A.
 Proof.
-  exists x.
+  apply (Build_Contr _ x).
   intro y.
-  apply center, H.
+  rapply center.
 Defined.
 
 (** If inhabitation implies contractibility, then we have an h-proposition.  We probably won't often have a hypothesis of the form [A -> Contr A], so we make sure we give priority to other instances. *)
 Global Instance hprop_inhabited_contr (A : Type)
   : (A -> Contr A) -> IsHProp A | 10000.
 Proof.
-  intros H x y.
+  intros H; apply istrunc_S; intros x y.
   pose (C := H x).
   apply contr_paths_contr.
 Defined.
@@ -395,15 +403,17 @@ Defined.
 Theorem path_ishprop `{H : IsHProp A}
   : forall x y : A, x = y.
 Proof.
-  apply H.
+  intros x y.
+  rapply center.
 Defined.
 
 (** Conversely, this property characterizes hprops. *)
 Theorem hprop_allpath (A : Type)
   : (forall (x y : A), x = y) -> IsHProp A.
-  intros H x y.
-  pose (C := Build_Contr A x (H x)).
-  apply contr_paths_contr.
+Proof.
+  intros H; apply istrunc_S; intros x y.
+  nrapply contr_paths_contr.
+  exact (Build_Contr _ x (H x)).
 Defined.
 
 (** Two propositions are equivalent as soon as there are maps in both directions. *)
@@ -435,29 +445,42 @@ Proof.
   - rapply contr_inhabited_hprop.
 Defined.
 
-Corollary equiv_contr_hprop (A : Type) `{Funext} `{IsHProp A}
-  : Contr A <~> A.
+(** ** Truncatedness: any dependent product of n-types is an n-type *)
+
+Definition contr_forall `{Funext} `{P : A -> Type} `{forall a, Contr (P a)}
+  : Contr (forall a, P a).
 Proof.
-  exact (equiv_iff_hprop_uncurried (iff_contr_hprop A)).
+  apply (Build_Contr _ (fun a => center (P a))).
+  intro f.  apply path_forall.  intro a.  apply contr.
+Defined.
+
+Global Instance istrunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
+  : IsTrunc n (forall a, P a) | 100.
+Proof.
+  generalize dependent P.
+  simple_induction n n IH; simpl; intros P ?.
+  (* case [n = -2], i.e. contractibility *)
+  - apply contr_forall.
+  (* case n = n'.+1 *)
+  - apply istrunc_S.
+    intros f g; apply (istrunc_isequiv_istrunc@{u1 u1} _ (apD10@{_ _ u1} ^-1)).
 Defined.
 
 (** Truncatedness is an hprop. *)
 Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
   : IsHProp (IsTrunc n A) | 0.
 Proof.
-  apply hprop_inhabited_contr.
-  revert A.
-  simple_induction n n IH; unfold IsTrunc; simpl.
-  - intros A ?.
-    exact _.
-  - intros A AH1.
-    exists AH1.
-    intro AH2.
-    apply path_forall; intro x.
-    apply path_forall; intro y.
-    apply @path_contr.
-    apply IH, AH1.
-Qed.
+  revert A; simple_induction n n IH; cbn; intro A.
+  - nrapply (istrunc_equiv_istrunc _ (equiv_istrunc_unfold (-2) A)^-1%equiv).
+    apply hprop_allpath.
+    intros [a1 c1] [a2 c2].
+    destruct (c1 a2).
+    apply (ap (exist _ a1)).
+    funext x.
+    pose (Build_Contr _ a1 c1); apply path2_contr.
+  - rapply (istrunc_equiv_istrunc _ (equiv_istrunc_unfold n.+1 A)^-1%equiv).
+    (* This case follows from [istrunc_forall]. *)
+Defined.
 
 (** By [trunc_hprop], it follows that [IsTrunc n A] is also [m]-truncated for any [m >= -1]. *)
 
@@ -470,4 +493,15 @@ Proof.
   apply path_ishprop.
 Defined.
 
+(** If a type [A] is [n]-truncated, then [IsTrunc n A] is contractible. *)
+Global Instance contr_istrunc `{Funext} (n : trunc_index) (A : Type) `{istruncA : IsTrunc n A}
+  : Contr (IsTrunc n A) | 100
+  := contr_inhabited_hprop _ _.
+
+Corollary equiv_contr_hprop (A : Type) `{Funext} `{IsHProp A}
+  : Contr A <~> A.
+Proof.
+  exact (equiv_iff_hprop_uncurried (iff_contr_hprop A)).
+Defined.
+
 (** If you are looking for a theorem about truncation, you may want to read the note "Finding Theorems" in "STYLE.md". *)
diff --git a/theories/Categories/Category/Pi.v b/theories/Categories/Category/Pi.v
index 60d550f0631..a9afc27ebc9 100644
--- a/theories/Categories/Category/Pi.v
+++ b/theories/Categories/Category/Pi.v
@@ -1,5 +1,6 @@
 (** * Dependent Product Category *)
 Require Import Category.Strict.
+Require Import Basics.Trunc.
 Require Import Types.Forall.
 
 Set Universe Polymorphism.
diff --git a/theories/Categories/Category/Sigma/Univalent.v b/theories/Categories/Category/Sigma/Univalent.v
index 48f46ead3a8..966312d1a34 100644
--- a/theories/Categories/Category/Sigma/Univalent.v
+++ b/theories/Categories/Category/Sigma/Univalent.v
@@ -211,6 +211,7 @@ Section on_both.
   (** TODO: generalize this to a theorem [forall A P, IsHSet A -> IsHSet { x : A | P x } -> forall x, IsHSet (P x)], [inO_unsigma] of ##672 *)
   Local Instance ishset_pmor {s d m} : IsHSet (Pmor s d m).
   Proof.
+    apply istrunc_S.
     intros p q.
     apply hprop_allpath.
     let H := constr:(_ : forall x y : mor s d, IsHProp (x = y)) in
diff --git a/theories/Categories/Category/Sum.v b/theories/Categories/Category/Sum.v
index 44a9c9fea60..6608f7f4a63 100644
--- a/theories/Categories/Category/Sum.v
+++ b/theories/Categories/Category/Sum.v
@@ -52,7 +52,7 @@ Proof.
             _
             _);
   abstract (
-      repeat (simpl || intros [] || intro);
+      repeat (simpl || apply istrunc_S || intros [] || intro);
       auto with morphism;
       typeclasses eauto
     ).
diff --git a/theories/Categories/Category/Univalent.v b/theories/Categories/Category/Univalent.v
index 6a9e5895f40..9bad22769ca 100644
--- a/theories/Categories/Category/Univalent.v
+++ b/theories/Categories/Category/Univalent.v
@@ -19,6 +19,7 @@ Notation isotoid C s d := (@equiv_inv _ _ (@idtoiso C s d) _).
 
 Global Instance trunc_category `{IsCategory C} : IsTrunc 1 C | 10000.
 Proof.
+  apply istrunc_S.
   intros ? ?.
   eapply istrunc_equiv_istrunc;
   [ symmetry;
diff --git a/theories/Categories/InitialTerminalCategory/Core.v b/theories/Categories/InitialTerminalCategory/Core.v
index e69f87b9c89..b79ec519aa4 100644
--- a/theories/Categories/InitialTerminalCategory/Core.v
+++ b/theories/Categories/InitialTerminalCategory/Core.v
@@ -26,7 +26,7 @@ Class IsInitialCategory (C : PreCategory)
 
 Global Instance trunc_initial_category `{IsInitialCategory C}
 : IsHProp C
-  := fun x y => initial_category_ind _ x.
+  := istrunc_S _ (fun x y => initial_category_ind _ x).
 Global Instance trunc_initial_category_mor `{IsInitialCategory C} x y
 : Contr (morphism C x y)
   := initial_category_ind _ x.
diff --git a/theories/Categories/NatCategory.v b/theories/Categories/NatCategory.v
index 7bdd2459b52..686f091a0f7 100644
--- a/theories/Categories/NatCategory.v
+++ b/theories/Categories/NatCategory.v
@@ -29,6 +29,7 @@ Module Export Core.
   Proof.
     induction n; [ typeclasses eauto |].
     induction n; [ typeclasses eauto |].
+    apply istrunc_S.
     intros [x|x] [y|y];
       typeclasses eauto.
   Qed.
diff --git a/theories/Categories/SemiSimplicialSets.v b/theories/Categories/SemiSimplicialSets.v
index 6fe5064894e..4f5fe0218f6 100644
--- a/theories/Categories/SemiSimplicialSets.v
+++ b/theories/Categories/SemiSimplicialSets.v
@@ -1,5 +1,5 @@
 (** * The category of semisimplicial sets *)
-Require Import Types.
+Require Import Types Basics.Trunc.
 Require Import Category.Core Functor.Core.
 Require Import Category.Morphisms.
 Require Import Category.Dual FunctorCategory.Core.
@@ -24,7 +24,7 @@ Module Export Core.
         nonstandard), then semi-simplicial sets (also a non-standard
         term) (sic) are [Fun(Γᵒᵖ, Set)]. Define the obvious inclusion
         [Γ -> Δ], which we will use to make simplicial sets without
-        having to worry about "degneracies". *)
+        having to worry about "degeneracies". *)
 
     Definition semisimplex_category : PreCategory
       := wide simplex_category
diff --git a/theories/Categories/UniversalProperties.v b/theories/Categories/UniversalProperties.v
index 07dc22de9dc..7f5b259101c 100644
--- a/theories/Categories/UniversalProperties.v
+++ b/theories/Categories/UniversalProperties.v
@@ -111,13 +111,13 @@ Section UniversalMorphism.
              A
              p
              (fun A' p' =>
-                {| center := (m A' p'; H A' p');
-                   contr m' := path_sigma
+                Build_Contr _ (m A' p'; H A' p')
+                              (fun m' => path_sigma
                                  _
                                  (m A' p'; H A' p')
                                  m'
                                  (H' A' p' m'.1 m'.2)
-                                 (center _) |}).
+                                 (center _))).
 
       (** Projections from nested sigmas are currently rather slow.  We should just be able to do
 
@@ -237,15 +237,15 @@ Section UniversalMorphism.
                  (Y : D) (f : morphism C X (U Y))
       : Contr { m : morphism D (IsInitialMorphism_object M) Y
               | U _1 m o IsInitialMorphism_morphism M = f }
-        := {| center := (IsInitialMorphism_property_morphism M Y f;
-                         IsInitialMorphism_property_morphism_property M Y f);
-              contr m' := path_sigma
+        := Build_Contr _ (IsInitialMorphism_property_morphism M Y f;
+                         IsInitialMorphism_property_morphism_property M Y f)
+              (fun m' => path_sigma
                             _
                             (IsInitialMorphism_property_morphism M Y f;
                              IsInitialMorphism_property_morphism_property M Y f)
                             m'
                             (@IsInitialMorphism_property_morphism_unique M Y f m'.1 m'.2)
-                            (center _) |}.
+                            (center _)).
     End EliminationAbstractionBarrier.
 
     Global Arguments IsInitialMorphism_object : simpl never.
diff --git a/theories/Classes/implementations/binary_naturals.v b/theories/Classes/implementations/binary_naturals.v
index b3c162aac1a..246a4e61f6e 100644
--- a/theories/Classes/implementations/binary_naturals.v
+++ b/theories/Classes/implementations/binary_naturals.v
@@ -278,7 +278,7 @@ Section semiring_laws.
   Global Instance binnat_semiring : IsSemiRing binnat.
   Proof.
     split; try split; try split; try split; hnf; intros.
-    1, 5: exact (binnat_set x y).
+    1, 5: apply istrunc_S; intros x y; exact (binnat_set x y).
     all: apply (equiv_inj unary).
     1, 2, 3, 7: repeat rewrite <- unaryplus.
     4, 5, 6, 7: rewrite <- unarymult.
diff --git a/theories/Classes/implementations/field_of_fractions.v b/theories/Classes/implementations/field_of_fractions.v
index fb01b2e6160..2ba7aba1a3d 100644
--- a/theories/Classes/implementations/field_of_fractions.v
+++ b/theories/Classes/implementations/field_of_fractions.v
@@ -1,4 +1,4 @@
-Require Import HoTT.HIT.quotient.
+Require Import HoTT.HIT.quotient HoTT.Basics.Trunc.
 Require Import 
   HoTT.Classes.interfaces.abstract_algebra
   HoTT.Classes.theory.dec_fields.
@@ -269,7 +269,7 @@ Definition F_ind2@{i j} (P : F -> F -> Type@{i}) {sP : forall x y, IsHProp (P x
   (dclass : forall x y : Frac R, P (' x) (' y)) : forall x y, P x y.
 Proof.
 apply (@F_ind (fun x => forall y, _)).
-- intros;apply Forall.istrunc_forall@{UR i j}.
+- intros;apply istrunc_forall@{UR i j}.
 - intros x.
   apply (F_ind _);intros y.
   apply dclass.
@@ -281,7 +281,7 @@ Definition F_ind3@{i j} (P : F -> F -> F -> Type@{i})
   : forall x y z, P x y z.
 Proof.
 apply (@F_ind (fun x => forall y z, _)).
-- intros;apply Forall.istrunc_forall@{UR j j}.
+- intros;apply istrunc_forall@{UR j j}.
 - intros x.
   apply (F_ind2@{i j} _). auto.
 Qed.
diff --git a/theories/Classes/implementations/natpair_integers.v b/theories/Classes/implementations/natpair_integers.v
index 934faf72513..955c55a4c2d 100644
--- a/theories/Classes/implementations/natpair_integers.v
+++ b/theories/Classes/implementations/natpair_integers.v
@@ -1,5 +1,5 @@
 Require Import HoTT.HIT.quotient
-  HoTT.TruncType.
+  HoTT.TruncType HoTT.Basics.Trunc.
 Require Import
   HoTT.Classes.implementations.peano_naturals
   HoTT.Classes.interfaces.abstract_algebra
@@ -349,8 +349,8 @@ Definition Z_ind3@{i j} (P : Z -> Z -> Z -> Type@{i})
 Proof.
 apply (@Z_ind (fun x => forall y z, _));intros x.
 2:apply (Z_ind2@{i j} _);auto.
-apply (@Forall.istrunc_forall@{UN j j} _).
-intros. apply Forall.istrunc_forall@{UN i j}.
+apply (@istrunc_forall@{UN j j} _).
+intros. apply istrunc_forall@{UN i j}.
 Defined.
 
 Definition Z_rec@{i} {T : Type@{i} } {sT : IsHSet T}
diff --git a/theories/Classes/interfaces/abstract_algebra.v b/theories/Classes/interfaces/abstract_algebra.v
index 81bc1e34104..e4c3083752e 100644
--- a/theories/Classes/interfaces/abstract_algebra.v
+++ b/theories/Classes/interfaces/abstract_algebra.v
@@ -411,7 +411,7 @@ Definition issig_issemigroup x y : _ <~> @IsSemiGroup x y := ltac:(issig).
 Global Instance ishprop_issemigroup `{Funext}
   : forall x y, IsHProp (@IsSemiGroup x y).
 Proof.
-  intros x y a b.
+  intros x y; apply istrunc_S; intros a b.
   rewrite <- (eisretr (issig_issemigroup x y) a).
   rewrite <- (eisretr (issig_issemigroup x y) b).
   set (a' := (issig_issemigroup x y)^-1 a).
@@ -436,6 +436,7 @@ Definition issig_ismonoid x y z : _ <~> @IsMonoid x y z := ltac:(issig).
 
 Global Instance ishprop_ismonoid `{Funext} x y z : IsHProp (@IsMonoid x y z).
 Proof.
+  apply istrunc_S.
   intros a b.
   rewrite <- (eisretr (issig_ismonoid x y z) a).
   rewrite <- (eisretr (issig_ismonoid x y z) b).
@@ -470,6 +471,7 @@ Definition issig_isgroup w x y z : _ <~> @IsGroup w x y z := ltac:(issig).
 
 Global Instance ishprop_isgroup `{Funext} w x y z : IsHProp (@IsGroup w x y z).
 Proof.
+  apply istrunc_S.
   intros a b.
   rewrite <- (eisretr (issig_isgroup w x y z) a).
   rewrite <- (eisretr (issig_isgroup w x y z) b).
diff --git a/theories/Classes/interfaces/ua_algebra.v b/theories/Classes/interfaces/ua_algebra.v
index 16f1596f306..b80ca628c41 100644
--- a/theories/Classes/interfaces/ua_algebra.v
+++ b/theories/Classes/interfaces/ua_algebra.v
@@ -236,7 +236,7 @@ Proof.
   unshelve eapply path_path_sigma.
   - transitivity (ap carriers p); [by destruct p |].
     transitivity (ap carriers q); [exact r | by destruct q].
-  - apply hprop_allpath. apply hset_path2.
+  - apply path_ishprop.
 Defined.
 
 Module algebra_notations.
diff --git a/theories/Classes/theory/ua_first_isomorphism.v b/theories/Classes/theory/ua_first_isomorphism.v
index f35069ad0bd..e1ecd7526a6 100644
--- a/theories/Classes/theory/ua_first_isomorphism.v
+++ b/theories/Classes/theory/ua_first_isomorphism.v
@@ -6,6 +6,7 @@
 Require Import
   HSet
   Colimits.Quotient
+  Modalities.ReflectiveSubuniverse
   Classes.interfaces.canonical_names
   Classes.theory.ua_isomorphic
   Classes.theory.ua_subalgebra
@@ -213,7 +214,9 @@ Section first_isomorphism_surjection.
   Global Instance is_isomorphism_inc_first_isomorphism_surjection
     : IsIsomorphism (hom_inc_subalgebra B (in_image_hom f)).
   Proof.
-    apply is_isomorphism_inc_improper_subalgebra. apply S.
+    apply is_isomorphism_inc_improper_subalgebra.
+    intros s x; cbn.
+    apply center, S.
   Qed.
 
 (** The homomorphism [hom_first_isomorphism_surjection] is the
diff --git a/theories/Colimits/Pushout.v b/theories/Colimits/Pushout.v
index 400ea66d410..82785488857 100644
--- a/theories/Colimits/Pushout.v
+++ b/theories/Colimits/Pushout.v
@@ -235,7 +235,7 @@ Global Instance contr_pushout {A B C : Type} `{Contr A, Contr B, Contr C}
        (f : A -> B) (g : A -> C)
   : Contr (Pushout f g).
 Proof.
-  exists (pushl (center B)).
+  apply (Build_Contr _ (pushl (center B))).
   srapply Pushout_ind.
   - intros b; apply ap, path_contr.
   - intros c.
diff --git a/theories/Colimits/Sequential.v b/theories/Colimits/Sequential.v
index 87db05de536..f652fafd696 100644
--- a/theories/Colimits/Sequential.v
+++ b/theories/Colimits/Sequential.v
@@ -611,7 +611,7 @@ Global Instance trunc_seq_colim `{Univalence} {A : Sequence} k :
 Proof.
   revert A; induction k as [ | k IHk].
   - srapply contr_colim_contr_seq.
-  - intros A trH; srapply Colimit_ind.
+  - intros A trH; apply istrunc_S; srapply Colimit_ind.
     + intro n; revert trH; revert A; induction n as [ | n IHn].
       * intros A trH a; srapply Colimit_ind.
         { intros m b; revert b; revert a; revert trH; revert A; induction m as [ | m IHm].
diff --git a/theories/DProp.v b/theories/DProp.v
index 51c400d469c..09f66f622d5 100644
--- a/theories/DProp.v
+++ b/theories/DProp.v
@@ -127,7 +127,7 @@ Definition path_dhprop `{Univalence} {P Q : DHProp}
 
 Global Instance ishset_dprop `{Univalence} : IsHSet DProp.
 Proof.
-  intros P Q.
+  apply istrunc_S; intros P Q.
   refine (istrunc_equiv_istrunc _ (n := -1) (equiv_path_dprop P Q)).
 Defined.
 
diff --git a/theories/HFiber.v b/theories/HFiber.v
index 945300493fd..d5f4267a7ca 100644
--- a/theories/HFiber.v
+++ b/theories/HFiber.v
@@ -220,7 +220,8 @@ Global Instance istruncmap_ap {A B} n (f:A -> B) `{!IsTruncMap n.+1 f}
 Definition istruncmap_from_ap {A B} n (f:A -> B) `{!forall x y, IsTruncMap n (@ap _ _ f x y)}
   : IsTruncMap n.+1 f.
 Proof.
-  intros y [a p] [b q];
+  intro y; apply istrunc_S.
+  intros [a p] [b q];
     destruct q;
     exact (istrunc_equiv_istrunc _ (hfiber_ap p)).
 Defined.
diff --git a/theories/HIT/FreeIntQuotient.v b/theories/HIT/FreeIntQuotient.v
index f174099033e..073cebf9f1c 100644
--- a/theories/HIT/FreeIntQuotient.v
+++ b/theories/HIT/FreeIntQuotient.v
@@ -72,7 +72,8 @@ Section FreeIntAction.
       rewrite Circle_rec_beta_loop.
       unfold loop.
       exact (Coeq_rec_beta_cglue _ _ _ _).
-    - intros xu yv.
+    - apply istrunc_S.
+      intros xu yv.
       refine (istrunc_equiv_istrunc (n := -1) _ (equiv_path_sigma _ xu yv)).
       destruct xu as [x u], yv as [y v]; cbn.
       apply hprop_allpath.
diff --git a/theories/HIT/Interval.v b/theories/HIT/Interval.v
index b58194bcce3..195e1c66675 100644
--- a/theories/HIT/Interval.v
+++ b/theories/HIT/Interval.v
@@ -46,7 +46,7 @@ Defined.
 
 Global Instance contr_interval : Contr interval | 0.
 Proof.
-  exists zero.
+  apply (Build_Contr _ zero).
   refine (interval_ind _ 1 seg _).
   refine (transport_paths_r _ _ @ concat_1p _).
 Defined.
diff --git a/theories/HIT/epi.v b/theories/HIT/epi.v
index 00737913272..ac4e2684f3c 100644
--- a/theories/HIT/epi.v
+++ b/theories/HIT/epi.v
@@ -1,6 +1,7 @@
 Require Import Basics.
 Require Import Types.
 Require Import TruncType.
+Require Import ReflectiveSubuniverse.
 Require Import Colimits.Pushout Truncations.Core HIT.SetCone.
 
 Local Open Scope path_scope.
@@ -28,7 +29,7 @@ Proof.
   (** TODO(JasonGross): Can we do this entirely by chaining equivalences? *)
   apply equiv_iff_hprop.
   { intro hepi.
-    refine {| center := (g; idpath) |}.
+    nrapply (Build_Contr _ (g; idpath)).
     intro xy; specialize (hepi xy).
     apply path_sigma_uncurried.
     exists hepi.
@@ -55,7 +56,7 @@ Section cones.
   Lemma isepi'_contr_cone `{Funext} {A B : HSet} (f : A -> B) : isepi' f -> Contr (setcone f).
   Proof.
     intros hepi.
-    exists (setcone_point _).
+    apply (Build_Contr _ (setcone_point _)).
     pose (alpha1 := @pglue A B Unit f (const_tt _)).
     pose (tot:= { h : B -> setcone f & tr o push o inl o f = h o f }).
     transparent assert (l : tot).
@@ -160,7 +161,8 @@ Section isepi_issurj.
     assert (X0 : forall x : setcone f, fam x = fam (setcone_point f)).
     { intros. apply contr_dom_equiv. apply i. }
     specialize (X0 (tr (push (inl y)))). simpl in X0.
-    exact (transport Contr (ap trunctype_type X0)^ _).
+    unfold IsConnected.
+    refine (transport (fun A => Contr A) (ap trunctype_type X0)^ _); exact _.
   Defined.
 End isepi_issurj.
 
diff --git a/theories/HIT/quotient.v b/theories/HIT/quotient.v
index 9f62649f72c..b42e68a37d9 100644
--- a/theories/HIT/quotient.v
+++ b/theories/HIT/quotient.v
@@ -176,7 +176,7 @@ Section Equiv.
     intros ? ? dclass. apply quotient_ind with dclass.
     - simple refine (quotient_ind R (fun x => IsHSet (P x)) _ _); cbn beta; try exact _.
       intros; apply path_ishprop.
-    - intros. apply Hprop'.
+    - intros. apply path_ishprop.
   Defined.
 
   (** From Ch6 *)
diff --git a/theories/HProp.v b/theories/HProp.v
index fdebce2ff8d..b9070a95b13 100644
--- a/theories/HProp.v
+++ b/theories/HProp.v
@@ -12,17 +12,11 @@ Generalizable Variables A B.
 Theorem equiv_hprop_allpath `{Funext} (A : Type)
   : IsHProp A <~> (forall (x y : A), x = y).
 Proof.
-  apply (equiv_adjointify (@path_ishprop A) (@hprop_allpath A));
-  (* The proofs of the two homotopies making up this equivalence are almost identical.  First we start with a thing [f]. *)
-    intro f;
-  (* Then we apply funext a couple of times *)
-    apply path_forall; intro x;
-    apply path_forall; intro y;
-  (* Now we conclude that [A] is contractible *)
-    try pose (C := Build_Contr A x (f x));
-    try pose (D := contr_inhabited_hprop A x);
-  (* And conclude because we have a path in a contractible space. *)
-    apply path_contr.
+  rapply (equiv_iff_hprop (@path_ishprop A) (@hprop_allpath A)).
+  apply hprop_allpath; intros f g.
+  funext x y.
+  pose (C := Build_Contr A x (f x)).
+  apply path_contr.
 Defined.
 
 Theorem equiv_hprop_inhabited_contr `{Funext} {A}
@@ -30,9 +24,9 @@ Theorem equiv_hprop_inhabited_contr `{Funext} {A}
 Proof.
   apply (equiv_adjointify (@contr_inhabited_hprop A) (@hprop_inhabited_contr A)).
   - intro ic. by_extensionality x.
-    apply @path_contr. apply contr_contr. exact (ic x).
-  - intro hp. by_extensionality x. by_extensionality y.
-    apply @path_contr. apply contr_contr. exact (hp x y).
+    apply @path_contr. apply contr_istrunc. exact (ic x).
+  - intro hp.
+    apply path_ishprop.
 Defined.
 
 (** Being an hprop is also equivalent to the diagonal being an equivalence. *)
diff --git a/theories/HSet.v b/theories/HSet.v
index bac56b31f06..27450f4b126 100644
--- a/theories/HSet.v
+++ b/theories/HSet.v
@@ -13,12 +13,13 @@ Definition axiomK A := forall (x : A) (p : x = x), p = idpath x.
 Definition axiomK_hset {A} : IsHSet A -> axiomK A.
 Proof.
   intros H x p.
-  apply (H x x p (idpath x)).
+  nrapply path_ishprop.
+  exact (H x x).
 Defined.
 
 Definition hset_axiomK {A} `{axiomK A} : IsHSet A.
 Proof.
-  intros x y H.
+  apply istrunc_S; intros x y.
   apply @hprop_allpath.
   intros p q.
   by induction p.
@@ -33,8 +34,8 @@ Proof.
   - intros K. by_extensionality x. by_extensionality x'.
     cut (Contr (x=x)).
     + intro. eapply path_contr.
-    + exists 1. intros. symmetry; apply K.
-  - intro K. by_extensionality x. by_extensionality x'.
+    + apply (Build_Contr _ 1). intros. symmetry; apply K.
+  - intro K.
     eapply path_ishprop.
 Defined.
 
diff --git a/theories/Homotopy/ClassifyingSpace.v b/theories/Homotopy/ClassifyingSpace.v
index 07a171a8383..2ba6959f7ee 100644
--- a/theories/Homotopy/ClassifyingSpace.v
+++ b/theories/Homotopy/ClassifyingSpace.v
@@ -150,7 +150,7 @@ End Eliminators.
 Global Instance isconnected_classifyingspace {G : Group}
   : IsConnected 0 (ClassifyingSpace G).
 Proof.
-  exists (tr bbase).
+  apply (Build_Contr _ (tr bbase)).
   srapply Trunc_ind.
   srapply ClassifyingSpace_ind_hprop; reflexivity.
 Defined.
diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
index 6c60c8c14e9..23631ce7f0a 100644
--- a/theories/Homotopy/ExactSequence.v
+++ b/theories/Homotopy/ExactSequence.v
@@ -130,7 +130,7 @@ Defined.
 (** If Y is a set, then IsComplex is an HProp. *)
 Global Instance ishprop_iscomplex_hset `{Univalence} {F X Y : pType} `{IsHSet Y}
   (i : F ->* X) (f : X ->* Y)
-  : IsHProp (IsComplex i f) := {}.
+  : IsHProp (IsComplex i f) := _.
 
 (** ** Very short exact sequences and fiber sequences *)
 
@@ -151,7 +151,8 @@ Global Instance ishprop_isexact_hset `{Univalence} {F X Y : pType} `{IsHSet Y}
   (n : Modality) (i : F ->* X) (f : X ->* Y)
   : IsHProp (IsExact n i f).
 Proof.
-  rapply (transport IsHProp (x := { cx : IsComplex i f & IsConnMap n (cxfib cx) })).
+  rapply (transport (fun A => IsHProp A) (x := { cx : IsComplex i f & IsConnMap n (cxfib cx) })).
+  2: exact _.
   apply path_universe_uncurried; issig.
 Defined.
 
@@ -164,7 +165,7 @@ Proof.
   rapply (O_functor O (A:=hfiber (cxfib cx_isexact) (x; p))).
   - intros [z q].
     exact (z; ap pr1 q).
-  - apply conn_map_isexact.
+  - apply center, conn_map_isexact.
 Defined.
 
 (** Bundled version of the above. *)
diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
index 06fa446b779..561f6195da7 100644
--- a/theories/Homotopy/Join/Core.v
+++ b/theories/Homotopy/Join/Core.v
@@ -749,7 +749,7 @@ Section JoinTrunc.
   (** Joining with a contractible type produces a contractible type *)
   Global Instance contr_join A B `{Contr A} : Contr (Join A B).
   Proof.
-    exists (joinl (center A)).
+    apply (Build_Contr _ (joinl (center A))).
     snrapply Join_ind.
     - intros a; apply ap, contr.
     - intros b; apply jglue.
diff --git a/theories/Limits/Pullback.v b/theories/Limits/Pullback.v
index f8abd085c5d..c3db9bf3ddf 100644
--- a/theories/Limits/Pullback.v
+++ b/theories/Limits/Pullback.v
@@ -324,7 +324,7 @@ Proof.
   srapply equiv_adjointify.
   - intros [p q].
     refine (p; q; _).
-    apply (istrunc_sq (-2)).
+    apply (@center _ (istrunc_sq (-2))).
   - intros [p [q _]].
     exact (p, q).
   - intros [p [q ?]].
@@ -333,7 +333,7 @@ Proof.
     refine (transport_sigma' _ _ @ _).
     srapply path_sigma'.
     1: reflexivity.
-    apply (istrunc_sq (-2)).
+    apply path_ishprop.
   - reflexivity.
 Defined.
 
diff --git a/theories/Metatheory/FunextVarieties.v b/theories/Metatheory/FunextVarieties.v
index 781395cb330..f3caa108cd2 100644
--- a/theories/Metatheory/FunextVarieties.v
+++ b/theories/Metatheory/FunextVarieties.v
@@ -44,7 +44,7 @@ Definition NaiveFunext_implies_WeakFunext@{i j max}
   : NaiveFunext@{i j max} -> WeakFunext@{i j max}.
 Proof.
   intros nf A P Pc.
-  exists (fun x => center (P x)).
+  apply (Build_Contr _ (fun x => center (P x))).
   intros f; apply nf; intros x.
   apply contr.
 Defined.
@@ -74,7 +74,7 @@ Section Homotopies.
   Global Instance contr_basedhtpy : Contr {g : forall x, B x & f == g } | 1.
   Proof.
     unfold WeakFunext in wf.    (* Allow typeclass inference to find it *)
-    exists (f;idhtpy). intros [g h].
+    apply (Build_Contr _ (f;idhtpy)). intros [g h].
     (* The trick is to show that the type [{g : forall x, B x & f == g }] is a retract of [forall x, {y : B x & f x = y}], which is contractible due to J and weak funext.  Here are the retraction and its section. *)
     pose (r := fun k => exist (fun g => f == g)
       (fun x => (k x).1) (fun x => (k x).2)).
diff --git a/theories/Modalities/Closed.v b/theories/Modalities/Closed.v
index c6872d96815..597eedd8a91 100644
--- a/theories/Modalities/Closed.v
+++ b/theories/Modalities/Closed.v
@@ -83,7 +83,7 @@ Proof.
       pose (X_inO u).
       apply ooextendable_contr; exact _.
     + intros ext u.
-      exists ((fst (ext u 1%nat) Empty_rec).1 tt); intros x.
+      apply (Build_Contr _ ((fst (ext u 1%nat) Empty_rec).1 tt)); intros x.
       unfold const in ext.
       exact ((fst (snd (ext u 2) (fst (ext u 1%nat) Empty_rec).1
                        (fun _ => x)) (Empty_ind _)).1 tt).
diff --git a/theories/Modalities/Fracture.v b/theories/Modalities/Fracture.v
index 3315b2b2dfb..72a7a0651d1 100644
--- a/theories/Modalities/Fracture.v
+++ b/theories/Modalities/Fracture.v
@@ -76,22 +76,23 @@ It may sometimes happen that in addition, the "intersection" of [O1] and [O2] is
                (BCf : { B : Type_ O1 & { C : Type_ O2 & C -> O2 B }})
     : fracture_unglue (fracture_glue_uncurried BCf) = BCf.
     Proof.
-      destruct BCf as [B [C f]]; simpl.
+      destruct BCf as [B [C f]].
       (** The first two components of our path will be applications of univalence.  We begin by observing that maps we will use are equivalences. *)
       assert (IsEquiv (O_rec ((to O2 B)^*' f))).
       { apply isequiv_O_rec_O_inverts.
         apply O_inverts_conn_map, conn_map_pullback'.
-        intros ob; apply isconnectedo1_ino2; exact _. }
+        intros ob; apply isconnectedo1_ino2.
+        rapply mapinO_between_inO. }
       assert (IsEquiv (O_rec (f^* (to O2 B)))).
       { apply isequiv_O_rec_O_inverts.
         apply O_inverts_conn_map, conn_map_pullback; exact _. }
       (** Now we start building the path. *)
       simple refine (path_sigma' _ _ _).
-      { apply path_TypeO; simpl.
+      { apply path_TypeO; unfold ".1", ".2".
         refine (path_universe (O_rec ((to O2 B)^*' f))). }
-      refine (transport_sigma' _ _ @ _); simpl.
+      refine (transport_sigma' _ _ @ _); unfold ".1", ".2".
       simple refine (path_sigma' _ _ _).
-      { apply path_TypeO; simpl.
+      { apply path_TypeO; unfold ".1", ".2".
         refine (path_universe (O_rec (f^* (to O2 B)))). }
       (** It remains to identify the induced function with the given [f].  We begin with some boilerplate. *)
       apply path_arrow; intros c.
@@ -125,10 +126,10 @@ It may sometimes happen that in addition, the "intersection" of [O1] and [O2] is
         refine (O_functor_homotopy O2 _ _ (O_rec_beta _) _ @ _).
         revert c; equiv_intro (O_rec (f^* (to O2 B))) x.
         refine (ap _ (eissect _ _) @ _).
-        revert x; apply O_indpaths; intros x; simpl.
-        refine (to_O_natural O2 _ x @ _); simpl.
+        revert x; apply O_indpaths; intros x.
+        refine (to_O_natural O2 _ x @ _).
         refine (_ @ ap f (O_rec_beta _ _)^).
-        destruct x as [a [b q]]; simpl; exact (q^).
+        destruct x as [a [b q]]; exact (q^).
     Qed.
 
     Definition fracture_unglue_issect `{Univalence} (A : Type)
@@ -162,7 +163,7 @@ Definition gluable_open_closed `{Funext} (U : HProp)
 Proof.
   intros A.
   change (Contr (U -> A) -> (U -> Contr A)); intros ? u.
-  exists (center (U -> A) u); intros a.
+  apply (Build_Contr _ (center (U -> A) u)); intros a.
   exact (ap10 (path_contr _ (fun _ => a)) u).
 Defined.
 
@@ -171,7 +172,7 @@ Definition disjoint_open_closed `{Funext} (U : HProp)
 Proof.
   intros A.
   change ((U -> Contr A) -> Contr (U -> A)); intros uc.
-  exists (fun u => let i := uc u in center A).
+  apply (Build_Contr _ (fun u => let i := uc u in center A)).
   intros f; apply path_arrow; intros u.
   pose (uc u); apply path_contr.
 Defined.
@@ -191,8 +192,7 @@ Proof.
       refine (equiv_isequiv (@equiv_contr_contr U Unit _ _)).
     - refine (isequiv_adjointify _ (to (Op' U) A) _ _).
       + intros a; apply O_rec_beta.
-      + intros oa; revert oa; apply O_indpaths; intros a; simpl.
-        apply ap. rapply O_rec_beta. }
+      + apply O_indpaths; cbn. reflexivity. }
   apply ooextendable_contr; exact _.
 Defined.
 
diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
index 2f4fd07c11b..ce79479cd72 100644
--- a/theories/Modalities/Lex.v
+++ b/theories/Modalities/Lex.v
@@ -192,7 +192,8 @@ Section LexModality.
   Proof.
     generalize dependent A; simple_induction n n IHn; intros A ?.
     - exact _.               (** Already proven for all modalities. *)
-    - refine (O_ind (fun x => forall y, IsTrunc n (x = y)) _); intros x.
+    - apply istrunc_S.
+      refine (O_ind (fun x => forall y, IsTrunc n (x = y)) _); intros x.
       refine (O_ind (fun y => IsTrunc n (to O A x = y)) _); intros y.
       refine (istrunc_equiv_istrunc _ (equiv_path_O x y)).
   Defined.
diff --git a/theories/Modalities/Localization.v b/theories/Modalities/Localization.v
index 919c3fc7a2b..ce004a1ca6f 100644
--- a/theories/Modalities/Localization.v
+++ b/theories/Modalities/Localization.v
@@ -349,7 +349,7 @@ Proof.
     intros i.
     apply ishprop_ooextendable@{a a i i i
                                 i i i i i
-                                i i i i i}.
+                                i i i i i i}.
   - apply islocal_equiv_islocal.
   - apply islocal_localize.
   - cbn. intros Q Q_inO.
diff --git a/theories/Modalities/Nullification.v b/theories/Modalities/Nullification.v
index effc14fddad..219edcb5f4e 100644
--- a/theories/Modalities/Nullification.v
+++ b/theories/Modalities/Nullification.v
@@ -56,11 +56,11 @@ Proof.
       apply ooextendable_over_unit; intros c.
       refine (ooextendable_postcompose@{a a i i i i i i i i}
                 (fun (_:Unit) => B (c tt)) _ _
-                (fun u => transport B (ap c (path_unit@{a} tt u))) _).
+                (fun u => transport B (ap@{Set _} c (path_unit tt u))) _).
       refine (ooextendable_islocal _ i).
     + reflexivity.
     + apply inO_paths@{i i}.
-  Defined.
+Defined.
 
 (** And here is the "real" definition of the notation [IsNull]. *)
 Notation IsNull f := (In (Nul f)).
diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index 8253f8bc00a..ca73853d54c 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -68,11 +68,11 @@ Definition Type_@{i j} (O : Subuniverse@{i}) : Type@{j}
 Coercion TypeO_pr1 O (T : Type_ O) := @pr1 Type (In O) T.
 
 (** The second component of [TypeO] is unique.  *)
-Definition path_TypeO@{i j} {fs : Funext} O (T T' : Type_ O) (p : T.1 = T'.1)
+Definition path_TypeO@{i j} {fs : Funext} O (T T' : Type_@{i j} O) (p : T.1 = T'.1)
   : T = T'
   := path_sigma_hprop@{j i j} T T' p.
 
-Definition equiv_path_TypeO@{i j} {fs : Funext} O (T T' : Type_ O)
+Definition equiv_path_TypeO@{i j} {fs : Funext} O (T T' : Type_@{i j} O)
   : (paths@{j} T.1 T'.1) <~> (T = T')
   := equiv_path_sigma_hprop@{j i j} T T'.
 
@@ -702,7 +702,7 @@ Section Reflective_Subuniverse.
     Global Instance contr_typeof_O_unit `{Univalence} (A : Type)
     : Contr (typeof_to_O A).
     Proof.
-      exists (O A ; (to O A ; (_ , _))).
+      apply (Build_Contr _ (O A ; (to O A ; (_ , _)))).
       intros [OA [Ou [? ?]]].
       pose (f := O_rec Ou : O A -> OA).
       pose (g := (O_functor Ou)^-1 o to O OA : (OA -> O A)).
@@ -1049,8 +1049,7 @@ Section Reflective_Subuniverse.
       generalize dependent A; simple_induction n n IH; intros A ?.
       - (** We have to be slightly clever here: the actual definition of [Contr] involves a sigma, which [O] is not generally closed under, but fortunately we have [equiv_contr_inhabited_allpath]. *)
         refine (inO_equiv_inO _ equiv_contr_inhabited_allpath^-1).
-      - change (In O (forall x y:A, IsTrunc n (x=y))).
-        exact _.
+      - refine (inO_equiv_inO _ (equiv_istrunc_unfold n.+1 A)^-1).
     Defined.
 
     (** ** Coproducts *)
@@ -1373,7 +1372,7 @@ Section ConnectedTypes.
   : NullHomotopy (to O A) -> IsConnected O A.
   Proof.
     intros nh.
-    exists (nh .1).
+    apply (Build_Contr _ (nh .1)).
     rapply O_indpaths.
     intros x; symmetry; apply (nh .2).
   Defined.
diff --git a/theories/Modalities/Separated.v b/theories/Modalities/Separated.v
index 8d6bc57f781..d02da34f7bb 100644
--- a/theories/Modalities/Separated.v
+++ b/theories/Modalities/Separated.v
@@ -120,10 +120,11 @@ Proof.
 Defined.
 
 (* As a special case, if X embeds into an n-type for n >= -1 then X is an n-type. Note that this doesn't hold for n = -2. *)
-Corollary istrunc_embedding_trunc `{Funext} {X Y : Type} {n : trunc_index} `{IsTrunc n.+1 Y}
-      (i : X -> Y) `{IsEmbedding i} : IsTrunc n.+1 X.
+Corollary istrunc_embedding_trunc `{Funext} {X Y : Type} {n : trunc_index} `{istr : IsTrunc n.+1 Y}
+      (i : X -> Y) `{isem : IsEmbedding i} : IsTrunc n.+1 X.
 Proof.
-  exact (@in_SepO_embedding (Tr n) _ _ i IsEmbedding0 H0).
+  apply istrunc_S.
+  exact (@in_SepO_embedding (Tr n) _ _ i isem istr).
 Defined.
 
 Global Instance in_SepO_hprop (O : ReflectiveSubuniverse)
diff --git a/theories/Modalities/Topological.v b/theories/Modalities/Topological.v
index e0a4618bf8b..0a1c7420bfa 100644
--- a/theories/Modalities/Topological.v
+++ b/theories/Modalities/Topological.v
@@ -129,7 +129,7 @@ Proof.
           rapply (isconnected_acc_ngen (Nul D) (inr (a;(b,x)))). }
         pose (p := conn_map_elim (Nul D) (unit_name b)
                                  (fun u => f b = f u) (fun _ => 1)).
-        exists (f b ; p); intros [x q].
+        apply (Build_Contr _ (f b ; p)); intros [x q].
         refine (path_sigma' _ (q b)^ _); apply path_forall.
         refine (conn_map_elim (Nul D) (unit_name b) _ _); intros [].
         rewrite transport_forall_constant, transport_paths_l, inv_V.
diff --git a/theories/NullHomotopy.v b/theories/NullHomotopy.v
index 7dab6bb37e2..ee0b1831ec9 100644
--- a/theories/NullHomotopy.v
+++ b/theories/NullHomotopy.v
@@ -19,7 +19,7 @@ Section NullHomotopy.
   Proof.
     apply @istrunc_sigma; auto.
     intros y. apply (@istrunc_forall _).
-    intros x. apply istrunc_succ.
+    intros x. apply istrunc_paths'.
   Defined.
 
   Definition nullhomotopy_homotopic {X Y : Type} {f g : X -> Y} (p : f == g)
diff --git a/theories/PathAny.v b/theories/PathAny.v
index 359858e14f1..d4b302acb53 100644
--- a/theories/PathAny.v
+++ b/theories/PathAny.v
@@ -52,7 +52,7 @@ Definition contr_sigma_sigma (A : Type) (B : A -> Type)
 Proof.
   pose (d := (center {y:B a & D a y c}).2).
   set (b := (center {y:B a & D a y c}).1) in *.
-  exists ((a;b);(c;d)).
+  apply (Build_Contr _ ((a;b);(c;d))).
   intros [[a' b'] [c' d']]; cbn in *.
   pose (ac' := (a';c')).
   pose (bd' := (b';d') : {y:B ac'.1 & D ac'.1 y ac'.2}).
diff --git a/theories/Pointed/Loops.v b/theories/Pointed/Loops.v
index 415f64c0415..00c016388c3 100644
--- a/theories/Pointed/Loops.v
+++ b/theories/Pointed/Loops.v
@@ -397,9 +397,10 @@ Theorem equiv_istrunc_istrunc_loops `{Univalence} n X
 Proof.
   srapply equiv_iff_hprop.
   intro tr_loops.
-  intros x y p.
+  apply istrunc_S; intros x y.
+  apply istrunc_S; intros p.
   destruct p.
-  apply tr_loops.
+  nrapply tr_loops.
 Defined.
 
 (* 7.2.9, with [n] here meaning the same as [n-1] there. Note that [n.-1] in the statement is short for [trunc_index_pred (nat_to_trunc_index n)] which is definitionally equal to [(trunc_index_inc minus_two n).+1]. *)
diff --git a/theories/PropResizing/Nat.v b/theories/PropResizing/Nat.v
index 7fef7b7ff9f..4a912a322bd 100644
--- a/theories/PropResizing/Nat.v
+++ b/theories/PropResizing/Nat.v
@@ -265,6 +265,7 @@ Section AssumeStuff.
 
   Instance ishset_N@{} : IsHSet N.
   Proof.
+    apply istrunc_S.
     intros n m.
     change (IsHProp (n = m)).
     refine (istrunc_equiv_istrunc (n.1 = m.1) (equiv_path_sigma_hprop n m)).
@@ -302,7 +303,7 @@ Section AssumeStuff.
   Local Instance ishprop_graph_zero_or_succ@{} : forall n : Graph,
       IsHProp ((n = graph_zero) + { m : N & n = graph_succ m.1 }).
   Proof.
-    intros n. apply ishprop_sum@{p u p}.
+    intros n. apply ishprop_sum@{u p p}.
     - apply (@istrunc_equiv_istrunc _ _ (equiv_path_inverse _ _)),ishprop_path_graph_in_N.
       exact zero.2.
     - apply @ishprop_sigma_disjoint.
@@ -581,7 +582,7 @@ Section AssumeStuff.
 
   Instance contr_le_zero@{} : Contr {n:N & n <= zero}.
   Proof.
-    exists (exist (fun n => n <= zero) zero (N_zero_le zero)).
+    apply (Build_Contr _ (exist (fun n => n <= zero) zero (N_zero_le zero))).
     intros [n H].
     apply path_sigma_hprop.
     exact (N_le_zero n H)^.
@@ -810,7 +811,7 @@ Section AssumeStuff.
                 apply path_ishprop.
               - apply concat_1p. }
         + intros [f H].
-          exists (fun mh => Empty_rec (N_lt_zero mh.1 mh.2)).
+          apply (Build_Contr _ (fun mh => Empty_rec (N_lt_zero mh.1 mh.2))).
           intros g.
           apply path_forall; intros m.
           destruct (N_lt_zero m.1 m.2).
@@ -825,7 +826,7 @@ Section AssumeStuff.
       - apply equiv_precompose'.
         apply equiv_N_segment_succ.
       - apply equiv_functor_prod_l.
-        apply equiv_unit_rec@{x nr Set}.
+        apply equiv_unit_rec@{x nr}.
     Defined.
 
     Local Definition equiv_seg_succ@{} (n m : N) (H : m < succ n)
diff --git a/theories/Sets/GCH.v b/theories/Sets/GCH.v
index c37a7df831c..4dc68b29a61 100644
--- a/theories/Sets/GCH.v
+++ b/theories/Sets/GCH.v
@@ -34,10 +34,10 @@ Lemma hprop_GCH {PR : PropResizing} {FE : Funext} :
 Proof.
   repeat (nrapply istrunc_forall; intros).
   apply hprop_allpath. intros [H|H] [H'|H'].
-  - enough (H = H') as ->; trivial. apply (InjectsInto a0 a).
+  - enough (H = H') as ->; trivial. apply path_ishprop.
   - apply Empty_rec. eapply merely_destruct; try eapply (Cantor_inj a); trivial. now apply InjectsInto_trans with a0.
   - apply Empty_rec. eapply merely_destruct; try eapply (Cantor_inj a); trivial. now apply InjectsInto_trans with a0.
-  - enough (H = H') as ->; trivial. apply (InjectsInto (a -> HProp) a0).
+  - enough (H = H') as ->; trivial. apply path_ishprop.
 Qed.
 
 
@@ -82,7 +82,7 @@ Section LEM.
     intros [p Hp] [q Hq]; cbn.
     intros ->. unshelve eapply path_sigma; cbn.
     - reflexivity.
-    - cbn. apply (r q).
+    - cbn. apply path_ishprop.
   Qed.
 
   Lemma inject_sings :
diff --git a/theories/Sets/GCHtoAC.v b/theories/Sets/GCHtoAC.v
index 63fec8f30be..06fddf89259 100644
--- a/theories/Sets/GCHtoAC.v
+++ b/theories/Sets/GCHtoAC.v
@@ -73,10 +73,10 @@ Proof.
   - exact (fun b : Bool => if b then merely Unit else merely Empty).
   - intros []; destruct LEM as [H|H]; auto.
     + destruct (H (tr tt)).
-    + apply (@merely_destruct Empty); easy.
+    + apply (@merely_destruct Empty); try easy. exact _.
   - intros P. destruct LEM as [H|H]; apply equiv_path_iff_hprop.
     + split; auto. intros _. apply tr. exact tt.
-    + split; try easy. intros HE. apply (@merely_destruct Empty); easy.
+    + split; try easy. intros HE. apply (@merely_destruct Empty); try easy. exact _.
 Qed.
 
 Lemma path_bool_subsingleton :
@@ -92,7 +92,7 @@ Proof.
   - intros x. destruct (LEM (p x) _) as [H|H]; [left | right]; now exists x.
   - intros [[x _]|[x _]]; exact x.
   - cbn. intros [[x Hx]|[x Hx]]; destruct LEM as [H|H]; try contradiction.
-    + enough (H = Hx) as -> by reflexivity. apply p.
+    + enough (H = Hx) as -> by reflexivity. apply path_ishprop.
     + enough (H = Hx) as -> by reflexivity. apply path_forall. now intros HP.
   - cbn. intros x. now destruct LEM.
 Qed.
diff --git a/theories/Sets/Hartogs.v b/theories/Sets/Hartogs.v
index d29047171a6..59acd93ec3e 100644
--- a/theories/Sets/Hartogs.v
+++ b/theories/Sets/Hartogs.v
@@ -31,7 +31,7 @@ Section Hartogs_Number.
 
   Definition hartogs_number' : Ordinal.
   Proof.
-    set (carrier := {B : Ordinal & card B <= card A}).
+    set (carrier := {B : Ordinal@{A _} & card B <= card A}).
     set (relation := fun (B C : carrier) => B.1 < C.1).
 
     exists carrier relation. srapply (isordinal_simulation pr1).
@@ -225,7 +225,7 @@ Section Hartogs_Number.
     - snrapply isequiv_surj_emb.
       + apply BuildIsSurjection. intros [X HX]. eapply merely_destruct.
         * eapply equiv_resize_hprop, HX.
-        * intros [a <-]. cbn. apply tr. exists a. cbn. apply ap. apply ishprop_resize_hprop.
+        * intros [a <-]. cbn. apply tr. exists a. cbn. apply ap. apply path_ishprop.
       + apply isembedding_isinj_hset. intros a b. intros H % pr1_path. cbn in H.
         specialize (injective_uni_fix (hartogs_number'_injection.1 a) (hartogs_number'_injection.1 b)).
         intros H'. apply H' in H. now apply hartogs_number'_injection.2.
@@ -253,7 +253,7 @@ Section Hartogs_Number.
     exists f : hartogs_number -> 𝒫 (𝒫 (𝒫 A)), IsInjective f.
   Proof.  
     cbn. exists proj1. intros [X HX] [Y HY]. cbn. intros ->.
-    apply ap. apply ishprop_resize_hprop.
+    apply ap. apply path_ishprop.
   Qed.
 
   Lemma ordinal_initial (O : Ordinal) (a : O) :
@@ -278,20 +278,23 @@ Section Hartogs_Number.
     transparent assert (HNO : hartogs_number'). { exists hartogs_number. apply HN. }
     apply (ordinal_initial hartogs_number' HNO).
     eapply (transitive_Isomorphism hartogs_number' hartogs_number).
-    - apply isomorphism_inverse, resize_ordinal_iso.
+    - apply isomorphism_inverse.
+      unfold hartogs_number.
+      exact (resize_ordinal_iso hartogs_number' hartogs_number_carrier hartogs_equiv).
     - assert (Isomorphism hartogs_number ↓hartogs_number) by apply isomorphism_to_initial_segment.
       eapply transitive_Isomorphism; try apply X.
       unshelve eexists.
       + srapply equiv_adjointify.
         * intros [a Ha % equiv_resize_hprop]. unshelve eexists.
-          -- exists a. eapply transitive_card; try apply HN.
-             now apply le_Cardinal_lt_Ordinal.
+          -- exists a. transitivity (card hartogs_number).
+             ++ nrapply le_Cardinal_lt_Ordinal; apply Ha.
+             ++ apply HN.
           -- apply equiv_resize_hprop. cbn. exact Ha.
         * intros [[a Ha] H % equiv_resize_hprop]. exists a.
           apply equiv_resize_hprop. apply H.
         * intros [[a Ha] H]. apply path_sigma_hprop. apply path_sigma_hprop. reflexivity.
         * intros [a Ha]. apply path_sigma_hprop. reflexivity.
       + intros [[a Ha] H1] [[b H] H2]. cbn. reflexivity.
-  Qed.
+  Defined.
 
 End Hartogs_Number.
diff --git a/theories/Sets/Ordinals.v b/theories/Sets/Ordinals.v
index 4c13272b018..4856dd65ecf 100644
--- a/theories/Sets/Ordinals.v
+++ b/theories/Sets/Ordinals.v
@@ -141,17 +141,7 @@ Proof.
   split; apply H.
 Defined.
 
-
-Global Instance transitive_iff
-  : Transitive iff.
-Proof.
-  intros A B C A_B B_C.
-  split.
-  - intros a. apply B_C. apply A_B. exact a.
-  - intros c. apply A_B. apply B_C. exact c.
-Qed.
-
-
+(** We state this first without using [Transitive] to allow more general universe variables. *)
 Lemma transitive_Isomorphism
   : forall A B C,
     Isomorphism A B
@@ -167,22 +157,9 @@ Proof.
   - intros gfa_gfa'. apply Hf. apply Hg. exact gfa_gfa'.
 Defined.
 
-
 Global Instance isomorphism_compose_backwards
-  : Transitive Isomorphism.
-Proof.
-  intros [A R__A] [B R__B] [C R__C] [f Hf] [g Hg].
-  exists (equiv_compose' g f).
-  intros a a'.
-  transitivity (R__B (f a) (f a')). {
-    apply Hf.
-  }
-  apply Hg.
-Qed.
-
-
-
-
+  : Transitive Isomorphism
+  := transitive_Isomorphism.
 
 Definition equiv_path_Ordinal `{Univalence} (A B : Ordinal)
   : Isomorphism A B <~> A = B.
@@ -408,6 +385,7 @@ Qed.
 Global Instance ishset_Ordinal `{Univalence}
   : IsHSet Ordinal.
 Proof.
+  apply istrunc_S.
   intros A B.
   apply (istrunc_equiv_istrunc (Isomorphism A B)). {
     apply equiv_path_Ordinal.
diff --git a/theories/Sets/Powers.v b/theories/Sets/Powers.v
index 2f27ff2e335..0d381527721 100644
--- a/theories/Sets/Powers.v
+++ b/theories/Sets/Powers.v
@@ -30,15 +30,20 @@ Definition power_iterated_shift X n
 Global Instance hset_power {UA : Univalence} (X : HSet)
   : IsHSet (X -> HProp).
 Proof.
+  apply istrunc_S.
   intros p q. apply hprop_allpath. intros H H'.
   destruct (equiv_path_arrow p q) as [f [g Hfg Hgf _]].
   rewrite <- (Hfg H), <- (Hfg H'). apply ap. apply path_forall.
-  intros x. apply isset_HProp.
+  intros x. apply path_ishprop.
 Qed.
 
 Global Instance hset_power_iterated {UA : Univalence} (X : HSet) n
-  : IsHSet (power_iterated X n)
-  := nat_iter_invariant _ _ _ _ _ _.
+  : IsHSet (power_iterated X n).
+Proof.
+  nrapply (nat_iter_invariant n power_type (fun A => IsHSet A)).
+  - intros Y HS. rapply hset_power.
+  - exact _.
+Defined.
 
 Lemma Injection_power_iterated {UA : Univalence} {PR : PropResizing} (X : HSet) n
   : Injection X (power_iterated X n).
diff --git a/theories/Spaces/BAut.v b/theories/Spaces/BAut.v
index 8e763b29b4f..1cddc92768d 100644
--- a/theories/Spaces/BAut.v
+++ b/theories/Spaces/BAut.v
@@ -62,6 +62,7 @@ Ltac baut_reduce :=
 Global Instance trunc_baut `{Univalence} {n X} `{IsTrunc n.+1 X}
 : IsTrunc n.+2 (BAut X).
 Proof.
+  apply istrunc_S.
   intros Z W.
   baut_reduce.
   exact (@istrunc_equiv_istrunc _ _ (path_baut _ _) n.+1 _).
diff --git a/theories/Spaces/BAut/Rigid.v b/theories/Spaces/BAut/Rigid.v
index c8c60390dcc..ddcaad8d5c7 100644
--- a/theories/Spaces/BAut/Rigid.v
+++ b/theories/Spaces/BAut/Rigid.v
@@ -17,7 +17,7 @@ Class IsRigid (A : Type) :=
 Global Instance contr_aut_rigid `{Funext} (A : Type) `{IsRigid A}
   : Contr (A <~> A).
 Proof.
-  exists equiv_idmap.
+  apply (Build_Contr _ equiv_idmap).
   intros f; apply path_equiv, path_arrow, path_aut_rigid.
 Defined.
 
@@ -28,6 +28,7 @@ Global Instance contr_baut_rigid `{Univalence} {A : Type} `{IsRigid A}
 Proof.
   refine (contr_change_center (point (BAut A))).
   refine (contr_trunc_conn (Tr 0)).
+  apply istrunc_S.
   intros Z W; baut_reduce.
   refine (istrunc_equiv_istrunc (n := -1) (A <~> A)
                       (path_baut (point (BAut A)) (point (BAut A)))).
diff --git a/theories/Spaces/Circle.v b/theories/Spaces/Circle.v
index 7b4db18e2e3..160fa46175a 100644
--- a/theories/Spaces/Circle.v
+++ b/theories/Spaces/Circle.v
@@ -210,6 +210,7 @@ Defined.
 (** It follows that the circle is a 1-type. *)
 Global Instance istrunc_Circle `{Univalence} : IsTrunc 1 Circle.
 Proof.
+  apply istrunc_S.
   intros x y.
   assert (p := merely_path_is0connected Circle base x).
   assert (q := merely_path_is0connected Circle base y).
diff --git a/theories/Spaces/Spheres.v b/theories/Spaces/Spheres.v
index dd0c653cc44..d1792fa74be 100644
--- a/theories/Spaces/Spheres.v
+++ b/theories/Spaces/Spheres.v
@@ -302,7 +302,7 @@ Proof.
   - (* n = -2 *) apply hprop_allpath.
     intros x0 x1. set (f := (fun b => if (S0_to_Bool b) then x0 else x1)).
     set (n := HX f). exact (n.2 North @ (n.2 South)^).
-  - (* n ≥ -1 *) intros x0 x1.
+  - (* n ≥ -1 *) apply istrunc_S; intros x0 x1.
     apply (istrunc_allnullhomot n').
     intro f. apply nullhomot_paths_from_susp, HX.
 Defined.
diff --git a/theories/TruncType.v b/theories/TruncType.v
index 179df606a4b..4a273775d18 100644
--- a/theories/TruncType.v
+++ b/theories/TruncType.v
@@ -73,7 +73,7 @@ Section TruncType.
   Proof.
     unfold path_trunctype; simpl.
     rewrite path_universe_compose_uncurried.
-    rewrite (path_sigma_hprop_pp _ _ _ (trunctype_istrunc B)).
+    rewrite (path_sigma_hprop_pp (path_universe_uncurried f) _ _ (trunctype_istrunc B)).
     refine (concat_p1 _ @ concat_1p _ @ _).
     refine (_ @ (ap _ (concat_1p _))^ @ (ap _ (concat_p1 _))^).
     refine (_ @ (ap (fun z => z @ _) (concat_1p _))^ @ (ap (fun z => z @ _) (concat_p1 _))^).
@@ -97,6 +97,7 @@ Section TruncType.
   Global Instance istrunc_trunctype {n : trunc_index}
     : IsTrunc n.+1 (TruncType n) | 0.
   Proof.
+    apply istrunc_S.
     intros A B.
     refine (istrunc_equiv_istrunc _ (equiv_path_trunctype@{i j} A B)).
     case n as [ | n'].
@@ -106,7 +107,7 @@ Section TruncType.
 
   Global Instance isset_HProp : IsHSet HProp := _.
 
-  Global Instance istrunc_sig_istrunc : forall n, IsTrunc n.+1 (sig (IsTrunc n)) | 0.
+  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).
diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v
index 6cc4674ff8c..b84d0244e05 100644
--- a/theories/Truncations/Connectedness.v
+++ b/theories/Truncations/Connectedness.v
@@ -41,10 +41,11 @@ Lemma istrunc_extension_along_conn `{Univalence} {m n : trunc_index}
 Proof.
   revert P HP d. induction m as [ | m' IH]; intros P HP d; simpl in *.
   (* m = –2 *)
-  - exists (extension_conn_map_elim n f P d).
+  - apply (Build_Contr _ (extension_conn_map_elim n f P d)).
     intros y. apply (allpath_extension_conn_map n); assumption.
     (* m = S m' *)
-  - intros e e'. refine (istrunc_isequiv_istrunc _ (path_extension e e')).
+  - apply istrunc_S.
+    intros e e'. refine (istrunc_isequiv_istrunc _ (path_extension e e')).
   (* magically infers: paths in extensions = extensions into paths, which by induction is m'-truncated. *)
 Defined.
 
@@ -175,7 +176,7 @@ Defined.
 Global Instance is0connected_component {X : Type} (x : X)
   : IsConnected 0 { z : X & merely (z = x) }.
 Proof.
-  exists (tr (x; tr idpath)).
+  apply (Build_Contr _ (tr (x; tr idpath))).
   rapply Trunc_ind; intros [Z p].
   strip_truncations.
   apply (ap tr).
diff --git a/theories/Truncations/Core.v b/theories/Truncations/Core.v
index 8729573e8a9..76dce533bf0 100644
--- a/theories/Truncations/Core.v
+++ b/theories/Truncations/Core.v
@@ -58,14 +58,15 @@ Definition Trunc_rec_tr n {A : Type}
 
 Definition Tr (n : trunc_index) : Modality.
 Proof.
-  srapply (Build_Modality (IsTrunc n)).
-  - intros A B ? f ?; apply (istrunc_isequiv_istrunc A f).
+  srapply (Build_Modality (fun A => IsTrunc n A)); cbn.
+  - intros A B ? f ?; rapply (istrunc_isequiv_istrunc A f).
   - exact (Trunc n).
   - intros; apply istrunc_truncation.
   - intros A; apply tr.
   - intros A B ? f oa; cbn in *.
     exact (Trunc_ind B f oa).
   - intros; reflexivity.
+  - exact (@istrunc_paths' n).
 Defined.
 
 (** We don't usually declare modalities as coercions, but this particular one is convenient so that lemmas about (for instance) connected maps can be applied to truncation modalities without the user/reader needing to be (particularly) aware of the general notion of modality. *)
@@ -244,7 +245,7 @@ Proof.
   rapply (Trunc_functor _ (X:= (hfiber (g o f) c))).
   - intros [a p].
     exact (f a; p).
-  - apply isconn.
+  - apply center, isconn.
 Defined.
 
 (** Retractions are surjective. *)
@@ -269,7 +270,8 @@ Definition isembedding_precompose_surjection_hset `{Funext} {X Y Z : Type}
   `{IsHSet X} (f : Y -> Z) `{IsSurjection f}
   : IsEmbedding (fun phi : Z -> X => phi o f).
 Proof.
-  intros phi g0 g1; cbn.
+  intros phi; apply istrunc_S.
+  intros g0 g1; cbn.
   rapply contr_inhabited_hprop.
   apply path_sigma_hprop, equiv_path_arrow.
   rapply conn_map_elim; intro y.
diff --git a/theories/Truncations/SeparatedTrunc.v b/theories/Truncations/SeparatedTrunc.v
index 0a27a4143e9..078ea400741 100644
--- a/theories/Truncations/SeparatedTrunc.v
+++ b/theories/Truncations/SeparatedTrunc.v
@@ -16,7 +16,7 @@ Global Instance O_eq_Tr (n : trunc_index)
 Proof.
   split; intros A A_inO.
   - intros x y; exact _.
-  - exact _.
+  - rapply istrunc_S.
 Defined.
 
 (** It follows that [Tr n <<< Tr n.+1].  However, it is easier to prove this directly than to go through separatedness. *)
diff --git a/theories/Types/Arrow.v b/theories/Types/Arrow.v
index 46e42a73ab5..a021eb97b7c 100644
--- a/theories/Types/Arrow.v
+++ b/theories/Types/Arrow.v
@@ -2,7 +2,7 @@
 (** * Theorems about Non-dependent function types *)
 
 Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable
-               Basics.Equivalences.
+               Basics.Equivalences Basics.Trunc.
 Require Import Types.Forall.
 Local Open Scope path_scope.
 
diff --git a/theories/Types/Empty.v b/theories/Types/Empty.v
index a1e02d712c6..f573317c3e3 100644
--- a/theories/Types/Empty.v
+++ b/theories/Types/Empty.v
@@ -1,7 +1,7 @@
 (* -*- mode: coq; mode: visual-line -*- *)
 (** * Theorems about the empty type *)
 
-Require Import Basics.Overture Basics.Equivalences.
+Require Import Basics.Overture Basics.Equivalences Basics.Trunc.
 Local Open Scope path_scope.
 
 (** ** Unpacking *)
@@ -15,7 +15,7 @@ Local Open Scope path_scope.
 Global Instance contr_from_Empty {_ : Funext} (A : Empty -> Type) :
   Contr (forall x:Empty, A x).
 Proof.
-  refine (Build_Contr (forall x:Empty, A x) (Empty_ind A) _).
+  refine (Build_Contr _ (Empty_ind A) _).
   intros f; apply path_forall; intros x; elim x.
 Defined.
 
@@ -35,8 +35,12 @@ Definition equiv_empty_rec `{Funext} (A : Type)
 
 (** ** Behavior with respect to truncation *)
 
-Global Instance hprop_Empty : IsHProp Empty.
-Proof. intro x. destruct x. Defined.
+Global Instance istrunc_Empty (n : trunc_index) : IsTrunc n.+1 Empty.
+Proof.
+  refine (@istrunc_leq (-1)%trunc n.+1 tt _ _).
+  apply istrunc_S.
+  intros [].
+Defined.
 
 Global Instance all_to_empty_isequiv (T : Type) (f : T -> Empty) : IsEquiv f.
 Proof.
diff --git a/theories/Types/Equiv.v b/theories/Types/Equiv.v
index e2fbe6cc708..49ef24dda37 100644
--- a/theories/Types/Equiv.v
+++ b/theories/Types/Equiv.v
@@ -123,7 +123,9 @@ Section AssumeFunext.
   Global Instance istrunc_equiv {n : trunc_index} {A B : Type} `{IsTrunc n.+1 B}
   : IsTrunc n.+1 (A <~> B).
   Proof.
-    simpl. intros e1 e2.
+    simpl.
+    apply istrunc_S.
+    intros e1 e2.
     apply (istrunc_equiv_istrunc _ (equiv_path_equiv e1 e2)).
   Defined.
 
@@ -131,7 +133,7 @@ Section AssumeFunext.
   Global Instance contr_equiv_contr_contr {A B : Type} `{Contr A} `{Contr B}
   : Contr (A <~> B).
   Proof.
-    exists equiv_contr_contr.
+    apply (Build_Contr _ equiv_contr_contr).
     intros e. apply path_equiv, path_forall. intros ?; apply contr.
   Defined.
 
@@ -139,7 +141,7 @@ Section AssumeFunext.
   Global Instance contr_aut_hprop A `{IsHProp A}
   : Contr (A <~> A).
   Proof.
-    exists 1%equiv.
+    apply (Build_Contr _ 1%equiv).
     intros e; apply path_equiv, path_forall. intros ?; apply path_ishprop.
   Defined.
 
diff --git a/theories/Types/Forall.v b/theories/Types/Forall.v
index 0429978eea5..22f65cc5094 100644
--- a/theories/Types/Forall.v
+++ b/theories/Types/Forall.v
@@ -4,6 +4,8 @@
 Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids
                Basics.Tactics Basics.Trunc Basics.Contractible.
 
+Require Export Basics.Trunc (istrunc_forall).
+
 Local Open Scope path_scope.
 
 
@@ -337,25 +339,7 @@ Global Arguments equiv_path_forall11 {A B}%type_scope {P} (f g)%function_scope.
 
 Global Arguments path_forall11 {A B}%type_scope {P} (f g)%function_scope _.
 
-(** ** Truncatedness: any dependent product of n-types is an n-type *)
-
-Global Instance contr_forall `{P : A -> Type} `{forall a, Contr (P a)}
-  : Contr (forall a, P a) | 100.
-Proof.
-  exists (fun a => center (P a)).
-  intro f.  apply path_forall.  intro a.  apply contr.
-Defined.
-
-Global Instance istrunc_forall `{P : A -> Type} `{forall a, IsTrunc n (P a)}
-  : IsTrunc n (forall a, P a) | 100.
-Proof.
-  generalize dependent P.
-  simple_induction n n IH; simpl; intros P ?.
-  (* case [n = -2], i.e. contractibility *)
-  - exact _.
-  (* case n = n'.+1 *)
-  - intros f g; apply (istrunc_isequiv_istrunc@{u1 u1} _ (apD10@{_ _ u1} ^-1)).
-Defined.
+(** ** Truncatedness: any dependent product of n-types is an n-type: see [contr_forall] and [istrunc_forall] in Basics.Trunc. *)
 
 (** ** Contractibility: A product over a contractible type is equivalent to the fiber over the center. *)
 
diff --git a/theories/Types/IWType.v b/theories/Types/IWType.v
index 81db2c555ba..3ed58532d30 100644
--- a/theories/Types/IWType.v
+++ b/theories/Types/IWType.v
@@ -416,6 +416,7 @@ Proof.
   induction n as [|n IHn].
   1: apply ishprop_iwtype.
   intros I A B i j h l.
+  apply istrunc_S.
   intros x y.
   refine (istrunc_equiv_istrunc _
     (equiv_path_iwtype I A B i j l x y) (n := n.+1)).
diff --git a/theories/Types/Prod.v b/theories/Types/Prod.v
index c72f5df3a6b..fed28642927 100644
--- a/theories/Types/Prod.v
+++ b/theories/Types/Prod.v
@@ -363,14 +363,15 @@ Global Instance istrunc_prod `{IsTrunc n A} `{IsTrunc n B} : IsTrunc n (A * B) |
 Proof.
   generalize dependent B; generalize dependent A.
   simple_induction n n IH; simpl; (intros A ? B ?).
-  { exists (center A, center B).
+  { apply (Build_Contr _ (center A, center B)).
     intros z; apply path_prod; apply contr. }
+  apply istrunc_S.
   intros x y.
   exact (istrunc_equiv_istrunc _ (equiv_path_prod x y)).
 Defined.
 
 Global Instance contr_prod `{CA : Contr A} `{CB : Contr B} : Contr (A * B) | 100
-  := @istrunc_prod (-2) A CA B CB.
+  := istrunc_prod.
 
 (** ** Decidability *)
 
diff --git a/theories/Types/Sigma.v b/theories/Types/Sigma.v
index 95e8c938783..12a2030d7c8 100644
--- a/theories/Types/Sigma.v
+++ b/theories/Types/Sigma.v
@@ -610,9 +610,10 @@ Global Instance istrunc_sigma `{P : A -> Type}
 Proof.
   generalize dependent A.
   induction n; simpl; intros A P ac Pc.
-  { exists (center A; center (P (center A))).
+  { apply (Build_Contr _ (center A; center (P (center A)))).
     intros [a ?].
     refine (path_sigma' P (contr a) (path_contr _ _)). }
+  apply istrunc_S.
   intros u v.
   refine (istrunc_isequiv_istrunc _ (path_sigma_uncurried P u v)).
 Defined.
diff --git a/theories/Types/Sum.v b/theories/Types/Sum.v
index e6315d6e59a..2af0186a843 100644
--- a/theories/Types/Sum.v
+++ b/theories/Types/Sum.v
@@ -917,12 +917,11 @@ Global Instance istrunc_sum n' (n := n'.+2)
          `{IsTrunc n A, IsTrunc n B}
 : IsTrunc n (A + B) | 100.
 Proof.
+  apply istrunc_S.
   intros a b.
   eapply istrunc_equiv_istrunc;
     [ exact (equiv_path_sum _ _) | ].
-  destruct a, b; simpl in *;
-  try typeclasses eauto;
-  intros [].
+  destruct a, b; exact _.
 Defined.
 
 Global Instance ishset_sum `{HA : IsHSet A, HB : IsHSet B} : IsHSet (A + B) | 100
diff --git a/theories/Types/Unit.v b/theories/Types/Unit.v
index 124809108aa..739db0772e7 100644
--- a/theories/Types/Unit.v
+++ b/theories/Types/Unit.v
@@ -4,6 +4,8 @@
 Require Import Basics.Overture Basics.Equivalences.
 Local Open Scope path_scope.
 
+Local Set Universe Minimization ToSet.
+
 Generalizable Variables A.
 
 (** ** Eta conversion *)
@@ -101,10 +103,7 @@ Definition equiv_unit_coind `{Funext} (A : Type)
 (** ** Truncation *)
 
 (* The Unit type is contractible *)
-Global Instance contr_unit : Contr Unit | 0 := {|
-  center := tt;
-  contr := fun t : Unit => match t with tt => 1 end
-|}.
+Global Instance contr_unit : Contr Unit | 0 := Build_Contr _ tt (fun t : Unit => match t with tt => 1 end).
 
 (** ** Equivalences *)
 
@@ -116,5 +115,5 @@ Definition equiv_contr_unit `{Contr A} : A <~> Unit
 Global Instance contr_equiv_unit (A : Type) (f : A <~> Unit) : Contr A | 10000
   := contr_equiv' Unit f^-1%equiv.
 
-(** The constant map to [Unit].  We define this so we can get rid of an unneeded universe variable that Coq generates when this is not annotated. If we ever turn on [Universe Minimization ToSet], then we could get rid of this and remove some imports of this file. *)
-Definition const_tt@{u} (A : Type@{u}) := @const@{Set u} A Unit tt.
+(** The constant map to [Unit].  We define this so we can get rid of an unneeded universe variable that Coq generates when [const tt] is used in a context that doesn't have [Universe Minimization ToSet] as this file does. If we ever set that globally, then we could get rid of this and remove some imports of this file. *)
+Definition const_tt (A : Type) := @const A Unit tt.
diff --git a/theories/Types/Universe.v b/theories/Types/Universe.v
index 854d145b318..69e1c36a27b 100644
--- a/theories/Types/Universe.v
+++ b/theories/Types/Universe.v
@@ -498,7 +498,7 @@ Definition equiv_induction_inv_comp {U : Type} (P : forall V, V <~> U -> Type)
 Global Instance contr_basedequiv@{u +} {X : Type@{u}}
 : Contr {Y : Type@{u} & X <~> Y}.
 Proof.
-  exists (X; equiv_idmap).
+  apply (Build_Contr _ (X; equiv_idmap)).
   intros [Y f]; revert Y f.
   exact (equiv_induction _ idpath).
 Defined.
diff --git a/theories/Types/WType.v b/theories/Types/WType.v
index 04fc78140c9..3c9b96c7a0a 100644
--- a/theories/Types/WType.v
+++ b/theories/Types/WType.v
@@ -44,6 +44,7 @@ Global Instance istrunc_wtype `{Funext}
   {A B} {n : trunc_index} `{IsTrunc n.+1 A}
 : IsTrunc n.+1 (W A B) | 100.
 Proof.
+  apply istrunc_S.
   intros z; induction z as [a w].
   intro y; destruct y as [a0 w0].
   nrefine (istrunc_equiv_istrunc _ (equiv_path_wtype' _ _)).