Convert more files to Inductive IsTrunc

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.
 

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.
 

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

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.
 

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.

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.

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

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.

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)

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.

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

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.

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

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 *)
@@ -113,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.