Merge pull request #2198 from jdchristensen/misc-cleanups

Misc cleanups to PathGroupoids, Equiv, HProp and BoundedSearch

theories/Basics/PathGroupoids.v

@@ -16,7 +16,7 @@ Local Open Scope path_scope.
 
    Theorems about concatenation of paths are called [concat_XXX] where [XXX] tells us what is on the left-hand side of the equation. You have to guess the right-hand side. We use the following symbols in [XXX]:
 
-   - [1] means the identity path
+   - [1] means the identity path, or sometimes the identity function
    - [p] means 'the path'
    - [V] means 'the inverse path'
    - [A] means '[ap]'
@@ -27,12 +27,12 @@ Local Open Scope path_scope.
 
    Associativity is indicated with an underscore. Here are some examples of how the name gives hints about the left-hand side of the equation.
 
-   - [concat_1p] means [1 * p]
-   - [concat_Vp] means [p^ * p]
-   - [concat_p_pp] means [p * (q * r)]
-   - [concat_pp_p] means [(p * q) * r]
-   - [concat_V_pp] means [p^ * (p * q)]
-   - [concat_pV_p] means [(q * p^) * p] or [(p * p^) * q], but probably the former because for the latter you could just use [concat_pV].
+   - [concat_1p] means [1 @ p]
+   - [concat_Vp] means [p^ @ p]
+   - [concat_p_pp] means [p @ (q @ r)]
+   - [concat_pp_p] means [(p @ q) @ r]
+   - [concat_V_pp] means [p^ @ (p @ q)]
+   - [concat_pV_p] means [(q @ p^) @ p] or [(p @ p^) @ q], but probably the former because for the latter you could just use [concat_pV].
 
    Laws about inverse of something are of the form [inv_XXX], and those about [ap] are of the form [ap_XXX], and so on. For example:
 
@@ -55,11 +55,9 @@ Local Open Scope path_scope.
      because we move to the right-hand side, and we are moving the left
      argument of concat.
 
-   - [moveR_1M] means that we transform [p = q] (rather than [p = 1 @ q]) to [p * q^ = 1].
+   - [moveR_1M] means that we transform [p = q] (rather than [p = 1 @ q]) to [p @ q^ = 1].
 
    There are also cancellation laws called [cancelR] and [cancelL], which are inverse to the 2-dimensional 'whiskering' operations [whiskerR] and [whiskerL].
-
-   We may now proceed with the groupoid structure proper.
 *)
 
 (** ** The 1-dimensional groupoid structure. *)

theories/BoundedSearch.v

@@ -5,8 +5,7 @@ Require Import HoTT.Spaces.Nat.Core.
 Section bounded_search.
 
   Context (P : nat -> Type)
-          (P_dec : forall n, Decidable (P n))
-          (P_inhab : hexists (fun n => P n)).
+          (P_dec : forall n, Decidable (P n)).
 
   (** We open type_scope again after nat_scope in order to use the product type notation. *)
   Local Open Scope nat_scope.
@@ -80,15 +79,17 @@ Section bounded_search.
     - destruct (none n (leq_refl n) Pn).
   Defined.
 
-  Local Definition prop_n_to_min_n : min_n_Type.
+  Local Definition prop_n_to_min_n (P_inhab : hexists (fun n => P n))
+    : min_n_Type.
   Proof.
     refine (Trunc_rec _ P_inhab).
     intros [n Pn]. exact (n_to_min_n n Pn).
   Defined.
 
-  Definition minimal_n : { n : nat & P n }.
+  Definition minimal_n (P_inhab : hexists (fun n => P n))
+    : { n : nat & P n }.
   Proof.
-    destruct prop_n_to_min_n as [n pl]. destruct pl as [p _].
+    destruct (prop_n_to_min_n P_inhab) as [n pl]. destruct pl as [p _].
     exact (n; fst merely_inhabited_iff_inhabited_stable p).
   Defined.
 

theories/Types/Equiv.v

@@ -144,7 +144,6 @@ Section AssumeFunext.
   Global Instance istrunc_equiv {n : trunc_index} {A B : Type} `{IsTrunc n.+1 B}
     : IsTrunc n.+1 (A <~> B).
   Proof.
-    simpl.
     apply istrunc_S.
     intros e1 e2.
     apply (istrunc_equiv_istrunc _ (equiv_path_equiv e1 e2)).

theories/Universes/HProp.v

@@ -152,8 +152,8 @@ Defined.
 (** When [A] is an hprop, so is [Stable A] (by [ishprop_stable_hprop]), so [Stable A * IsHProp A] is an hprop for any [A]. *)
 Global Instance ishprop_stable_ishprop `{Funext} (A : Type) : IsHProp (Stable A * IsHProp A).
 Proof.
-  apply hprop_allpath; intros [st1 hp1] [st2 hp2].
-  apply path_ishprop.
+  apply istrunc_inhabited_istrunc; intros [stable ishprop].
+  exact _.
 Defined.
 
 (** Under function extensionality, if [A] is a stable type, then [~~A] is the propositional truncation of [A]. Here, for dependency reasons, we don't give the equivalence to [Tr (-1) A], but just show that the recursion principle holds. See Metatheory/ImpredicativeTruncation.v for a generalization to all types, and Modalities/Notnot.v for a description of the universal property of [~~A] when [A] is not assumed to be stable. *)