Merge pull request #2319 from jdchristensen/misc

Miscellaneous small changes

Author: jdchristensen

theories/Basics/Overture.v

@@ -396,7 +396,7 @@ Arguments transport {A}%_type_scope P%_function_scope {x y} p%_path_scope u : si
 Notation "p # u" := (transport _ p u) (only parsing) : path_scope.
 
 (** The first time [rewrite] is used in each direction, it creates transport lemmas called [internal_paths_rew] and [internal_paths_rew_r].  See ../Tactics.v for how these compare to [transport].  We use [rewrite] here to trigger the creation of these lemmas.  This ensures that they are defined outside of sections, so they are not unnecessarily polymorphic.  The lemmas below are not used in the library. *)
-(** TODO: If Coq PR#18299 is merged (possibly in Coq 8.20), then we can instead register wrappers for [transport] to be used for rewriting.  See the comment by Dan Christensen in that PR for how to do this.  Then the tactics [internal_paths_rew_to_transport] and [rewrite_to_transport] can be removed from ../Tactics.v. *)
+(** TODO: Since Coq 8.20 has PR#18299, once that is our minimum version we can instead register wrappers for [transport] to be used for rewriting.  See the comment by Dan Christensen in that PR for how to do this.  Then the tactics [internal_paths_rew_to_transport] and [rewrite_to_transport] can be removed from ../Tactics.v. *)
 Local Lemma define_internal_paths_rew A x y P (u : P x) (H : x = y :> A) : P y.
 Proof. rewrite <- H. exact u. Defined.
 

theories/Basics/Settings.v

@@ -2,8 +2,6 @@
 
 (** This file contains all the tweaks and settings we make to Coq. *)
 
-(** ** Warnings *)
-
 (** ** Plugins *)
 
 (** Load the Ltac plugin. This is the tactic language we use for proofs. *)

theories/Basics/Trunc.v

@@ -56,13 +56,13 @@ Definition nat_to_trunc_index@{} (n : nat) : trunc_index
 
 Coercion nat_to_trunc_index : nat >-> trunc_index.
 
-Definition trunc_index_inc'_0n (n : nat)
+Definition trunc_index_inc'_0n@{} (n : nat)
   : trunc_index_inc' 0%nat n = n.
 Proof.
-  induction n as [|n p].
+  simple_induction n n IHn.
   1: reflexivity.
   refine (trunc_index_inc'_succ _ _ @ _).
-  exact (ap _ p).
+  exact (ap _ IHn).
 Defined.
 
 Definition int_to_trunc_index@{} (v : Decimal.int) : option trunc_index

theories/Categories/Category/Morphisms.v

@@ -1,6 +1,6 @@
 (** * Definitions and theorems about {iso,epi,mono,}morphisms in a precategory *)
 Require Import Category.Core Functor.Core.
-Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.
+Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Basics.Equivalences Types.Sigma.
 
 Set Universe Polymorphism.
 Set Implicit Arguments.
@@ -44,9 +44,6 @@ Local Infix "<~=~>" := Isomorphic : category_scope.
 (** ** Theorems about isomorphisms *)
 Section iso_contr.
   Variable C : PreCategory.
-
-
-
   Variables s d : C.
 
   Local Notation IsIsomorphism_sig_T m :=

theories/Homotopy/HSpace/Moduli.v

@@ -74,30 +74,30 @@ Proof.
   apply concat_p1.
 Defined.
 
-(** Our next goal is to see that when [A] is a left-invertible H-space, then the fibration [ev A] is trivial. *)
+(** Our next goal is to see that when [A] is a left-invertible H-space, then the fibration [ev A] is trivial. We begin with two results that allow the domain to be a general pointed type [B]. We'll later just need the case when [B] is [A]. *)
 
-(** This lemma says that the family [fun a => A ->* [A,a]] is trivial. *)
-Lemma equiv_pmap_hspace `{Funext} {A : pType}
+(** This lemma says that the family [fun a => B ->* [A,a]] is trivial. *)
+Lemma equiv_pmap_hspace `{Funext} {A B : pType}
   (a : A) `{IsHSpace A} `{!IsEquiv (hspace_op a)}
-  : (A ->* A) <~> (A ->* [A,a]).
+  : (B ->* A) <~> (B ->* [A,a]).
 Proof.
   napply pequiv_pequiv_postcompose.
   rapply pequiv_hspace_left_op.
 Defined.
 
-(** The lemma gives us an equivalence on the total spaces (domains) of [ev A] and [psnd] (the projection out of the displayed product). *)
-Proposition equiv_map_pmap_hspace `{Funext} {A : pType}
+(** The next result is a consequence of the previous lemma. *)
+Proposition equiv_map_pmap_hspace `{Funext} {A B : pType}
   `{IsHSpace A} `{forall a:A, IsEquiv (a *.)}
-  : (A ->* A) * A <~> (A -> A).
+  : (B ->* A) * A <~> (B -> A).
 Proof.
-  transitivity {a : A  & {f : A -> A & f pt = a}}.
+  transitivity {a : A  & {f : B -> A & f pt = a}}.
   2: exact (equiv_sigma_contr _ oE (equiv_sigma_symm _)^-1%equiv).
   refine (_ oE (equiv_sigma_prod0 _ _)^-1%equiv oE equiv_prod_symm _ _).
   apply equiv_functor_sigma_id; intro a.
-  exact ((issig_pmap A [A,a])^-1%equiv oE equiv_pmap_hspace a).
+  exact ((issig_pmap B [A,a])^-1%equiv oE equiv_pmap_hspace a).
 Defined.
 
-(** The above is a pointed equivalence. *)
+(** The equivalence [equiv_map_pmap_hspace] is pointed when [B] is [A]. (Note that [selfmaps A] is pointed at [idmap].) This is a pointed equivalence between the domains of [psnd : (A ->* A) * A ->* A] and [ev A : selfmaps A -> A], respectively. *)
 Proposition pequiv_map_pmap_hspace `{Funext} {A : pType}
   `{IsHSpace A} `{forall a:A, IsEquiv (a *.)}
   : [(A ->* A) * A, (pmap_idmap, pt)] <~>* selfmaps A.

theories/Homotopy/Join/Core.v

@@ -30,7 +30,7 @@ Section Join.
 
   Definition Join_ind {A B : Type} (P : Join A B -> Type)
     (P_A : forall a, P (joinl a)) (P_B : forall b, P (joinr b))
-    (P_g : forall a b, transport P (jglue a b) (P_A a) = (P_B b))
+    (P_g : forall a b, transport P (jglue a b) (P_A a) = P_B b)
     : forall (x : Join A B), P x.
   Proof.
     apply (Pushout_ind P P_A P_B).
@@ -145,7 +145,7 @@ Arguments joinr {A B}%_type_scope _ , A [B] _.
 
 (** ** Zigzags in joins *)
 
-(** These paths are very common, so we give them names. *)
+(** These paths are very common, so we give them names and prove a few results about them. *)
 Definition zigzag {A B : Type} (a a' : A) (b : B)
   : joinl a = joinl a'
   := jglue a b @ (jglue a' b)^.
@@ -154,6 +154,14 @@ Definition zagzig {A B : Type} (a : A) (b b' : B)
   : joinr b = joinr b'
   := (jglue a b)^ @ jglue a b'.
 
+Definition zigzag_zigzag {A B : Type} (a a' : A) (b : B)
+  : zigzag a a' b @ zigzag a' a b = 1
+  := concat_pp_p _ _ _ @ (1 @@ concat_V_pp _ _) @ concat_pV _.
+
+Definition zigzag_inv {A B : Type} (a a' : A) (b : B)
+  : (zigzag a a' b)^ = zigzag a' a b
+  := inv_pp _ _ @ (inv_V _ @@ 1).
+
 (** And we give a beta rule for zigzags. *)
 Definition Join_rec_beta_zigzag {A B P : Type} (P_A : A -> P)
   (P_B : B -> P) (P_g : forall a b, P_A a = P_B b) a a' b

theories/Spaces/Nat/Core.v

@@ -135,7 +135,7 @@ Scheme leq_ind := Induction for leq Sort Type.
 Scheme leq_rect := Induction for leq Sort Type.
 Scheme leq_rec := Induction for leq Sort Type.
 
-Notation "n <= m" := (leq n m) : nat_scope.
+Infix "<=" := leq : nat_scope.
 
 Existing Class leq.
 Existing Instances leq_refl leq_succ_r.
@@ -144,25 +144,27 @@ Existing Instances leq_refl leq_succ_r.
 
 (** We define the less-than relation [lt] in terms of [leq] *)
 Definition lt n m : Type0 := leq (S n) m.
+Infix "<" := lt : nat_scope.
 
 (** We declare it as an existing class so typeclass search is performed on its goals. *)
 Existing Class lt.
 #[export] Hint Unfold lt : typeclass_instances.
-Infix "<" := lt : nat_scope.
 
 (** *** Greater than or equal To [>=] *)
 
 Definition geq n m := leq m n.
+Infix ">=" := geq : nat_scope.
+
 Existing Class geq.
 #[export] Hint Unfold geq : typeclass_instances.
-Infix ">=" := geq : nat_scope.
 
 (*** Greater Than [>] *)
 
 Definition gt n m := lt m n.
+Infix ">" := gt : nat_scope.
+
 Existing Class gt.
 #[export] Hint Unfold gt : typeclass_instances.
-Infix ">" := gt : nat_scope.
 
 (** *** Combined comparison predicates *)
 

theories/Types/Equiv.v

@@ -222,7 +222,7 @@ Defined.
 (** A version that shows that the underlying functions are equal. *)
 Definition transport_equiv' {A : Type} {B C : A -> Type}
   {x1 x2 : A} (p : x1 = x2) (f : B x1 <~> C x1)
-  : transport (fun x => B x <~> C x) p f = (equiv_transport _ p) oE f oE (equiv_transport _ p^) :> (B x2 -> C x2).
+  : transport (fun x => B x <~> C x) p f = (transport _ p) o f o (transport _ p^) :> (B x2 -> C x2).
 Proof.
   destruct p; auto.
 Defined.
@@ -235,3 +235,49 @@ Proof.
   apply path_equiv.
   destruct p; auto.
 Defined.
+
+(** The special case when the codomain type is constant. *)
+Definition transport_equiv_toconst {A : Type} {B : A -> Type} {C : Type}
+  {x1 x2 : A} (p : x1 = x2) (f : B x1 <~> C) (y : B x2)
+  : (transport (fun x => B x <~> C) p f) y = f (p^ # y).
+Proof.
+  by destruct p.
+Defined.
+
+Definition transport_equiv_toconst' {A : Type} {B : A -> Type} {C : Type}
+  {x1 x2 : A} (p : x1 = x2) (f : B x1 <~> C)
+  : transport (fun x => B x <~> C) p f = f o (transport _ p^) :> (B x2 -> C).
+Proof.
+  by destruct p.
+Defined.
+
+Definition transport_equiv_toconst'' `{Funext} {A : Type} {B : A -> Type} {C : Type}
+  {x1 x2 : A} (p : x1 = x2) (f : B x1 <~> C)
+  : transport (fun x => B x <~> C) p f = f oE (equiv_transport _ p^).
+Proof.
+  apply path_equiv.
+  by destruct p.
+Defined.
+
+(** The special case when the domain type is constant. *)
+Definition transport_equiv_fromconst {A B : Type} {C : A -> Type}
+  {x1 x2 : A} (p : x1 = x2) (f : B <~> C x1) (y : B)
+  : (transport (fun x => B <~> C x) p f) y = p # (f y).
+Proof.
+  by destruct p.
+Defined.
+
+Definition transport_equiv_fromconst' {A B : Type} {C : A -> Type}
+  {x1 x2 : A} (p : x1 = x2) (f : B <~> C x1)
+  : (transport (fun x => B <~> C x) p f) = transport C p o f :> (B -> C x2).
+Proof.
+  by destruct p.
+Defined.
+
+Definition transport_equiv_fromconst'' `{Funext} {A B : Type} {C : A -> Type}
+  {x1 x2 : A} (p : x1 = x2) (f : B <~> C x1)
+  : (transport (fun x => B <~> C x) p f) = equiv_transport C p oE f.
+Proof.
+  apply path_equiv.
+  by destruct p.
+Defined.

theories/Universes/HProp.v

@@ -128,7 +128,7 @@ Proof.
   - exact (fun _ => p).
 Defined.
 
-(** If an hprop is not inhabited, then it is equivalent to [Empty]. Note that we'd don't need the assumption that the type is an hprop here. *)
+(** If an hprop is not inhabited, then it is equivalent to [Empty]. Note that we don't need the assumption that the type is an hprop here. *)
 Definition if_not_hprop_then_equiv_Empty (hprop : Type) : ~hprop -> hprop <~> Empty
   := equiv_to_empty.
 

theories/WildCat/Category.v

@@ -3,7 +3,7 @@ Require Import WildCat.Core WildCat.NatTrans WildCat.FunctorCat.
 
 (** * Category of categories *)
 
-(** TODO: make into a bicategory *)
+(** TODO: make into a bicategory; define equivalences *)
 
 (** ** Definition *)