Merge pull request HoTT#2216 from jdchristensen/minor-misc-fixes

Misc fixes to comments, spacing and some proofs

theories/Algebra/Groups/FreeProduct.v

@@ -731,7 +731,7 @@ Definition freeproduct_ind_homotopy {G H K : Group}
 Proof.
   rapply (freeproduct_ind_hprop _ l r).
   intros x y; nrapply grp_homo_op_agree. (* Slow, ~0.2s. *)
-Time Defined. (* Slow, ~0.15s. *)
+Defined. (* Slow, ~0.15s. *)
 
 Definition freeproduct_rec_beta_inl {G H K : Group}
   (f : G $-> K) (g : H $-> K)

theories/Algebra/Groups/Group.v

@@ -280,6 +280,7 @@ Defined.
 (** Group homomorphisms preserve inverses. *)
 Definition grp_homo_inv {G H} (f : GroupHomomorphism G H)
   : forall x, f x^ = (f x)^.
+(* This can also be proved using [:= preserves_inverse.] from Classes/theory/groups.v.  That uses [rewrite] and is marked [Qed]. *)
 Proof.
   intro x.
   apply (inverse_unique (f x)).

theories/Homotopy/HSpace/Core.v

@@ -139,7 +139,7 @@ Definition phomotopy_from_homotopy `{Funext} {A B : pType}
   (m : forall (a : A), (point A) = (point A) -> a = a)
   (q :  m pt == idmap) {f g : B ->* A} (K : f == g)
   : f ==* g
-  := (phomotopy_from_path_arrow m q (path_forall _ _ K)).
+  := phomotopy_from_path_arrow m q (path_forall _ _ K).
 
 (** We specialize to H-spaces. *)
 Definition hspace_phomotopy_from_homotopy `{Funext} {A B : pType}

theories/Modalities/Modality.v

@@ -513,7 +513,7 @@ Section ModalFact.
   : IsConnMap O (factor1 (image f))
     := inclass1 (image f).
 
-  Global Instance inO_map_factor1_image {A B : Type} (f : A -> B)
+  Global Instance inO_map_factor2_image {A B : Type} (f : A -> B)
   : MapIn O (factor2 (image f))
     := inclass2 (image f).
 

theories/Pointed/pTrunc.v

@@ -159,7 +159,7 @@ Defined.
 
 (** ** Truncatedness of [pForall] and [pMap] *)
 
-(** Buchholtz-van Doorn-Rijke, Theorem 4.2:  Let [j >= -1] and [n >= -2].  When [X] is [j]-connected and [Y] is a pointed family of [j+k+1]-truncated types, the type of pointed sections is [n]-truncated.  We formalize it with [j] replaced with a trunc index [m], and so there is a shift compared to the informal statement. This version also allows [n] to be one smaller than BvDR allow. *)
+(** Buchholtz-van Doorn-Rijke, Theorem 4.2:  Let [j >= -1] and [n >= -2].  When [X] is [j]-connected and [Y] is a pointed family of [j+n+1]-truncated types, the type of pointed sections is [n]-truncated.  We formalize it with [j] replaced with a trunc index [m.+1] to enforce [j >= -1]. This version also allows [n] to be one smaller than BvDR allow. *)
 Definition istrunc_pforall `{Univalence} {m n : trunc_index}
   (X : pType@{u}) {iscX : IsConnected m.+1 X}
   (Y : pFam@{u v} X) {istY : forall x, IsTrunc (n +2+ m) (Y x)}
@@ -175,7 +175,7 @@ Definition istrunc_pmap `{Univalence} {m n : trunc_index} (X Y : pType)
   : IsTrunc n (X ->* Y)
   := istrunc_pforall X (pfam_const Y).
 
-(** We can give a different proof of the [n = -1] case (with the conclusion upgraded to contractibility).  This proof works for any reflective subuniverse and avoids univalence.  Is it possible to generalize this to dependent functions while still avoiding univalence and/or keeping [O] a general RSU or modality?  Can [istrunc_pmap] be proven without univalence?  What about [istrunc_pforall]?  If the [n = -2] or [n = -1] cases can be proven without univalence, the rest can be done inductively without univalence. *)
+(** We can give a different proof of the [n = -1] case (with the conclusion upgraded to contractibility).  This proof works with [Tr (m.+1)] replaced with any reflective subuniverse [O] and doesn't require univalence.  Is it possible to generalize this to dependent functions while still avoiding univalence and/or keeping [O] a general RSU or modality?  Can [istrunc_pmap] be proven without univalence?  What about [istrunc_pforall]?  If the [n = -2] or [n = -1] cases can be proven without univalence, the rest can be done inductively without univalence. *)
 Definition contr_pmap_isconnected_inO `{Funext} (O : ReflectiveSubuniverse)
   (X : pType) `{IsConnected O X} (Y : pType) `{In O Y}
   : Contr (X ->* Y).

theories/Spaces/Nat/Binomial.v

@@ -96,9 +96,8 @@ Proof.
   (* The case when [m = n]. *)
   { rewrite nat_sub_cancel.
     rewrite nat_mul_one_r.
-    rewrite nat_div_cancel.
-    1: nrapply nat_choose_diag.
-    exact _. }
+    rhs rapply nat_div_cancel.
+    nrapply nat_choose_diag. }
   (* The case with [n.+1] and [m.+1] with [m < n] and an induction hypothesis. *)
   intros m H IHn.
   rewrite_refl nat_choose_succ.

theories/Spaces/Nat/Core.v

@@ -1580,7 +1580,7 @@ Defined.
 (** ** An induction principle for two variables with a constraint. *)
 Definition nat_double_ind_leq@{u} (P : nat -> nat -> Type@{u})
   (Hn0 : forall n, P n 0)
-  (Hnn : forall n, P n n)
+  (Hnn : forall n, P n.+1 n.+1)
   (IH : forall n m, m < n -> (forall m', m' <= n -> P n m') -> P n.+1 m.+1)
   : forall n m, m <= n -> P n m.
 Proof.

theories/Truncations/Connectedness.v

@@ -48,7 +48,7 @@ Proof.
     (* m = S m' *)
   - 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. *)
+    (* Magically infers: paths in extensions = extensions into paths, which by induction is [m']-truncated. *)
 Defined.
 
 (** ** Connectedness of path spaces *)
@@ -91,9 +91,9 @@ Definition conn_point_elim `{Univalence} (n : trunc_index) {A : pType@{u}} `{IsC
            (P : A -> Type@{u}) `{forall a, IsTrunc n (P a)} (p0 : P (point A))
   : forall a, P a.
 Proof.
-  (** This follows from [conn_point_incl] and [conn_map_elim], but we give a direct proof. *)
+  (* This follows from [conn_point_incl] and [conn_map_elim], but we give a direct proof. *)
   intro a.
-  (** Since [A] is [n+1]-connected, [a0 = a] is [n]-connected, which means that [Tr n (a0 = a)] has an element. *)
+  (* Since [A] is [n+1]-connected, [a0 = a] is [n]-connected, which means that [Tr n (a0 = a)] has an element. *)
   pose proof (p := center (Tr n ((point A) = a))).
   strip_truncations.
   exact (p # p0).