Merge pull request #1768 from jdchristensen/join-assoc

Associativity of Join, and lots more

theories/Basics/Equivalences.v

@@ -82,40 +82,6 @@ Ltac change_apply_equiv_compose :=
     change ((f oE g) x) with (f (g x))
   end.
 
-(** Anything homotopic to an equivalence is an equivalence. *)
-Section IsEquivHomotopic.
-
-  Context {A B : Type} (f : A -> B) {g : A -> B}.
-  Context `{IsEquiv A B f}.
-  Hypothesis h : f == g.
-
-  Let retr := (fun b:B => (h (f^-1 b))^ @ eisretr f b).
-  Let sect := (fun a:A => (ap f^-1 (h a))^ @ eissect f a).
-
-  (* We prove the triangle identity with rewrite tactics.  Since we lose control over the proof term that way, we make the result opaque with "Qed". *)
-  Local Definition adj (a : A) : retr (g a) = ap g (sect a).
-  Proof.
-    unfold sect, retr.
-    rewrite ap_pp. apply moveR_Vp.
-    rewrite concat_p_pp, <- concat_Ap, concat_pp_p, <- concat_Ap.
-    rewrite ap_V; apply moveL_Vp.
-    rewrite <- ap_compose; rewrite (concat_A1p (eisretr f) (h a)).
-    apply whiskerR, eisadj.
-  Qed.
-
-  (* This should not be an instance; it can cause the unifier to spin forever searching for functions to be homotopic to. *)
-  Definition isequiv_homotopic : IsEquiv g
-    := Build_IsEquiv _ _ g (f ^-1) retr sect adj.
-
-  Definition equiv_homotopic : A <~> B
-    := Build_Equiv _ _ g isequiv_homotopic.
-
-End IsEquivHomotopic.
-
-Definition isequiv_homotopic' {A B : Type} (f : A <~> B) {g : A -> B} (h : f == g)
-  : IsEquiv g
-  := isequiv_homotopic f h.
-
 (** Transporting is an equivalence. *)
 Section EquivTransport.
 
@@ -169,6 +135,38 @@ End Adjointify.
 Arguments isequiv_adjointify {A B}%type_scope (f g)%function_scope isretr issect.
 Arguments equiv_adjointify {A B}%type_scope (f g)%function_scope isretr issect.
 
+(** Anything homotopic to an equivalence is an equivalence. This should not be an instance; it can cause the unifier to spin forever searching for functions to be homotopic to. *)
+Definition isequiv_homotopic {A B : Type} (f : A -> B) {g : A -> B}
+  `{IsEquiv A B f} (h : f == g)
+  : IsEquiv g.
+Proof.
+  snrapply isequiv_adjointify.
+  - exact f^-1.
+  - intro b.  exact ((h _)^ @ eisretr f b).
+  - intro a.  exact (ap f^-1 (h a)^ @ eissect f a).
+Defined.
+
+Definition isequiv_homotopic' {A B : Type} (f : A <~> B) {g : A -> B} (h : f == g)
+  : IsEquiv g
+  := isequiv_homotopic f h.
+
+Definition equiv_homotopic {A B : Type} (f : A -> B) {g : A -> B}
+  `{IsEquiv A B f} (h : f == g)
+  : A <~> B
+  := Build_Equiv _ _ g (isequiv_homotopic f h).
+
+(** If [e] is an equivalence, [f] is homotopic to [e], and [g] is homotopic to [e^-1], then there is an equivalence whose underlying map is [f] and whose inverse is [g], definitionally. *)
+Definition equiv_homotopic_inverse {A B} (e : A <~> B)
+  {f : A -> B} {g : B -> A} (h : f == e) (k : g == e^-1)
+  : A <~> B.
+Proof.
+  snrapply equiv_adjointify.
+  - exact f.
+  - exact g.
+  - intro a.  exact (ap f (k a) @ h _ @ eisretr e a).
+  - intro b.  exact (ap g (h b) @ k _ @ eissect e b).
+Defined.
+
 (** An involution is an endomap that is its own inverse. *)
 Definition isequiv_involution {X : Type} (f : X -> X) (isinvol : f o f == idmap)
 : IsEquiv f

theories/Basics/PathGroupoids.v

@@ -78,6 +78,15 @@ Definition concat_1p {A : Type} {x y : A} (p : x = y) :
   :=
   match p with idpath => 1 end.
 
+(** It's common to need to use both. *)
+Definition concat_p1_1p {A : Type} {x y : A} (p : x = y)
+  : p @ 1 = 1 @ p
+  := concat_p1 p @ (concat_1p p)^.
+
+Definition concat_1p_p1 {A : Type} {x y : A} (p : x = y)
+  : 1 @ p = p @ 1
+  := concat_1p p @ (concat_p1 p)^.
+
 (** Concatenation is associative. *)
 Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
   p @ (q @ r) = (p @ q) @ r :=
@@ -437,7 +446,7 @@ Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y
   (ap f q) @ (p y) = (p x) @ (ap g q)
   :=
   match q with
-    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+    | idpath => concat_1p_p1 _
   end.
 
 (* A useful variant of concat_Ap. *)
@@ -453,7 +462,7 @@ Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A}
   (ap f q) @ (p y) = (p x) @ q
   :=
   match q with
-    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+    | idpath => concat_1p_p1 _
   end.
 
 (* The corresponding variant of concat_A1p. *)
@@ -468,9 +477,19 @@ Definition concat_pA1 {A : Type} {f : A -> A} (p : forall x, x = f x) {x y : A}
   (p x) @ (ap f q) =  q @ (p y)
   :=
   match q as i in (_ = y) return (p x @ ap f i = i @ p y) with
-    | idpath => concat_p1 _ @ (concat_1p _)^
+    | idpath => concat_p1_1p _
   end.
 
+Definition apD_homotopic {A : Type} {B : A -> Type} {f g : forall x, B x}
+  (p : forall x, f x = g x) {x y : A} (q : x = y)
+  : apD f q = ap (transport B q) (p x) @ apD g q @ (p y)^.
+Proof.
+  apply moveL_pV.
+  destruct q; unfold apD, transport.
+  symmetry.
+  exact (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
+Defined.
+
 (** Naturality with other paths hanging around. *)
 Definition concat_pA_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
   {x y : A} (q : x = y)
@@ -479,7 +498,7 @@ Definition concat_pA_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
   (r @ ap f q) @ (p y @ s) = (r @ p x) @ (ap g q @ s).
 Proof.
   destruct q, s; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -490,7 +509,7 @@ Definition concat_pA_p {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
   (r @ ap f q) @ p y = (r @ p x) @ ap g q.
 Proof.
   destruct q; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -501,8 +520,7 @@ Definition concat_A_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
   (ap f q) @ (p y @ s) = (p x) @ (ap g q @ s).
 Proof.
   destruct q, s; cbn.
-  repeat rewrite concat_p1, concat_1p.
-  reflexivity.
+  apply concat_1p.
 Defined.
 
 Definition concat_pA1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
@@ -512,7 +530,7 @@ Definition concat_pA1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
   (r @ ap f q) @ (p y @ s) = (r @ p x) @ (q @ s).
 Proof.
   destruct q, s; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -523,7 +541,7 @@ Definition concat_pp_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
   (r @ p x) @ (ap g q @ s) = (r @ q) @ (p y @ s).
 Proof.
   destruct q, s; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -534,7 +552,7 @@ Definition concat_pA1_p {A : Type} {f : A -> A} (p : forall x, f x = x)
   (r @ ap f q) @ p y = (r @ p x) @ q.
 Proof.
   destruct q; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -545,8 +563,7 @@ Definition concat_A1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
   (ap f q) @ (p y @ s) = (p x) @ (q @ s).
 Proof.
   destruct q, s; cbn.
-  repeat rewrite concat_p1, concat_1p.
-  reflexivity.
+  apply concat_1p.
 Defined.
 
 Definition concat_pp_A1 {A : Type} {g : A -> A} (p : forall x, x = g x)
@@ -556,7 +573,7 @@ Definition concat_pp_A1 {A : Type} {g : A -> A} (p : forall x, x = g x)
   (r @ p x) @ ap g q = (r @ q) @ p y.
 Proof.
   destruct q; simpl.
-  repeat rewrite concat_p1.
+  induction (p x).
   reflexivity.
 Defined.
 
@@ -567,8 +584,7 @@ Definition concat_p_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
   p x @ (ap g q @ s) = q @ (p y @ s).
 Proof.
   destruct q, s; simpl.
-  repeat rewrite concat_p1, concat_1p.
-  reflexivity.
+  symmetry; apply concat_1p.
 Defined.
 
 (** Some coherence lemmas for functoriality *)
@@ -814,7 +830,13 @@ Definition concat_AT {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
   {z w : P x} (r : p = q) (s : z = w)
   : ap (transport P p) s  @  transport2 P r w
     = transport2 P r z  @  ap (transport P q) s
-  := match r with idpath => (concat_p1 _ @ (concat_1p _)^) end.
+  := match r with idpath => (concat_p1_1p _) end.
+
+Definition transport_pp_1 {A : Type} (P : A -> Type) {a b : A} (p : a = b) (x : P a)
+  : transport_pp P p 1 x = transport2 P (concat_p1 p) x.
+Proof.
+  by induction p.
+Defined.
 
 (* TODO: What should this be called? *)
 Lemma ap_transport {A} {P Q : A -> Type} {x y : A} (p : x = y) (f : forall x, P x -> Q x) (z : P x) :
@@ -1048,7 +1070,7 @@ Definition cancelR {A} {x y z : A} (p q : x = y) (r : y = z)
 (** Whiskering and identity paths. *)
 
 Definition whiskerR_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
-  (concat_p1 p) ^ @ whiskerR h 1 @ concat_p1 q = h
+  (concat_p1 p)^ @ whiskerR h 1 @ concat_p1 q = h
   :=
   match h with idpath =>
     match p with idpath =>

theories/Basics/Tactics.v

@@ -421,6 +421,13 @@ Tactic Notation "snrapply" uconstr(term)
 Tactic Notation "snrapply'" uconstr(term)
   := do_with_holes' ltac:(fun x => snrefine x) term.
 
+(** Apply a tactic to one side of an equation.  For example, [lhs rapply lemma].  [tac] should produce a path. *)
+
+Tactic Notation "lhs" tactic3(tac) := nrefine (ltac:(tac) @ _).
+Tactic Notation "lhs_V" tactic3(tac) := nrefine (ltac:(tac)^ @ _).
+Tactic Notation "rhs" tactic3(tac) := nrefine (_ @ ltac:(tac)^).
+Tactic Notation "rhs_V" tactic3(tac) := nrefine (_ @ ltac:(tac)).
+
 (** Ssreflect tactics, adapted by Robbert Krebbers *)
 Ltac done :=
   trivial; intros; solve

theories/Colimits/Coeq.v

@@ -91,7 +91,9 @@ Proof.
     srapply Coeq_ind; intros b.
     1: cbn;reflexivity.
     cbn.
-    abstract (rewrite transport_paths_FlFr, concat_p1, Coeq_rec_beta_cglue, concat_Vp; reflexivity).
+    nrapply transport_paths_FlFr'.
+    apply equiv_p1_1q.
+    nrapply Coeq_rec_beta_cglue.
   - intros [h q]; srapply path_sigma'.
     + reflexivity.
     + cbn.
@@ -134,8 +136,8 @@ Definition functor_coeq_compose {B A f g B' A' f' g' B'' A'' f'' g''}
   == functor_coeq h' k' p' q' o functor_coeq h k p q.
 Proof.
   refine (Coeq_ind _ (fun a => 1) _); cbn; intros b.
-  rewrite transport_paths_FlFr.
-  rewrite concat_p1; apply moveR_Vp; rewrite concat_p1.
+  nrapply transport_paths_FlFr'.
+  apply equiv_p1_1q; symmetry.
   rewrite ap_compose.
   rewrite !functor_coeq_beta_cglue, !ap_pp, functor_coeq_beta_cglue.
   rewrite <- !ap_compose. cbn.

theories/Colimits/Colimit.v

@@ -138,9 +138,9 @@ Proof.
     srapply Colimit_ind.
     1: reflexivity.
     intros ????; cbn.
-    rewrite transport_paths_FlFr.
-    rewrite Colimit_rec_beta_colimp.
-    hott_simpl. }
+    nrapply transport_paths_FlFr'.
+    apply equiv_p1_1q.
+    apply Colimit_rec_beta_colimp. }
   { intros [].
     srapply path_cocone.
     1: reflexivity.
@@ -166,17 +166,16 @@ Proof.
     srapply path_cocone.
     1: reflexivity.
     intros i j f x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
+    apply equiv_p1_1q.
     apply Colimit_rec_beta_colimp.
   - intro f.
     apply path_forall.
     srapply Colimit_ind.
     1: reflexivity.
     intros i j g x; simpl.
-    rewrite transport_paths_FlFr.
-    rewrite Colimit_rec_beta_colimp.
-    refine (ap (fun x => concat x _) (concat_p1 _) @ _).
-    apply concat_Vp.
+    nrapply (transport_paths_FlFr' (g:=f)).
+    apply equiv_p1_1q.
+    apply Colimit_rec_beta_colimp.
 Defined.
 
 Global Instance iscolimit_colimit `{Funext} {G : Graph} (D : Diagram G)

theories/Colimits/Colimit_Coequalizer.v

@@ -70,9 +70,10 @@ Section Coequalizer.
       end.
       + reflexivity.
       + intros b; simpl.
-        rewrite transport_paths_FlFr.
-        rewrite Coeq_rec_beta_cglue.
-        hott_simpl.
+        nrapply (transport_paths_FlFr' (g:=F)).
+        apply equiv_p1_1q.
+        refine (Coeq_rec_beta_cglue _ _ _ _ @ _).
+        apply concat_p1.
   Defined.
 
   Definition equiv_Coeq_Coequalizer `{Funext}

theories/Colimits/Colimit_Pushout.v

@@ -142,12 +142,13 @@ Section PO.
         apply ap, eisretr.
       + reflexivity.
       + intro a; cbn.
-        rewrite transport_paths_FlFr, ap_idmap.
-        rewrite ap_compose, PO_rec_beta_pp.
+        nrapply transport_paths_FFlr'.
+        refine (concat_p1 _ @ _).
+        rewrite PO_rec_beta_pp.
         rewrite eisadj.
         destruct (eissect f a); cbn.
-        rewrite concat_1p, concat_p1.
-        apply concat_Vp.
+        rewrite concat_p1.
+        symmetry; apply concat_Vp.
     - cbn; reflexivity.
   Defined.
 
@@ -191,11 +192,10 @@ Section is_PO_pushout.
         srapply Pushout_ind; cbn.
         1,2: reflexivity.
         intro a; cbn.
-        rewrite transport_paths_FlFr, concat_p1.
-        rewrite Pushout_rec_beta_pglue.
-        eapply moveR_Vp.
-        unfold popp'.
-        by rewrite 2 concat_p1.
+        nrapply transport_paths_FlFr'; apply equiv_p1_1q.
+        unfold popp'; cbn.
+        refine (_ @ concat_p1 _).
+        nrapply Pushout_rec_beta_pglue.
   Defined.
 
   Definition equiv_pushout_PO : Pushout f g <~> PO f g.

theories/Colimits/Pushout.v

@@ -108,8 +108,8 @@ Proof.
     + intros b; reflexivity.
     + intros c; reflexivity.
     + intros a; cbn.
-      abstract (rewrite transport_paths_FlFr, Pushout_rec_beta_pglue;
-                rewrite concat_p1; apply concat_Vp).
+      nrapply transport_paths_FlFr'; apply equiv_p1_1q.
+      nrapply Pushout_rec_beta_pglue.
   - intros [[pushb pushc] pusha]; unfold pushout_unrec; cbn.
     srefine (path_sigma' _ _ _).
     + srefine (path_prod' _ _); reflexivity.
@@ -308,12 +308,12 @@ Section EquivSigmaPushout.
       + reflexivity.
       + reflexivity.
       + intros [x a].
-        rewrite transport_paths_FlFr.
-        rewrite ap_idmap, concat_p1.
-        apply moveR_Vp. rewrite concat_p1.
-        rewrite ap_compose.
-        rewrite esp2_beta_pglue, esp1_beta_pglue.
-        reflexivity.
+        refine (transport_paths_FFlr _ _ @ _).
+        refine (concat_p1 _ @@ 1 @ _).
+        apply moveR_Vp; symmetry.
+        refine (concat_p1 _ @ _).
+        refine (ap _ (esp2_beta_pglue _ _) @ _).
+        apply esp1_beta_pglue.
     - intros [x a]; revert a.
       srefine (Pushout_ind _ _ _ _); cbn.
       + reflexivity.