Merge pull request #1806 from jdchristensen/inductive-istrunc

Make IsTrunc an inductive type

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

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.

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

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.

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

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.

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

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.
 

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.

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.

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

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.