diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v
index d55200ac193..438fd7202c6 100644
--- a/theories/Basics/Equivalences.v
+++ b/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
diff --git a/theories/Basics/PathGroupoids.v b/theories/Basics/PathGroupoids.v
index 86e76ae197d..afbcf66afda 100644
--- a/theories/Basics/PathGroupoids.v
+++ b/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 =>
diff --git a/theories/Basics/Tactics.v b/theories/Basics/Tactics.v
index 1ef89ea0bf9..c9231e2d474 100644
--- a/theories/Basics/Tactics.v
+++ b/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
diff --git a/theories/Colimits/Coeq.v b/theories/Colimits/Coeq.v
index 4b1463c1c29..b1e249d3298 100644
--- a/theories/Colimits/Coeq.v
+++ b/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.
diff --git a/theories/Colimits/Colimit.v b/theories/Colimits/Colimit.v
index 1ee2c15e931..ea6928cb37d 100644
--- a/theories/Colimits/Colimit.v
+++ b/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)
diff --git a/theories/Colimits/Colimit_Coequalizer.v b/theories/Colimits/Colimit_Coequalizer.v
index 232142cf760..07daaf55457 100644
--- a/theories/Colimits/Colimit_Coequalizer.v
+++ b/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}
diff --git a/theories/Colimits/Colimit_Pushout.v b/theories/Colimits/Colimit_Pushout.v
index 316c1f91342..d6c43982d40 100644
--- a/theories/Colimits/Colimit_Pushout.v
+++ b/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.
diff --git a/theories/Colimits/Pushout.v b/theories/Colimits/Pushout.v
index e00c1e2a0ef..8ebb6edc54f 100644
--- a/theories/Colimits/Pushout.v
+++ b/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.
diff --git a/theories/Cubical/PathSquare.v b/theories/Cubical/PathSquare.v
index 199f548f7ff..988aa6557c2 100644
--- a/theories/Cubical/PathSquare.v
+++ b/theories/Cubical/PathSquare.v
@@ -111,11 +111,10 @@ Section PathSquaresFromPaths.
     {p p' : a00 = a10} {q q' : a00 = a01}.
 
   Definition equiv_sq_G1  : p = p' <~> PathSquare p p' 1 1
-    := sq_path oE (equiv_concat_lr (concat_p1 _)^ (concat_1p _))^-1.
+    := sq_path oE equiv_p1_1q.
 
   Definition equiv_sq_1G : q = q' <~> PathSquare 1 1 q q'
-    := sq_path oE (equiv_concat_lr (concat_1p _)^ (concat_p1 _))^-1
-      oE equiv_path_inverse _ _.
+    := sq_path oE equiv_1p_q1 oE equiv_path_inverse _ _.
 
 End PathSquaresFromPaths.
 
diff --git a/theories/Diagrams/Cocone.v b/theories/Diagrams/Cocone.v
index 864568b379b..cbc82f09037 100644
--- a/theories/Diagrams/Cocone.v
+++ b/theories/Diagrams/Cocone.v
@@ -109,7 +109,7 @@ Section FunctorialityCocone.
     srapply path_cocone; intro i.
     1: reflexivity.
     intros j g x; simpl.
-    refine (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
+    apply equiv_p1_1q, ap_idmap.
   Defined.
 
   Definition cocone_postcompose_comp {D : Diagram G}
@@ -120,7 +120,7 @@ Section FunctorialityCocone.
     srapply path_cocone; intro i.
     1: reflexivity.
     intros j h x; simpl.
-    refine (concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).
+    apply equiv_p1_1q, ap_compose.
   Defined.
 
   (** ** Precomposition for cocones *)
@@ -149,7 +149,7 @@ Section FunctorialityCocone.
     intro C; srapply path_cocone; simpl.
     1: reflexivity.
     intros; simpl.
-    refine (concat_p1 _).
+    apply concat_p1.
   Defined.
 
   Definition cocone_precompose_comp {D1 D2 D3 : Diagram G}
@@ -161,7 +161,7 @@ Section FunctorialityCocone.
     srapply path_cocone.
     1: reflexivity.
     intros i j g x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
+    apply equiv_p1_1q.
     unfold CommutativeSquares.comm_square_comp.
     refine (concat_p_pp _ _ _ @ _).
     apply ap10, ap.
@@ -183,7 +183,7 @@ Section FunctorialityCocone.
     srapply path_cocone; intro i.
     1: reflexivity.
     intros j g x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
+    apply equiv_p1_1q.
     etransitivity.
     + apply ap_pp.
     + apply ap10, ap.
diff --git a/theories/Diagrams/Cone.v b/theories/Diagrams/Cone.v
index 656ccb763a3..859aa622dac 100644
--- a/theories/Diagrams/Cone.v
+++ b/theories/Diagrams/Cone.v
@@ -106,7 +106,7 @@ Section FunctorialityCone.
     srapply path_cone; intro i.
     1: reflexivity.
     intros j g x; simpl.
-    refine (concat_p1 _ @ (concat_1p _)^).
+    apply concat_p1_1p.
   Defined.
 
   Definition cone_precompose_comp {D : Diagram G}
@@ -117,7 +117,7 @@ Section FunctorialityCone.
     srapply path_cone; intro i.
     1: reflexivity.
     intros j h x; simpl.
-    refine (concat_p1 _ @ (concat_1p _)^).
+    apply concat_p1_1p.
   Defined.
 
   (** ** Postcomposition for cones *)
@@ -157,7 +157,7 @@ Section FunctorialityCone.
     srapply path_cone.
     1: reflexivity.
     intros i j g x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
+    apply equiv_p1_1q.
     unfold CommutativeSquares.comm_square_comp.
     refine (_ @ concat_p_pp _ _ _).
     apply ap.
@@ -177,8 +177,7 @@ Section FunctorialityCone.
     srapply path_cone; intro i.
     1: reflexivity.
     intros j g x; simpl.
-    refine (concat_p1 _ @ _ @ (concat_1p _)^).
-    reflexivity.
+    apply concat_p1_1p.
   Defined.
 
   (** The postcomposition with a diagram equivalence is an equivalence. *)
diff --git a/theories/Homotopy/BlakersMassey.v b/theories/Homotopy/BlakersMassey.v
index ecbcc9e1197..3ec2e162a5b 100644
--- a/theories/Homotopy/BlakersMassey.v
+++ b/theories/Homotopy/BlakersMassey.v
@@ -1,7 +1,7 @@
 Require Import HoTT.Basics HoTT.Types.
 Require Import Colimits.Pushout.
 Require Import Colimits.SpanPushout.
-Require Import Homotopy.Join.
+Require Import Homotopy.Join.Core.
 Require Import Truncations.
 
 (** * The Generalized Blakers-Massey Theorem *)
diff --git a/theories/Homotopy/CayleyDickson.v b/theories/Homotopy/CayleyDickson.v
index 28f13d2a379..966981f7fb3 100644
--- a/theories/Homotopy/CayleyDickson.v
+++ b/theories/Homotopy/CayleyDickson.v
@@ -2,7 +2,7 @@ Require Import Cubical.
 Require Import Pointed.
 Require Import Homotopy.HSpace.Core.
 Require Import Homotopy.Suspension.
-Require Import Homotopy.Join.
+Require Import Homotopy.Join.Core.
 
 Local Open Scope pointed_scope.
 Local Open Scope mc_mult_scope.
@@ -268,7 +268,7 @@ Section ImaginaroidHSpace.
         apply jglue. }
     intros a b.
     apply path_forall.
-    srapply Join_ind.
+    srapply Join_ind_dp.
     1: intro; apply jglue.
     1: intro; cbn; symmetry; apply jglue.
     intros c d.
@@ -300,7 +300,7 @@ Section ImaginaroidHSpace.
   Global Instance cd_op_left_identity
     : LeftIdentity cd_op pt.
   Proof.
-    srapply Join_ind.
+    srapply Join_ind_dp.
     { unfold cd_op, Join_rec, Pushout.Pushout_rec, Pushout.Pushout_ind; simpl;
         intro a; apply ap.
       srapply hspace_left_identity. }
@@ -316,7 +316,7 @@ Section ImaginaroidHSpace.
   Global Instance cd_op_right_identity
     : RightIdentity cd_op pt.
   Proof.
-    srapply Join_ind.
+    srapply Join_ind_dp.
     { unfold cd_op, Join_rec, Pushout.Pushout_rec, Pushout.Pushout_ind; simpl.
       intro a; apply ap.
       srapply hspace_right_identity. }
diff --git a/theories/Homotopy/Join.v b/theories/Homotopy/Join.v
index e39605a1dc9..8c904c128ab 100644
--- a/theories/Homotopy/Join.v
+++ b/theories/Homotopy/Join.v
@@ -1,281 +1,4 @@
-Require Import Basics Types Cubical.
-Require Import NullHomotopy.
-Require Import Extensions.
-Require Import Colimits.Pushout.
-Require Import Truncations.Core Truncations.Connectedness.
-Require Import Pointed.Core.
+Require Export Join.Core.
+Require Export Join.TriJoin.
+Require Export Join.JoinAssoc.
 
-Local Open Scope pointed_scope.
-Local Open Scope path_scope.
-
-(** * Joins *)
-
-(** The join is the pushout of two types under their product. *)
-Section Join.
-
-  Definition Join (A : Type@{i}) (B : Type@{j})
-    := Pushout@{k i j k} (@fst A B) (@snd A B).
-
-  Definition joinl {A B} : A -> Join A B
-    := fun a => @pushl (A*B) A B fst snd a.
-
-  Definition joinr {A B} : B -> Join A B
-    := fun b => @pushr (A*B) A B fst snd b.
-
-  Definition jglue {A B} a b : joinl a = joinr b
-    := @pglue (A*B) A B fst snd (a , b).
-
-  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, DPath P (jglue a b) (P_A a) (P_B b))
-    : forall (x : Join A B), P x.
-  Proof.
-    srapply (Pushout_ind P P_A P_B).
-    intros [a b].
-    apply dp_path_transport^-1.
-    exact (P_g a b).
-  Defined.
-
-  Definition Join_ind_beta_jglue {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, DPath P (jglue a b) (P_A a) (P_B b)) a b
-    : dp_apD (Join_ind P P_A P_B P_g) (jglue a b) = P_g a b.
-  Proof.
-    apply dp_apD_path_transport.
-    srapply Pushout_ind_beta_pglue.
-  Defined.
-
-  Definition Join_rec {A B P : Type} (P_A : A -> P) (P_B : B -> P)
-    (P_g : forall a b, P_A a = P_B b) : Join A B -> P.
-  Proof.
-    srapply (Pushout_rec P P_A P_B).
-    intros [a b].
-    apply P_g.
-  Defined.
-
-  Definition Join_rec_beta_jglue {A B P : Type} (P_A : A -> P)
-    (P_B : B -> P) (P_g : forall a b, P_A a = P_B b) a b
-    : ap (Join_rec P_A P_B P_g) (jglue a b) = P_g a b.
-  Proof.
-    srapply Pushout_rec_beta_pglue.
-  Defined.
-
-  (** Joining with a contractible type produces a contractible type *)
-  Global Instance contr_join A B `{Contr A} : Contr (Join A B).
-  Proof.
-    exists (pushl (center A)).
-    intros y; simple refine (Pushout_ind _ _ _ _ y).
-    - intros a; apply ap, contr.
-    - intros b; exact (pglue (center A , b)).
-    - intros [a b]; cbn.
-      refine ( _ @ apD (fun a' => jglue a' b) (contr a)^).
-      rewrite transport_paths_r, transport_paths_FlFr; cbn.
-      rewrite ap_V, inv_V, concat_pp_p.
-      rewrite ap_const, concat_p1.
-      reflexivity.
-  Defined.
-
-  (** Join is symmetric *)
-  Definition join_sym A B : Join A B <~> Join B A.
-  Proof.
-    unfold Join; refine (pushout_sym oE _).
-    refine (equiv_pushout (equiv_prod_symm A B) 1 1 _ _);
-      intros [a b]; reflexivity.
-  Defined.
-
-  Definition join_natsq_v {A B : Type} {a a' : A} {b b' : B}
-    (p : a = a') (q : b = b')
-    : PathSquare (ap joinl p) (ap joinr q) (jglue a b) (jglue a' b').
-  Proof.
-    destruct p, q.
-    apply sq_refl_v.
-  Defined.
-
-  Definition join_natsq_h {A B : Type} {a a' : A} {b b' : B}
-    (p : a = a') (q : b = b')
-    : PathSquare (jglue a b) (jglue a' b') (ap joinl p) (ap joinr q).
-  Proof.
-    destruct p, q.
-    apply sq_refl_h.
-  Defined.
-
-  Definition functor_join {A B C D} (f : A -> C) (g : B -> D)
-    : Join A B -> Join C D.
-  Proof.
-    srapply Join_rec.
-    1: intro a; apply joinl, f, a.
-    1: intro b; apply joinr, g, b.
-    intros a b.
-    apply jglue.
-  Defined.
-
-  Definition functor_join_compose {A B C D E F}
-    (f : A -> C) (g : B -> D) (h : C -> E) (i : D -> F)
-    : functor_join (h o f) (i o g) == functor_join h i o functor_join f g.
-  Proof.
-    srapply Join_ind.
-    1,2: reflexivity.
-    intros a b.
-    simpl.
-    apply sq_dp^-1.
-    apply sq_1G.
-    symmetry.
-    rewrite ap_compose.
-    rewrite 3 Join_rec_beta_jglue.
-    reflexivity.
-  Defined.
-
-  Definition functor_join_idmap {A}
-    : functor_join idmap idmap == (idmap : Join A A -> Join A A).
-  Proof.
-    srapply Join_ind.
-    1,2: reflexivity.
-    intros a b.
-    cbn; apply dp_paths_FlFr.
-    rewrite Join_rec_beta_jglue.
-    rewrite ap_idmap, concat_p1.
-    apply concat_Vp.
-  Defined.
-
-  Global Instance isequiv_functor_join {A B C D}
-    (f : A -> C) `{!IsEquiv f} (g : B -> D) `{!IsEquiv g}
-    : IsEquiv (functor_join f g).
-  Proof.
-    srapply isequiv_adjointify.
-    1: apply (functor_join f^-1 g^-1).
-    1,2: srapply Join_ind.
-    1,2: intro; unfold functor_join, Join_rec, Pushout_rec, Pushout_ind; simpl.
-    1,2: apply ap, eisretr.
-    2,3: intro; unfold functor_join, Join_rec, Pushout_rec, Pushout_ind; simpl.
-    2,3: apply ap, eissect.
-    1,2: intros c d; cbn.
-    1,2: apply sq_dp^-1.
-     1 : rewrite (ap_compose _ (functor_join f g)).
-     2 : rewrite (ap_compose (functor_join f g)).
-    1,2: rewrite 2 Join_rec_beta_jglue, ap_idmap.
-    1,2: apply join_natsq_v.
-  Defined.
-
-  Definition equiv_functor_join {A B C D} (f : A <~> C) (g : B <~> D)
-    : Join A B <~> Join C D := Build_Equiv _ _ (functor_join f g) _.
-
-  (** The join of hprops is an hprop *)
-  Global Instance ishprop_join `{Funext} A B `{IsHProp A} `{IsHProp B} : IsHProp (Join A B).
-  Proof.
-    apply hprop_inhabited_contr.
-    unfold Join.
-    refine (Pushout_rec _ _ _ (fun _ => path_ishprop _ _)).
-    - intros a; apply contr_join.  
-      exact (contr_inhabited_hprop A a).
-    - intros b; refine (istrunc_equiv_istrunc (Join B A) (join_sym B A)).
-      apply contr_join.
-      exact (contr_inhabited_hprop B b).
-  Defined.
-
-  Lemma equiv_into_hprop `{Funext} {A B P : Type} `{IsHProp P} (f : A -> P)
-    : (Join A B -> P) <~> (B -> P).
-  Proof.
-    srapply equiv_iff_hprop.
-    1: exact (fun f => f o joinr).
-    intros g.
-    srapply Join_rec.
-    1,2: assumption.
-    intros a b.
-    apply path_ishprop.
-  Defined.
-
-  (** And coincides with their disjunction *)
-  Definition equiv_join_hor `{Funext} A B `{IsHProp A} `{IsHProp B} 
-    : Join A B <~> hor A B.
-  Proof.
-    apply equiv_iff_hprop.
-    - refine (Pushout_rec _ (fun a => tr (inl a)) (fun b => tr (inr b)) (fun _ => path_ishprop _ _)).
-    - apply Trunc_rec, push.
-  Defined.
-
-  (** Joins add connectivity *)
-  Global Instance isconnected_join `{Univalence} {m n : trunc_index}
-         (A B : Type) `{IsConnected m A} `{IsConnected n B}
-    : IsConnected (m +2+ n) (Join A B).
-  Proof.
-    apply isconnected_from_elim; intros C ? k.
-    pose @istrunc_inO_tr.
-    pose proof (istrunc_extension_along_conn
-                  (fun b:B => tt) (fun _ => C) (k o pushr)).
-    unfold ExtensionAlong in *.
-    transparent assert (f : (A -> {s : Unit -> C &
-                                   forall x, s tt = k (pushr x)})).
-    { intros a; exists (fun _ => k (pushl a)); intros b.
-      exact (ap k (jglue a b)). }
-    assert (h := isconnected_elim
-                   m {s : Unit -> C & forall x : B, s tt = k (pushr x)} f).
-    unfold NullHomotopy in *; destruct h as [[c g] h].
-    exists (c tt).
-    srefine (Pushout_ind _ _ _ _).
-    - intros a; cbn. exact (ap10 (h a)..1 tt).
-    - intros b; cbn. exact ((g b)^).
-    - intros [a b].
-      rewrite transport_paths_FlFr, ap_const, concat_p1; cbn.
-      subst f; set (ha := h a); clearbody ha; clear h;
-      assert (ha2 := ha..2); set (ha1 := ha..1) in *;
-      clearbody ha1; clear ha; cbn in *.
-      rewrite <- (inv_V (ap10 ha1 tt)).
-      rewrite <- inv_pp.
-      apply inverse2.
-      refine (_ @ apD10 ha2 b); clear ha2.
-      rewrite transport_forall_constant, transport_paths_FlFr.
-      rewrite ap_const, concat_p1.
-      reflexivity.
-  Defined.
-
-  Definition pjoin (A : pType) (B : Type) : pType
-    := [Join A B, joinl pt].
-
-End Join.
-
-(** Diamond lemmas for Join *)
-Section Diamond.
-
-  Context {A B : Type}.
-
-  Definition Diamond (a a' : A) (b b' : B)
-    := PathSquare (jglue a b) (jglue a' b')^ (jglue a b') (jglue a' b)^.
-
-  Definition diamond_h {a a' : A} (b b' : B) (p : a = a')
-    : Diamond a a' b b'.
-  Proof.
-    destruct p.
-    apply sq_path.
-    exact (concat_pV _ @ (concat_pV _)^).
-  Defined.
-
-  Definition diamond_v (a a' : A) {b b' : B} (p : b = b')
-    : Diamond a a' b b'.
-  Proof.
-    destruct p.
-    by apply sq_path.
-  Defined.
-
-  Lemma diamond_symm (a : A) (b : B)
-    : diamond_v a a 1 = diamond_h b b 1.
-  Proof.
-    unfold diamond_v, diamond_h.
-    symmetry; apply ap, concat_pV.
-  Defined.
-
-End Diamond.
-
-Definition diamond_twist {A : Type} {a a' : A} (p : a = a')
-  : DPath (fun x => Diamond a' x a x) p
-    (diamond_v a' a 1) (diamond_h a a' 1).
-Proof.
-  destruct p.
-  apply diamond_symm.
-Defined.
-
-(** The join of n.+1 copies of a type. *)
-Fixpoint Join_power (A : Type) (n : nat) : Type :=
-  match n with
-  | 0%nat => A
-  | m.+1%nat => Join A (Join_power A m)
-  end.
diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v
new file mode 100644
index 00000000000..2facc4b3158
--- /dev/null
+++ b/theories/Homotopy/Join/Core.v
@@ -0,0 +1,792 @@
+Require Import Basics Types Cubical.
+Require Import NullHomotopy.
+Require Import Extensions.
+Require Import Colimits.Pushout.
+Require Import Truncations.Core Truncations.Connectedness.
+Require Import Pointed.Core.
+Require Import WildCat.
+
+Local Open Scope pointed_scope.
+Local Open Scope path_scope.
+
+(** * Joins *)
+
+(** The join is the pushout of two types under their product. *)
+Section Join.
+
+  Definition Join (A : Type@{i}) (B : Type@{j})
+    := Pushout@{k i j k} (@fst A B) (@snd A B).
+
+  Definition joinl {A B} : A -> Join A B
+    := fun a => @pushl (A*B) A B fst snd a.
+
+  Definition joinr {A B} : B -> Join A B
+    := fun b => @pushr (A*B) A B fst snd b.
+
+  Definition jglue {A B} a b : joinl a = joinr b
+    := @pglue (A*B) A B fst snd (a , b).
+
+  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))
+    : forall (x : Join A B), P x.
+  Proof.
+    apply (Pushout_ind P P_A P_B).
+    exact (fun ab => P_g (fst ab) (snd ab)).
+  Defined.
+
+  Definition Join_ind_beta_jglue {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)) a b
+    : apD (Join_ind P P_A P_B P_g) (jglue a b) = P_g a b
+    := Pushout_ind_beta_pglue _ _ _ _ _.
+
+  (* A version of [Join_ind] that uses dependant paths. *)
+  Definition Join_ind_dp {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, DPath P (jglue a b) (P_A a) (P_B b))
+    : forall (x : Join A B), P x.
+  Proof.
+    refine (Join_ind P P_A P_B _).
+    intros a b.
+    apply dp_path_transport^-1.
+    exact (P_g a b).
+  Defined.
+
+  Definition Join_ind_dp_beta_jglue {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, DPath P (jglue a b) (P_A a) (P_B b)) a b
+    : dp_apD (Join_ind_dp P P_A P_B P_g) (jglue a b) = P_g a b.
+  Proof.
+    apply dp_apD_path_transport.
+    snrapply Join_ind_beta_jglue.
+  Defined.
+
+  (** A version of [Join_ind] specifically for proving that two functions defined on a [Join] are homotopic. *)
+  Definition Join_ind_FlFr {A B P : Type} (f g : Join A B -> P)
+    (Hl : forall a, f (joinl a) = g (joinl a))
+    (Hr : forall b, f (joinr b) = g (joinr b))
+    (Hglue : forall a b, ap f (jglue a b) @ Hr b = Hl a @ ap g (jglue a b))
+    : f == g.
+  Proof.
+    snrapply Join_ind.
+    - exact Hl.
+    - exact Hr.
+    - intros a b.
+      nrapply transport_paths_FlFr'.
+      apply Hglue.
+  Defined.
+
+  (** And a version for showing that a composite is homotopic to the identity. *)
+  Definition Join_ind_FFlr {A B P : Type} (f : Join A B -> P) (g : P -> Join A B)
+    (Hl : forall a, g (f (joinl a)) = joinl a)
+    (Hr : forall b, g (f (joinr b)) = joinr b)
+    (Hglue : forall a b, ap g (ap f (jglue a b)) @ Hr b = Hl a @ jglue a b)
+    : forall x, g (f x) = x.
+  Proof.
+    snrapply Join_ind.
+    - exact Hl.
+    - exact Hr.
+    - intros a b.
+      nrapply transport_paths_FFlr'.
+      apply Hglue.
+  Defined.
+
+  Definition Join_rec {A B P : Type} (P_A : A -> P) (P_B : B -> P)
+    (P_g : forall a b, P_A a = P_B b) : Join A B -> P.
+  Proof.
+    apply (Pushout_rec P P_A P_B).
+    exact (fun ab => P_g (fst ab) (snd ab)).
+  Defined.
+
+  Definition Join_rec_beta_jglue {A B P : Type} (P_A : A -> P)
+    (P_B : B -> P) (P_g : forall a b, P_A a = P_B b) a b
+    : ap (Join_rec P_A P_B P_g) (jglue a b) = P_g a b.
+  Proof.
+    snrapply Pushout_rec_beta_pglue.
+  Defined.
+
+  (** If [A] is ipointed, so is [Join A B]. *)
+  Definition pjoin (A : pType) (B : Type) : pType
+    := [Join A B, joinl pt].
+
+End Join.
+
+(** * We now prove many things about [Join_rec], for example, that it is an equivalence of 0-groupoids from the [JoinRecData] that we define next.  The framework we use is a bit elaborate, but it parallels the framework used in TriJoin.v, where careful organization is essential. *)
+
+Record JoinRecData {A B P : Type} := {
+    jl : A -> P;
+    jr : B -> P;
+    jg : forall a b, jl a = jr b;
+  }.
+
+Arguments JoinRecData : clear implicits.
+Arguments Build_JoinRecData {A B P}%type_scope (jl jr jg)%function_scope.
+
+(** We use the name [join_rec] for the version of [Join_rec] defined on this data. *)
+Definition join_rec {A B P : Type} (f : JoinRecData A B P)
+  : Join A B -> P
+  := Join_rec (jl f) (jr f) (jg f).
+
+Definition join_rec_beta_jg {A B P : Type} (f : JoinRecData A B P) (a : A) (b : B)
+  : ap (join_rec f) (jglue a b) = jg f a b
+  := Join_rec_beta_jglue _ _ _ a b.
+
+(** * We're next going to define a map in the other direction.  We do it via showing that [JoinRecData] is a 0-coherent 1-functor to [Type]. We'll later show that it is a 1-functor to 0-groupoids. *)
+Definition joinrecdata_fun {A B P Q : Type} (g : P -> Q) (f : JoinRecData A B P)
+  : JoinRecData A B Q.
+Proof.
+  snrapply Build_JoinRecData.
+  - exact (g o jl f).
+  - exact (g o jr f).
+  - exact (fun a b => ap g (jg f a b)).
+Defined.
+
+(** The join itself has canonical [JoinRecData]. *)
+Definition joinrecdata_join (A B : Type) : JoinRecData A B (Join A B)
+  := Build_JoinRecData joinl joinr jglue.
+
+(** Combining these gives a function going in the opposite direction to [join_rec]. *)
+Definition join_rec_inv {A B P : Type} (f : Join A B -> P)
+  : JoinRecData A B P
+  := joinrecdata_fun f (joinrecdata_join A B).
+
+(** * Under [Funext], [join_rec] and [join_rec_inv] should be inverse equivalences.  We'll avoid [Funext] and show that they are equivalences of 0-groupoids, where we choose the path structures carefully.  We begin by describing a notion of paths between elements of [JoinRecData A B P]. Under [Funext], this type will be equivalent to the identity type.  But without [Funext], this definition will be more useful. *)
+
+Record JoinRecPath {A B P : Type} {f g : JoinRecData A B P} := {
+    hl : forall a, jl f a = jl g a;
+    hr : forall b, jr f b = jr g b;
+    hg : forall a b, jg f a b @ hr b = hl a @ jg g a b;
+  }.
+
+Arguments JoinRecPath {A B P} f g.
+
+(** In the special case where the first two components of [f] and [g] agree definitionally, [hl] and [hr] can be identity paths, and [hg] simplifies slightly. *)
+Definition bundle_joinrecpath {A B P : Type} {jl' : A -> P} {jr' : B -> P}
+  {f g : forall a b, jl' a = jr' b}
+  (h : forall a b, f a b = g a b)
+  : JoinRecPath (Build_JoinRecData jl' jr' f) (Build_JoinRecData jl' jr' g).
+Proof.
+  snrapply Build_JoinRecPath.
+  1, 2: reflexivity.
+  intros; apply equiv_p1_1q, h.
+Defined.
+
+(** A tactic that helps us apply the previous result. *)
+Ltac bundle_joinrecpath :=
+  hnf;
+  match goal with |- JoinRecPath ?F ?G =>
+    refine (bundle_joinrecpath (f:=jg F) (g:=jg G) _) end.
+
+(** Using [JoinRecPath], we can restate the beta rule for [join_rec]. This says that [join_rec_inv] is split surjective. *)
+Definition join_rec_beta {A B P : Type} (f : JoinRecData A B P)
+  : JoinRecPath (join_rec_inv (join_rec f)) f
+  := bundle_joinrecpath (join_rec_beta_jg f).
+
+(** [join_rec_inv] is essentially injective, as a map between 0-groupoids. *)
+Definition isinj_join_rec_inv {A B P : Type} {f g : Join A B -> P}
+  (h : JoinRecPath (join_rec_inv f) (join_rec_inv g))
+  : f == g
+  := Join_ind_FlFr _ _ (hl h) (hr h) (hg h).
+
+(** * We now introduce several lemmas and tactics that will dispense with some routine goals. The idea is that a generic interval can be assumed to be trivial on the first vertex, and a generic square can be assumed to be the identity on the domain edge. In order to apply the [paths_ind] and [square_ind] lemmas that make this precise, we need to generalize various terms in the goal. *)
+
+(** This destructs a three component term [f], generalizes each piece evaluated appropriately, and clears all pieces. *)
+Ltac generalize_three f a b :=
+  let fg := fresh in let fr := fresh in let fl := fresh in
+  destruct f as [fl fr fg]; cbn;
+  generalize (fg a b); clear fg;
+  generalize (fr b); clear fr;
+  generalize (fl a); clear fl.
+
+(** For [f : JoinRecData A B P], if we have [a] and [b] and are trying to prove a statement only involving [jl f a], [jr f b] and [jg f a b], we can assume [jr f b] is [jl f a] and that [jg f a b] is reflexivity.  This is just path induction, but it requires generalizing the goal appropriately. *)
+Ltac interval_ind f a b :=
+  generalize_three f a b;
+  intro f; (* We really only wanted two of them generalized here, so we intro one. *)
+  apply paths_ind.
+
+(** Similarly, for [h : JoinRecPath f g], if we have [a] and [b] and are trying to prove a goal only involving [h] and [g] evaluated at those points, we can assume that [g] is [f] and that [h] is "reflexivity".  For this, we first define a lemma that is like "path induction on h", and then a tactic that uses it. *)
+
+Definition square_ind {P : Type} (a b : P) (ab : a = b)
+  (Q : forall (a' b' : P) (ab' : a' = b') (ha : a = a') (hb : b = b') (k : ab @ hb = ha @ ab'), Type)
+  (s : Q a b ab idpath idpath (equiv_p1_1q idpath))
+  : forall a' b' ab' ha hb k, Q a' b' ab' ha hb k.
+Proof.
+  intros.
+  induction ha, hb.
+  revert k; equiv_intro (equiv_p1_1q (p:=ab) (q:=ab')) k'; induction k'.
+  induction ab.
+  exact s.
+Defined.
+
+(* [g] should be the codomain of [h]. *)
+Global Ltac square_ind g h a b :=
+  generalize_three h a b;
+  generalize_three g a b;
+  apply square_ind.
+
+(** * Here we start using the WildCat library to organize things. *)
+
+(** We begin by showing that [JoinRecData A B P] is a 0-groupoid, one piece at a time. *)
+Global Instance isgraph_joinrecdata (A B P : Type) : IsGraph (JoinRecData A B P)
+  := {| Hom := JoinRecPath |}.
+
+Global Instance is01cat_joinrecdata (A B P : Type) : Is01Cat (JoinRecData A B P).
+Proof.
+  apply Build_Is01Cat.
+  - intro f.
+    bundle_joinrecpath.
+    reflexivity.
+  - intros f1 f2 f3 h2 h1.
+    snrapply Build_JoinRecPath; intros; cbn beta.
+    + exact (hl h1 a @ hl h2 a).
+    + exact (hr h1 b @ hr h2 b).
+    + (* Some simple path algebra works as well. *)
+      square_ind f3 h2 a b.
+      square_ind f2 h1 a b.
+      by interval_ind f1 a b.
+Defined.
+
+Global Instance is0gpd_joinrecdata (A B P : Type) : Is0Gpd (JoinRecData A B P).
+Proof.
+  apply Build_Is0Gpd.
+  intros f g h.
+  snrapply Build_JoinRecPath; intros; cbn beta.
+  + exact (hl h a)^.
+  + exact (hr h b)^.
+  + (* Some simple path algebra works as well. *)
+    square_ind g h a b.
+    by interval_ind f a b.
+Defined.
+
+Definition joinrecdata_0gpd (A B P : Type) : ZeroGpd
+  := Build_ZeroGpd (JoinRecData A B P) _ _ _.
+
+(** * Next we show that [joinrecdata_0gpd A B] is a 1-functor from [Type] to [ZeroGpd]. *)
+
+(** It's a 1-functor that lands in [ZeroGpd], and the morphisms of [ZeroGpd] are 0-functors, so it's easy to get confused about the levels. *)
+
+(** First we need to show that the induced map is a morphism in [ZeroGpd], i.e. that it is a 0-functor. *)
+Global Instance is0functor_joinrecdata_fun {A B P Q : Type} (g : P -> Q)
+  : Is0Functor (@joinrecdata_fun A B P Q g).
+Proof.
+  apply Build_Is0Functor.
+  intros f1 f2 h.
+  snrapply Build_JoinRecPath; intros; cbn.
+  - exact (ap g (hl h a)).
+  - exact (ap g (hr h b)).
+  - square_ind f2 h a b.
+    by interval_ind f1 a b.
+Defined.
+
+(** [joinrecdata_0gpd A B] is a 0-functor from [Type] to [ZeroGpd] (one level up). *)
+Global Instance is0functor_joinrecdata_0gpd (A B : Type) : Is0Functor (joinrecdata_0gpd A B).
+Proof.
+  apply Build_Is0Functor.
+  intros P Q g.
+  snrapply Build_Morphism_0Gpd.
+  - exact (joinrecdata_fun g).
+  - apply is0functor_joinrecdata_fun.
+Defined.
+
+(** [joinrecdata_0gpd A B] is a 1-functor from [Type] to [ZeroGpd]. *)
+Global Instance is1functor_joinrecdata_0gpd (A B : Type) : Is1Functor (joinrecdata_0gpd A B).
+Proof.
+  apply Build_Is1Functor.
+  (* If [g1 g2 : P -> Q] are homotopic, then the induced maps are homotopic: *)
+  - intros P Q g1 g2 h f; cbn in *.
+    snrapply Build_JoinRecPath; intros; cbn.
+    1, 2: apply h.
+    interval_ind f a b; cbn.
+    apply concat_1p_p1.
+  (* The identity map [P -> P] is sent to a map homotopic to the identity. *)
+  - intros P f; cbn.
+    bundle_joinrecpath; intros; cbn.
+    apply ap_idmap.
+  (* It respects composition. *)
+  - intros P Q R g1 g2 f; cbn.
+    bundle_joinrecpath; intros; cbn.
+    apply ap_compose.
+Defined.
+
+Definition joinrecdata_0gpd_fun (A B : Type) : Fun11 Type ZeroGpd
+  := Build_Fun11 _ _ (joinrecdata_0gpd A B).
+
+(** By the Yoneda lemma, it follows from [JoinRecData] being a 1-functor that given [JoinRecData] in [J], we get a map [(J -> P) $-> (JoinRecData A B P)] of 0-groupoids which is natural in [P]. Below we will specialize to the case where [J] is [Join A B] with the canonical [JoinRecData]. *)
+Definition join_nattrans_recdata {A B J : Type} (f : JoinRecData A B J)
+  : NatTrans (opyon_0gpd J) (joinrecdata_0gpd_fun A B).
+Proof.
+  srapply Build_NatTrans.  (* This finds the Yoneda lemma via typeclass search. Is that what we want? *)
+  Unshelve.
+  exact f.
+Defined.
+
+(** Thus we get a map [(Join A B -> P) $-> (JoinRecData A B P)] of 0-groupoids, natural in [P]. The underlying map is [join_rec_inv A B P]. *)
+Definition join_rec_inv_nattrans (A B : Type)
+  : NatTrans (opyon_0gpd (Join A B)) (joinrecdata_0gpd_fun A B)
+  := join_nattrans_recdata (joinrecdata_join A B).
+
+(** This natural transformation is in fact a natural equivalence of 0-groupoids. *)
+Definition join_rec_inv_natequiv (A B : Type)
+  : NatEquiv (opyon_0gpd (Join A B)) (joinrecdata_0gpd_fun A B).
+Proof.
+  snrapply Build_NatEquiv'.
+  1: apply join_rec_inv_nattrans.
+  intro P.
+  apply isequiv_0gpd_issurjinj.
+  apply Build_IsSurjInj.
+  - intros f; cbn in f.
+    exists (join_rec f).
+    apply join_rec_beta.
+  - exact (@isinj_join_rec_inv A B P).
+Defined.
+
+(** It will be handy to name the inverse natural equivalence. *)
+Definition join_rec_natequiv (A B : Type)
+  := natequiv_inverse _ _ (join_rec_inv_natequiv A B).
+
+(** [join_rec_natequiv A B P] is an equivalence of 0-groupoids whose underlying function is definitionally [join_rec]. *)
+Local Definition join_rec_natequiv_check (A B P : Type)
+  : equiv_fun_0gpd (join_rec_natequiv A B P) = @join_rec A B P
+  := idpath.
+
+(** It follows that [join_rec A B P] is a 0-functor. *)
+Global Instance is0functor_join_rec (A B P : Type) : Is0Functor (@join_rec A B P).
+Proof.
+  change (Is0Functor (equiv_fun_0gpd (join_rec_natequiv A B P))).
+  exact _.
+Defined.
+
+(** And that [join_rec A B] is natural.   The [$==] in the statement is just [==], but we use WildCat notation so that we can invert and compose these with WildCat notation. *)
+Definition join_rec_nat (A B : Type) {P Q : Type} (g : P -> Q) (f : JoinRecData A B P)
+  : join_rec (joinrecdata_fun g f) $== g o join_rec f.
+Proof.
+  exact (isnat (join_rec_natequiv A B) g f).
+Defined.
+
+(** * Various types of equalities between paths in joins. *)
+
+(** Naturality squares for given paths in [A] and [B]. *)
+Section JoinNatSq.
+
+  Definition join_natsq {A B : Type} {a a' : A} {b b' : B}
+    (p : a = a') (q : b = b')
+    : (ap joinl p) @ (jglue a' b') = (jglue a b) @ (ap joinr q).
+  Proof.
+    destruct p, q.
+    apply concat_1p_p1.
+  Defined.
+
+  Definition join_natsq_v {A B : Type} {a a' : A} {b b' : B}
+    (p : a = a') (q : b = b')
+    : PathSquare (ap joinl p) (ap joinr q) (jglue a b) (jglue a' b').
+  Proof.
+    destruct p, q.
+    apply sq_refl_v.
+  Defined.
+
+  Definition join_natsq_h {A B : Type} {a a' : A} {b b' : B}
+    (p : a = a') (q : b = b')
+    : PathSquare (jglue a b) (jglue a' b') (ap joinl p) (ap joinr q).
+  Proof.
+    destruct p, q.
+    apply sq_refl_h.
+  Defined.
+
+End JoinNatSq.
+
+(** The triangles that arise when one of the given paths is reflexivity. *)
+Section Triangle.
+
+  Context {A B : Type}.
+
+  Definition triangle_h {a a' : A} (b : B) (p : a = a')
+    : jglue a b @ (jglue a' b)^ = ap joinl p.
+  Proof.
+    destruct p.
+    apply concat_pV.
+  Defined.
+
+  Definition triangle_h' {a a' : A} (b : B) (p : a = a')
+    : ap joinl p @ (jglue a' b) = jglue a b.
+  Proof.
+    destruct p.
+    apply concat_1p.
+  Defined.
+
+  Definition triangle_v (a : A) {b b' : B} (p : b = b')
+    : (jglue a b)^ @ jglue a b' = ap joinr p.
+  Proof.
+    destruct p.
+    apply concat_Vp.
+  Defined.
+
+  Definition triangle_v' (a : A) {b b' : B} (p : b = b')
+    : jglue a b @ ap joinr p = jglue a b'.
+  Proof.
+    destruct p.
+    apply concat_p1.
+  Defined.
+
+End Triangle.
+
+(** Diamond lemmas for Join *)
+Section Diamond.
+
+  Context {A B : Type}.
+
+  Definition Diamond (a a' : A) (b b' : B)
+    := PathSquare (jglue a b) (jglue a' b')^ (jglue a b') (jglue a' b)^.
+
+  Definition diamond_h {a a' : A} (b b' : B) (p : a = a')
+    : Diamond a a' b b'.
+  Proof.
+    destruct p.
+    apply sq_path.
+    exact (concat_pV _ @ (concat_pV _)^).
+  Defined.
+
+  Definition diamond_v (a a' : A) {b b' : B} (p : b = b')
+    : Diamond a a' b b'.
+  Proof.
+    destruct p.
+    by apply sq_path.
+  Defined.
+
+  Lemma diamond_symm (a : A) (b : B)
+    : diamond_v a a 1 = diamond_h b b 1.
+  Proof.
+    unfold diamond_v, diamond_h.
+    symmetry; apply ap, concat_pV.
+  Defined.
+
+End Diamond.
+
+Definition diamond_twist {A : Type} {a a' : A} (p : a = a')
+  : DPath (fun x => Diamond a' x a x) p
+    (diamond_v a' a 1) (diamond_h a a' 1).
+Proof.
+  destruct p.
+  apply diamond_symm.
+Defined.
+
+(** * Functoriality of Join. *)
+Section FunctorJoin.
+
+  Definition functor_join {A B C D} (f : A -> C) (g : B -> D)
+    : Join A B -> Join C D.
+  Proof.
+    snrapply Join_rec.
+    1: exact (joinl o f).
+    1: exact (joinr o g).
+    intros a b.
+    apply jglue.
+  Defined.
+
+  Definition functor_join_beta_jglue {A B C D : Type} (f : A -> C) (g : B -> D)
+    (a : A) (b : B)
+    : ap (functor_join f g) (jglue a b) = jglue (f a) (g b)
+    := Join_rec_beta_jglue _ _ _ a b.
+
+  Definition functor_join_compose {A B C D E F}
+    (f : A -> C) (g : B -> D) (h : C -> E) (i : D -> F)
+    : functor_join (h o f) (i o g) == functor_join h i o functor_join f g.
+  Proof.
+    snrapply Join_ind_FlFr.
+    1,2: reflexivity.
+    intros a b.
+    simpl.
+    apply equiv_p1_1q.
+    lhs nrapply functor_join_beta_jglue; symmetry.
+    lhs nrapply (ap_compose (functor_join f g) _ (jglue a b)).
+    lhs nrefine (ap _ (functor_join_beta_jglue _ _ _ _)).
+    apply functor_join_beta_jglue.
+  Defined.
+
+  Definition functor_join_idmap {A B}
+    : functor_join idmap idmap == (idmap : Join A B -> Join A B).
+  Proof.
+    snrapply Join_ind_FlFr.
+    1,2: reflexivity.
+    intros a b.
+    simpl.
+    apply equiv_p1_1q.
+    lhs nrapply functor_join_beta_jglue.
+    symmetry; apply ap_idmap.
+  Defined.
+
+  Definition functor2_join {A B C D} {f f' : A -> C} {g g' : B -> D}
+    (h : f == f') (k : g == g')
+    : functor_join f g == functor_join f' g'.
+  Proof.
+    srapply Join_ind_FlFr.
+    - simpl; intros; apply ap, h.
+    - simpl; intros; apply ap, k.
+    - intros a b; cbn beta.
+      lhs nrapply (functor_join_beta_jglue _ _ _ _ @@ 1).
+      symmetry.
+      lhs nrapply (1 @@ functor_join_beta_jglue _ _ _ _).
+      apply join_natsq.
+  Defined.
+
+  Global Instance isequiv_functor_join {A B C D}
+    (f : A -> C) `{!IsEquiv f} (g : B -> D) `{!IsEquiv g}
+    : IsEquiv (functor_join f g).
+  Proof.
+    snrapply isequiv_adjointify.
+    - apply (functor_join f^-1 g^-1).
+    - etransitivity.
+      1: symmetry; apply functor_join_compose.
+      etransitivity.
+      1: exact (functor2_join (eisretr f) (eisretr g)).
+      apply functor_join_idmap.
+    - etransitivity.
+      1: symmetry; apply functor_join_compose.
+      etransitivity.
+      1: exact (functor2_join (eissect f) (eissect g)).
+      apply functor_join_idmap.
+  Defined.
+
+  Definition equiv_functor_join {A B C D} (f : A <~> C) (g : B <~> D)
+    : Join A B <~> Join C D := Build_Equiv _ _ (functor_join f g) _.
+
+End FunctorJoin.
+
+(** * We'll use the recursion equivalence above to prove the symmetry of Join, using the Yoneda lemma.  The idea is that [Join A B -> P] is equivalent (as a 0-groupoid) to [JoinRecData A B P], and the latter is very symmetrical by construction, which makes it easy to show that it is equivalent to [JoinRecData B A P].  Going back along the first equivalence gets us to [Join B A -> P].  These equivalences are natural in [P], so the symmetry equivalence follows from the Yoneda lemma.  This is mainly meant as a warmup to proving the associativity of the join. *)
+
+Section JoinSym.
+
+  Definition joinrecdata_sym (A B P : Type)
+    : joinrecdata_0gpd A B P $-> joinrecdata_0gpd B A P.
+  Proof.
+    snrapply Build_Morphism_0Gpd.
+    (* The map of types [JoinRecData A B P -> JoinRecData B A P]: *)
+    - intros [fl fr fg].
+      snrapply (Build_JoinRecData fr fl).
+      intros b a; exact (fg a b)^.
+    (* It respects the paths. *)
+    - apply Build_Is0Functor.
+      intros f g h; simpl.
+      snrapply Build_JoinRecPath; simpl.
+      1, 2: intros; apply h.
+      intros b a.
+      square_ind g h a b.
+      by interval_ind f a b.
+  Defined.
+
+  (** This map is its own inverse in the 1-category of 0-groupoids. *)
+  Definition joinrecdata_sym_inv (A B P : Type)
+    : joinrecdata_sym B A P $o joinrecdata_sym A B P $== Id _.
+  Proof.
+    intro f; simpl.
+    bundle_joinrecpath.
+    intros a b; simpl.
+    apply inv_V.
+  Defined.
+
+  (** We get the symmetry natural equivalence on [TriJoinRecData]. *)
+  Definition joinrecdata_sym_natequiv (A B : Type)
+    : NatEquiv (joinrecdata_0gpd_fun A B) (joinrecdata_0gpd_fun B A).
+  Proof.
+    snrapply Build_NatEquiv.
+    (* An equivalence of 0-groupoids for each [P]: *)
+    - intro P.
+      snrapply cate_adjointify.
+      1, 2: apply joinrecdata_sym.
+      1, 2: apply joinrecdata_sym_inv.
+    (* Naturality: *)
+    - intros P Q g f; simpl.
+      bundle_joinrecpath.
+      intros b a; simpl.
+      symmetry; apply ap_V.
+  Defined.
+
+  (** Combining with the recursion equivalence [join_rec_inv_natequiv] and its inverse gives the symmetry natural equivalence between the representable functors. *)
+  Definition joinrecdata_fun_sym (A B : Type)
+    : NatEquiv (opyon_0gpd (Join A B)) (opyon_0gpd (Join B A))
+    := natequiv_compose (join_rec_natequiv B A)
+        (natequiv_compose (joinrecdata_sym_natequiv A B) (join_rec_inv_natequiv A B)).
+
+  (** The Yoneda lemma for 0-groupoid valued functors therefore gives us an equivalence between the representing objects.  We mark this with a prime, since we'll use a homotopic map with a slightly simpler definition. *)
+  Definition equiv_join_sym' (A B : Type)
+    : Join A B <~> Join B A.
+  Proof.
+    rapply (opyon_equiv_0gpd (A:=Type)).
+    apply joinrecdata_fun_sym.
+  Defined.
+
+  (** It has the nice property that the underlying function of the inverse is again [equiv_join_sym'], with arguments permuted. *)
+  Local Definition equiv_join_sym_check1 (A B : Type)
+    : (equiv_join_sym' A B)^-1 = equiv_fun (equiv_join_sym' B A)
+    := idpath.
+
+  (** The definition we end up with is almost the same as the obvious one, but has an extra [ap idmap] in it. *)
+  Local Definition equiv_join_sym_check2 (A B : Type)
+    : equiv_fun (equiv_join_sym' A B) = Join_rec (fun a : A => joinr a) (fun b : B => joinl b)
+                                          (fun (a : A) (b : B) => (ap idmap (jglue b a))^)
+    := idpath.
+
+  (** The next two give the obvious definition. *)
+  Definition join_sym_recdata (A B : Type)
+    : JoinRecData A B (Join B A)
+    := Build_JoinRecData joinr joinl (fun a b => (jglue b a)^).
+
+  Definition join_sym (A B : Type)
+    : Join A B -> Join B A
+    := join_rec (join_sym_recdata A B).
+
+  Definition join_sym_beta_jglue {A B} (a : A) (b : B)
+    : ap (join_sym A B) (jglue a b) = (jglue b a)^
+    := Join_rec_beta_jglue _ _ _ _ _.
+
+  (** The obvious definition is homotopic to the definition via the Yoneda lemma. *)
+  Definition join_sym_homotopic (A B : Type)
+    : join_sym A B == equiv_join_sym' A B.
+  Proof.
+    symmetry.
+    (** Both sides are [join_rec] applied to [JoinRecData]: *)
+    rapply (fmap join_rec).
+    bundle_joinrecpath; intros; cbn.
+    refine (ap inverse _).
+    apply ap_idmap.
+  Defined.
+
+  (** Therefore the obvious definition is also an equivalence, and the inverse function can also be chosen to be [join_sym]. *)
+  Definition equiv_join_sym (A B : Type) : Join A B <~> Join B A
+    := equiv_homotopic_inverse (equiv_join_sym' A B)
+                              (join_sym_homotopic A B)
+                              (join_sym_homotopic B A).
+
+  (** It's also straightforward to directly prove that [join_sym] is an equivalence.  The above approach is meant to illustrate the Yoneda lemma.  In the case of [equiv_trijoin_twist], the Yoneda approach seems to be more straightforward. *)
+  Definition join_sym_inv A B : join_sym A B o join_sym B A == idmap.
+  Proof.
+    snrapply (Join_ind_FFlr (join_sym B A)).
+    - reflexivity.
+    - reflexivity.
+    - intros a b; cbn beta.
+      apply equiv_p1_1q.
+      refine (ap _ (join_rec_beta_jg _ a b) @ _); cbn.
+      refine (ap_V _ (jglue b a) @ _).
+      refine (ap inverse (join_rec_beta_jg _ b a) @ _).
+      apply inv_V.
+  Defined.
+
+  (** Finally, one can also prove that the join is symmetric using [pushout_sym] and [equiv_prod_symm], but this results in an equivalence whose inverse isn't of the same form. *)
+
+  Definition join_sym_nat {A B A' B'} (f : A -> A') (g : B -> B')
+    : join_sym A' B' o functor_join f g == functor_join g f o join_sym A B.
+  Proof.
+    snrapply Join_ind_FlFr.
+    1, 2: reflexivity.
+    intros a b; cbn beta.
+    apply equiv_p1_1q.
+    lhs nrefine (ap_compose' (functor_join f g) _ (jglue a b)).
+    lhs nrefine (ap _ (functor_join_beta_jglue _ _ _ _)).
+    lhs nrapply join_sym_beta_jglue.
+    symmetry.
+    lhs nrefine (ap_compose' (join_sym A B) _ (jglue a b)).
+    lhs nrefine (ap _ (join_sym_beta_jglue a b)).
+    refine (ap_V _ (jglue b a) @ ap inverse _).
+    apply functor_join_beta_jglue.
+  Defined.
+
+End JoinSym.
+
+(** Relationship to truncation levels and connectedness. *)
+Section JoinTrunc.
+
+  (** Joining with a contractible type produces a contractible type *)
+  Global Instance contr_join A B `{Contr A} : Contr (Join A B).
+  Proof.
+    exists (joinl (center A)).
+    snrapply Join_ind.
+    - intros a; apply ap, contr.
+    - intros b; apply jglue.
+    - intros a b; cbn.
+      lhs nrapply transport_paths_r.
+      apply triangle_h'.
+  Defined.
+
+  (** The join of hprops is an hprop *)
+  Global Instance ishprop_join `{Funext} A B `{IsHProp A} `{IsHProp B} : IsHProp (Join A B).
+  Proof.
+    apply hprop_inhabited_contr.
+    snrapply Join_rec.
+    - intros a; apply contr_join.
+      exact (contr_inhabited_hprop A a).
+    - intros b; refine (contr_equiv (Join B A) (equiv_join_sym B A)).
+      apply contr_join.
+      exact (contr_inhabited_hprop B b).
+    (* The two proofs of contractibility are equal because [Contr] is an [HProp].  This uses [Funext]. *)
+    - intros a b; apply path_ishprop.
+  Defined.
+
+  Lemma equiv_into_hprop `{Funext} {A B P : Type} `{IsHProp P} (f : A -> P)
+    : (Join A B -> P) <~> (B -> P).
+  Proof.
+    apply equiv_iff_hprop.
+    1: exact (fun f => f o joinr).
+    intros g.
+    snrapply Join_rec.
+    1,2: assumption.
+    intros a b.
+    apply path_ishprop.
+  Defined.
+
+  (** And coincides with their disjunction *)
+  Definition equiv_join_hor `{Funext} A B `{IsHProp A} `{IsHProp B}
+    : Join A B <~> hor A B.
+  Proof.
+    apply equiv_iff_hprop.
+    - exact (Join_rec (fun a => tr (inl a)) (fun b => tr (inr b)) (fun _ _ => path_ishprop _ _)).
+    - apply Trunc_rec, push.
+  Defined.
+
+  (** Joins add connectivity *)
+  Global Instance isconnected_join `{Univalence} {m n : trunc_index}
+         (A B : Type) `{IsConnected m A} `{IsConnected n B}
+    : IsConnected (m +2+ n) (Join A B).
+  Proof.
+    apply isconnected_from_elim; intros C ? k.
+    pose @istrunc_inO_tr.
+    pose proof (istrunc_extension_along_conn
+                  (fun b:B => tt) (fun _ => C) (k o joinr)).
+    unfold ExtensionAlong in *.
+    transparent assert (f : (A -> {s : Unit -> C &
+                                   forall x, s tt = k (joinr x)})).
+    { intros a; exists (fun _ => k (joinl a)); intros b.
+      exact (ap k (jglue a b)). }
+    assert (h := isconnected_elim
+                   m {s : Unit -> C & forall x : B, s tt = k (joinr x)} f).
+    unfold NullHomotopy in *; destruct h as [[c g] h].
+    exists (c tt).
+    snrapply Join_ind.
+    - intros a; cbn. exact (ap10 (h a)..1 tt).
+    - intros b; cbn. exact ((g b)^).
+    - intros a b.
+      rewrite transport_paths_FlFr, ap_const, concat_p1; cbn.
+      subst f; set (ha := h a); clearbody ha; clear h;
+      assert (ha2 := ha..2); set (ha1 := ha..1) in *;
+      clearbody ha1; clear ha; cbn in *.
+      rewrite <- (inv_V (ap10 ha1 tt)).
+      rewrite <- inv_pp.
+      apply inverse2.
+      refine (_ @ apD10 ha2 b); clear ha2.
+      rewrite transport_forall_constant, transport_paths_FlFr.
+      rewrite ap_const, concat_p1.
+      reflexivity.
+  Defined.
+
+End JoinTrunc.
+
+(** Iterated Join powers of a type. *)
+Section JoinPower.
+
+  (** The join of n.+1 copies of a type. *)
+  Fixpoint Join_power (A : Type) (n : nat) : Type :=
+    match n with
+    | 0%nat => A
+    | m.+1%nat => Join A (Join_power A m)
+    end.
+
+End JoinPower.
diff --git a/theories/Homotopy/Join/JoinAssoc.v b/theories/Homotopy/Join/JoinAssoc.v
new file mode 100644
index 00000000000..780c650399a
--- /dev/null
+++ b/theories/Homotopy/Join/JoinAssoc.v
@@ -0,0 +1,149 @@
+Require Import Basics Types WildCat Join.Core Join.TriJoin.
+
+(** * We use the recursion principle for the triple join (from TriJoin.v) to prove the associativity of Join.  We'll use the common technique of combining symmetry and a twist equivalence.  Temporarily writing * for Join, symmetry says that [A * B <~> B * A] and the twist says that [A * (B * C) <~> B * (A * C)].  From these we get a composite equivalence [A * (B * C) <~> A * (C * B) <~> C * (A * B) <~> (A * B) * C].  One advantage of this approach is that both symmetry and the twist are their own inverses, so there are fewer maps to define and fewer composites to prove are homotopic to the identity. Symmetry is proved in Join/Core.v. *)
+
+(** * We prove the twist equivalence [TriJoin A B C <~> TriJoin B A C], using the Yoneda lemma.  The idea is that [TriJoin A B C -> P] is equivalent (as a 0-groupoid) to [TriJoinRecData A B C P], and the latter is very symmetrical by construction, which makes it easy to show that it is equivalent to [TriJoinRecData B A C P].  Going back along the first equivalence gets us to [TriJoin B A C -> P].  These equivalences are natural in [P], so the twist equivalence follows from the Yoneda lemma. *)
+
+(** First we define a map of 0-groupoids that will underlie the natural equivalence. *)
+Definition trijoinrecdata_twist (A B C P : Type)
+  : trijoinrecdata_0gpd A B C P $-> trijoinrecdata_0gpd B A C P.
+Proof.
+  snrapply Build_Morphism_0Gpd.
+  (* The map of types [TriJoinRecData A B C P -> TriJoinRecData B A C P]: *)
+  - cbn.
+    intros [f1 f2 f3 f12 f13 f23 f123].
+    snrapply (Build_TriJoinRecData f2 f1 f3).
+    + intros b a; exact (f12 a b)^.
+    + exact f23.
+    + exact f13.
+    + intros a b c; cbn beta.
+      apply moveR_Vp.
+      symmetry; apply f123.
+  (* It respects the paths. *)
+  - apply Build_Is0Functor.
+    intros f g h; cbn in *.
+    snrapply Build_TriJoinRecPath; intros; simpl.
+    1, 2, 3, 5, 6: apply h.
+    + cbn zeta.
+      prism_ind_two g h b a _X_; cbn beta.
+      apply concat_p1_1p.
+    + cbn beta zeta.
+      prism_ind g h b a c; cbn beta.
+      by triangle_ind f b a c.
+Defined.
+
+(** This map is its own inverse in the 1-category of 0-groupoids. *)
+Definition trijoinrecdata_twist_inv (A B C P : Type)
+  : trijoinrecdata_twist B A C P $o trijoinrecdata_twist A B C P $== Id _.
+Proof.
+  intro f; simpl.
+  bundle_trijoinrecpath.
+  all: intros; cbn.
+  - apply inv_V.
+  - reflexivity.
+  - reflexivity.
+  - by triangle_ind f a b c.
+Defined.
+
+(** We get the twist natural equivalence on [TriJoinRecData]. *)
+Definition trijoinrecdata_twist_natequiv (A B C : Type)
+  : NatEquiv (trijoinrecdata_0gpd_fun A B C) (trijoinrecdata_0gpd_fun B A C).
+Proof.
+  snrapply Build_NatEquiv.
+  (* An equivalence of 0-groupoids for each [P]: *)
+  - intro P.
+    snrapply cate_adjointify.
+    1, 2: apply trijoinrecdata_twist.
+    1, 2: apply trijoinrecdata_twist_inv.
+  (* Naturality: *)
+  - intros P Q g f; simpl.
+    bundle_trijoinrecpath.
+    all: intros; cbn.
+    + symmetry; apply ap_V.
+    + reflexivity.
+    + reflexivity.
+    + by triangle_ind f b a c.
+Defined.
+
+(** Combining with the recursion equivalence [trijoin_rec_inv_natequiv] and its inverse gives the twist natural equivalence between the representable functors. *)
+Definition trijoinrecdata_fun_twist (A B C : Type)
+  : NatEquiv (opyon_0gpd (TriJoin A B C)) (opyon_0gpd (TriJoin B A C))
+  := natequiv_compose (trijoin_rec_natequiv B A C)
+      (natequiv_compose (trijoinrecdata_twist_natequiv A B C) (trijoin_rec_inv_natequiv A B C)).
+
+(** The Yoneda lemma for 0-groupoid valued functors therefore gives us an equivalence between the representing objects.  We mark this with a prime, since we'll use a homotopic map with a slightly simpler definition. *)
+Definition equiv_trijoin_twist' (A B C : Type)
+  : TriJoin A B C <~> TriJoin B A C.
+Proof.
+  rapply (opyon_equiv_0gpd (A:=Type)).
+  apply trijoinrecdata_fun_twist.
+Defined.
+
+(** It has the nice property that the underlying function of the inverse is again [equiv_trijoin_twist'], with arguments permuted. *)
+Local Definition trijoin_twist_check1 (A B C : Type)
+  : (equiv_trijoin_twist' A B C)^-1 = equiv_fun (equiv_trijoin_twist' B A C)
+  := idpath.
+
+(** The definition we end up with is almost the same as the obvious one, but has some extra [ap idmap]s in it. *)
+Local Definition twijoin_twist_check2 (A B C : Type)
+  : equiv_fun (equiv_trijoin_twist' A B C)
+    = trijoin_rec {| j1 := join2; j2 := join1; j3 := join3;
+      j12 := fun (b : A) (a : B) => (ap idmap (join12 a b))^;
+      j13 := fun (b : A) (c : C) => ap idmap (join23 b c);
+      j23 := fun (a : B) (c : C) => ap idmap (join13 a c);
+      j123 := fun (a : A) (b : B) (c : C) =>
+               moveR_Vp _ _ _ (ap_triangle idmap (join123 b a c))^ |}
+  := idpath.
+
+(** The next two give the obvious definition. *)
+Definition trijoin_twist_recdata (A B C : Type)
+  : TriJoinRecData A B C (TriJoin B A C)
+  := Build_TriJoinRecData join2 join1 join3
+      (fun a b => (join12 b a)^) join23 join13
+      (fun a b c => moveR_Vp _ _ _ (join123 b a c)^).
+
+Definition trijoin_twist (A B C : Type)
+  : TriJoin A B C -> TriJoin B A C
+  := trijoin_rec (trijoin_twist_recdata A B C).
+
+(** As an aside, note that [trijoin_twist] computes nicely on [joinr]. *)
+Local Definition trijoin_twist_joinr (A B C : Type)
+  : trijoin_twist A B C o joinr = functor_join idmap joinr
+  := idpath.
+
+(** The obvious definition is homotopic to the definition via the Yoneda lemma. *)
+Definition trijoin_twist_homotopic (A B C : Type)
+  : trijoin_twist A B C == equiv_trijoin_twist' A B C.
+Proof.
+  symmetry.
+  (** Both sides are [trijoin_rec] applied to [TriJoinRecData]: *)
+  rapply (fmap trijoin_rec).
+  bundle_trijoinrecpath; intros; cbn.
+  1: refine (ap inverse _).
+  1, 2, 3: apply ap_idmap.
+  generalize (join123 b a c).
+  generalize (join23 (A:=B) a c).
+  generalize (join13 (B:=A) b c).
+  generalize (join12 (C:=C) b a).
+  generalize (join3 (A:=B) (B:=A) c).
+  generalize (join2 (A:=B) (C:=C) a).
+  generalize (join1 (B:=A) (C:=C) b).
+  intros k1 k2 k3 k12 k13 k23 k123.
+  induction k12, k23, k123.
+  reflexivity.
+Defined.
+
+(** Therefore the obvious definition is also an equivalence, and the inverse function can also be chosen to be [trijoin_twist]. *)
+Definition equiv_trijoin_twist (A B C : Type)
+  : TriJoin A B C <~> TriJoin B A C
+  := equiv_homotopic_inverse (equiv_trijoin_twist' A B C)
+                            (trijoin_twist_homotopic A B C)
+                            (trijoin_twist_homotopic B A C).
+
+(** Finally, we get that Join is associative. *)
+Definition join_assoc A B C : Join A (Join B C) <~> Join (Join A B) C.
+Proof.
+  refine (_ oE equiv_functor_join equiv_idmap (equiv_join_sym B C)).
+  refine (_ oE equiv_trijoin_twist _ _ _).
+  apply equiv_join_sym.
+Defined.
diff --git a/theories/Homotopy/Join/TriJoin.v b/theories/Homotopy/Join/TriJoin.v
new file mode 100644
index 00000000000..45a683d0acb
--- /dev/null
+++ b/theories/Homotopy/Join/TriJoin.v
@@ -0,0 +1,668 @@
+Require Import Basics Types WildCat Join.Core.
+
+(** * We show that the iterated join satisfies symmetrical induction and recursion principles and prove that the recursion principle gives an equivalence of 0-groupoids.  We use this in JoinAssoc.v to prove that the join is associative.  Our approach parallels what is done in the two-variable case in Join/Core.v, especially starting with [TriJoinRecData] here and [JoinRecData] there.  That case is much simpler, so should be read first. *)
+
+Section TriJoinStructure.
+  Context {A B C : Type}.
+
+  Definition TriJoin := Join A (Join B C).
+
+  Definition join1 : A -> TriJoin := joinl.
+  Definition join2 : B -> TriJoin := fun b => (joinr (joinl b)).
+  Definition join3 : C -> TriJoin := fun c => (joinr (joinr c)).
+  Definition join12 : forall a b, join1 a = join2 b := fun a b => jglue a (joinl b).
+  Definition join13 : forall a c, join1 a = join3 c := fun a c => jglue a (joinr c).
+  Definition join23 : forall b c, join2 b = join3 c := fun b c => ap joinr (jglue b c).
+  Definition join123 : forall a b c, join12 a b @ join23 b c = join13 a c := fun a b c => triangle_v' a (jglue b c).
+End TriJoinStructure.
+
+Arguments TriJoin A B C : clear implicits.
+
+(** * The goal of the next few results is to define [ap_trijoin] and [ap_trijoin_transport]. *)
+
+(** Functions send triangles to triangles. *)
+Definition ap_triangle {X Y} (f : X -> Y)
+  {a b c : X} {ab : a = b} {bc : b = c} {ac : a = c} (abc : ab @ bc = ac)
+  : ap f ab @ ap f bc = ap f ac
+  := (ap_pp f ab bc)^ @ ap (ap f) abc.
+
+(** This general result abstracts away the situation where [J] is [TriJoin A B C], [a] is [joinl a'] for some [a'], [jr] is [joinr : Join B C -> J], [jg] is [fun w => jglue a' w], and [p] is [jglue b c].  By working in this generality, we can do induction on [p].  This also allows us to inline the proof of [triangle_v']. *)
+Definition ap_trijoin_general {J W P : Type} (f : J -> P)
+  (a : J) (jr : W -> J) (jg : forall w, a = jr w)
+  {b c : W} (p : b = c)
+  : ap f (jg b) @ ap f (ap jr p) = ap f (jg c).
+Proof.
+  apply ap_triangle.
+  induction p.
+  apply concat_p1.
+Defined.
+
+(** Functions send the canonical triangles in triple joins to triangles. *)
+Definition ap_trijoin {A B C P : Type} (f : TriJoin A B C -> P)
+  (a : A) (b : B) (c : C)
+  : ap f (join12 a b) @ ap f (join23 b c) = ap f (join13 a c).
+Proof.
+  nrapply ap_trijoin_general.
+Defined.
+
+Definition ap_trijoin_general_transport {J W P : Type} (f : J -> P)
+  (a : J) (jr : W -> J) (jg : forall w, a = jr w)
+  {b c : W} (p : b = c)
+  : ap_trijoin_general f a jr jg p
+    = (1 @@ ap_compose _ f _)^ @ (transport_paths_Fr _ _)^ @ apD (fun x => ap f (jg x)) p.
+Proof.
+  induction p.
+  unfold ap_trijoin_general; simpl.
+  induction (jg b).
+  reflexivity.
+Defined.
+
+Definition ap_trijoin_transport {A B C P : Type} (f : TriJoin A B C -> P)
+  (a : A) (b : B) (c : C)
+  : ap_trijoin f a b c
+    = (1 @@ ap_compose _ f _)^ @ (transport_paths_Fr _ _)^ @ apD (fun x => ap f (jglue a x)) (jglue b c).
+Proof.
+  nrapply ap_trijoin_general_transport.
+Defined.
+
+(** * Now we prove the induction principle for the triple join. *)
+
+(** A lemma that handles the path algebra in the final step. *)
+Local Definition trijoin_ind_helper {A BC : Type} (P : Join A BC -> Type)
+  (a : A) (b c : BC) (bc : b = c)
+  (j1' : P (joinl a)) (j2' : P (joinr b)) (j3' : P (joinr c))
+  (j12' : jglue a b # j1' = j2') (j13' : jglue a c # j1' = j3') (j23' : (ap joinr bc) # j2' = j3')
+  (j123' : transport_pp _ (jglue a b) (ap joinr bc) j1' @ ap (transport _ (ap joinr bc)) j12' @ j23'
+           = transport2 _ (triangle_v' a bc) _ @ j13')
+  : ((apD (fun x : BC => transport P (jglue a x) j1') bc)^
+       @ ap (transport (fun x : BC => P (joinr x)) bc) j12')
+      @ ((transport_compose P joinr bc j2') @ j23') = j13'.
+Proof.
+  induction bc; simpl.
+  rewrite transport_pp_1 in j123'.
+  cbn in *.
+  unfold transport; unfold transport in j123'.
+  rewrite ap_idmap; rewrite ap_idmap in j123'.
+  rewrite concat_pp_p in j123'.
+  apply cancelL in j123'.
+  rewrite 2 concat_1p.
+  exact j123'.
+Qed.
+
+(** An induction principle for the triple join. Note that the hypotheses are phrased completely in terms of the "constructors" of [TriJoin A B C]. *)
+Definition trijoin_ind (A B C : Type) (P : TriJoin A B C -> Type)
+  (join1' : forall a, P (join1 a))
+  (join2' : forall b, P (join2 b))
+  (join3' : forall c, P (join3 c))
+  (join12' : forall a b, join12 a b # join1' a = join2' b)
+  (join13' : forall a c, join13 a c # join1' a = join3' c)
+  (join23' : forall b c, join23 b c # join2' b = join3' c)
+  (join123' : forall a b c, transport_pp _ (join12 a b) (join23 b c) (join1' a)
+                         @ ap (transport _ (join23 b c)) (join12' a b) @ join23' b c
+                       = transport2 _ (join123 a b c) _ @ join13' a c)
+  : forall x, P x.
+Proof.
+  snrapply Join_ind.
+  - exact join1'.
+  - snrapply Join_ind.
+    + exact join2'.
+    + exact join3'.
+    + intros b c.
+      lhs rapply (transport_compose P).
+      apply join23'.
+  - intro a.
+    snrapply Join_ind.
+    + simpl. exact (join12' a).
+    + simpl. exact (join13' a).
+    + intros b c; cbn beta zeta.
+      lhs nrapply (transport_paths_FlFr_D (jglue b c)).
+      lhs nrapply (1 @@ _).
+      1: nrapply Join_ind_beta_jglue.
+      apply trijoin_ind_helper, join123'.
+Defined.
+
+(** * We now state the recursion principle and prove many things about it. *)
+
+(** We'll bundle up the arguments into a record. *)
+Record TriJoinRecData {A B C P : Type} := {
+    j1 : A -> P;
+    j2 : B -> P;
+    j3 : C -> P;
+    j12 : forall a b, j1 a = j2 b;
+    j13 : forall a c, j1 a = j3 c;
+    j23 : forall b c, j2 b = j3 c;
+    j123 : forall a b c, j12 a b @ j23 b c = j13 a c;
+  }.
+
+Arguments TriJoinRecData : clear implicits.
+Arguments Build_TriJoinRecData {A B C P}%type_scope (j1 j2 j3 j12 j13 j23 j123)%function_scope.
+
+Definition trijoin_rec {A B C P : Type} (f : TriJoinRecData A B C P)
+  : TriJoin A B C -> P.
+Proof.
+  snrapply Join_rec.
+  - exact (j1 f).
+  - snrapply Join_rec.
+    + exact (j2 f).
+    + exact (j3 f).
+    + exact (j23 f).
+  - intro a.
+    snrapply Join_ind; cbn beta.
+    + exact (j12 f a).
+    + exact (j13 f a).
+    + intros b c.
+      lhs nrapply transport_paths_Fr.
+      exact (1 @@ Join_rec_beta_jglue _ _ _ _ _ @ j123 f a b c).
+Defined.
+
+(** Beta rules for the recursion principle. *)
+Definition trijoin_rec_beta_join12 {A B C P : Type} (f : TriJoinRecData A B C P) (a : A) (b : B)
+  : ap (trijoin_rec f) (join12 a b) = j12 f a b
+  := Join_rec_beta_jglue _ _ _ _ _.
+
+Definition trijoin_rec_beta_join13 {A B C P : Type} (f : TriJoinRecData A B C P) (a : A) (c : C)
+  : ap (trijoin_rec f) (join13 a c) = j13 f a c
+  := Join_rec_beta_jglue _ _ _ _ _.
+
+Definition trijoin_rec_beta_join23 {A B C P : Type} (f : TriJoinRecData A B C P) (b : B) (c : C)
+  : ap (trijoin_rec f) (join23 b c) = j23 f b c.
+Proof.
+  unfold trijoin_rec, join23.
+  lhs_V nrapply (ap_compose joinr); simpl.
+  apply Join_rec_beta_jglue.
+Defined.
+
+Local Lemma trijoin_rec_beta_join123_helper {A : Type} {x y z : A}
+  {u0 u1 : x = y} {p0 p1 r1 : y = z} {q0 s1 t1 : x = z}
+  (p : p0 = p1) (q : q0 = u0 @ p0) (r : p0 = r1)
+  (s : u1 @ r1 = s1) (t : s1 = t1) (u : u0 = u1)
+  : ((1 @@ p)^ @ q^) @ (((q @ (u @@ 1)) @ ((1 @@ r) @ s)) @ t)
+    = ((u @@ (p^ @ r)) @ s) @ t.
+Proof.
+  induction u, t, s, r, p.
+  revert q0 q; by apply paths_ind_r.
+Defined.
+
+Definition trijoin_rec_beta_join123 {A B C P : Type} (f : TriJoinRecData A B C P)
+  (a : A) (b : B) (c : C)
+  : ap_trijoin (trijoin_rec f) a b c
+    = (trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c)
+        @ j123 f a b c @ (trijoin_rec_beta_join13 f a c)^.
+Proof.
+  (* Expand the LHS: *)
+  lhs nrapply ap_trijoin_transport.
+  rewrite (apD_homotopic (Join_rec_beta_jglue _ _ _ _) (jglue b c)).
+  rewrite Join_ind_beta_jglue.
+  (* Change [ap (transport __) _] on LHS. *)
+  rewrite (concat_p_pp _ (transport_paths_Fr (jglue b c) (j12 f a b)) _).
+  rewrite (concat_Ap (transport_paths_Fr (jglue b c))).
+  (* [trijoin_rec_beta_join23] expands to something of the form [p^ @ r], so that's what is in the lemma.  One can unfold it to see this, but the [Qed] is a bit faster without this.
+  unfold trijoin_rec_beta_join23. *)
+  (* Note that one of the [ap]s on the LHS computes to [u @@ 1], so that's what is in the lemma: *)
+  (* change (ap (fun q => q @ ?x) ?u) with (u @@ @idpath _ x). *)
+  (* Everything that remains is pure path algebra. *)
+  nrapply trijoin_rec_beta_join123_helper.
+Qed.
+
+(** * We're next going to define a map in the other direction.  We do it via showing that [TriJoinRecData] is a 0-coherent 1-functor to [Type]. We'll later show that it is a 1-functor to 0-groupoids. *)
+Definition trijoinrecdata_fun {A B C P Q : Type} (g : P -> Q) (f : TriJoinRecData A B C P)
+  : TriJoinRecData A B C Q.
+Proof.
+  snrapply Build_TriJoinRecData.
+  - exact (g o j1 f).
+  - exact (g o j2 f).
+  - exact (g o j3 f).
+  - exact (fun a b => ap g (j12 f a b)).
+  - exact (fun a c => ap g (j13 f a c)).
+  - exact (fun b c => ap g (j23 f b c)).
+  - intros a b c; cbn beta.
+    exact (ap_triangle g (j123 f a b c)).
+  (* The last four goals above can also be handled by the induction tactics below, but it's useful to be concrete. *)
+Defined.
+
+(** The triple join itself has canonical [TriJoinRecData]. *)
+Definition trijoinrecdata_trijoin (A B C : Type)
+  : TriJoinRecData A B C (Join A (Join B C))
+  := Build_TriJoinRecData join1 join2 join3 join12 join13 join23 join123.
+
+(** Combining these gives a function going in the opposite direction to [trijoin_rec]. *)
+Definition trijoin_rec_inv {A B C P : Type} (f : TriJoin A B C -> P)
+  : TriJoinRecData A B C P
+  := trijoinrecdata_fun f (trijoinrecdata_trijoin A B C).
+
+(** * Under [Funext], [trijoin_rec] and [trijoin_rec_inv] should be inverse equivalences.  We'll avoid [Funext] and show that they are equivalences of 0-groupoids, where we choose the path structures carefully.  We begin by describing a notion of paths between elements of [TriJoinRecData A B C P]. *)
+
+(** The type of fillers for a triangular prism with five 2d faces [abc], [abc'], [k12], [k13], [k23]. *)
+Definition prism {P : Type}
+  {a b c : P} {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac)
+  {a' b' c' : P} {ab' : a' = b'} {ac' : a' = c'} {bc' : b' = c'} (abc' : ab' @ bc' = ac')
+  {k1 : a = a'} {k2 : b = b'} {k3 : c = c'}
+  (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc')
+  := concat_p_pp _ _ _ @ whiskerR abc k3 @ k13
+    = whiskerL ab k23
+    @ concat_p_pp _ _ _ @ whiskerR k12 bc'
+    @ concat_pp_p _ _ _ @ whiskerL k1 abc'.
+
+(** The "identity" filler is slightly non-trivial, because the fillers for the squares, e.g. [ab @ 1 = 1 @ ab], must be non-trivial. *)
+Definition prism_id {P : Type}
+  {a b c : P} {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac)
+  : prism abc abc (equiv_p1_1q idpath) (equiv_p1_1q idpath) (equiv_p1_1q idpath).
+Proof.
+  induction ab, bc, abc; simpl.
+  reflexivity.
+Defined.
+
+(** The paths between elements of [TriJoinRecData A B C P].  Under [Funext], this type will be equivalent to the identity type.  But without [Funext], this definition will be more useful. *)
+Record TriJoinRecPath {A B C P : Type} {f g : TriJoinRecData A B C P} := {
+    h1 : forall a, j1 f a = j1 g a;
+    h2 : forall b, j2 f b = j2 g b;
+    h3 : forall c, j3 f c = j3 g c;
+    h12 : forall a b, j12 f a b @ h2 b = h1 a @ j12 g a b;
+    h13 : forall a c, j13 f a c @ h3 c = h1 a @ j13 g a c;
+    h23 : forall b c, j23 f b c @ h3 c = h2 b @ j23 g b c;
+    h123 : forall a b c, prism (j123 f a b c) (j123 g a b c) (h12 a b) (h13 a c) (h23 b c);
+  }.
+
+Arguments TriJoinRecPath {A B C P} f g.
+
+(** We also define data for [trijoin_rec] that unbundles the first three components.  This lets us talk about paths between two such when the first three components are definitionally equal. This is a common special case, and this set-up greatly simplifies a lot of path algebra in later proofs. *)
+Record TriJoinRecData' {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P} := {
+    j12' : forall a b, j1' a = j2' b;
+    j13' : forall a c, j1' a = j3' c;
+    j23' : forall b c, j2' b = j3' c;
+    j123' : forall a b c, j12' a b @ j23' b c = j13' a c;
+  }.
+
+Arguments TriJoinRecData' {A B C P} j1' j2' j3'.
+Arguments Build_TriJoinRecData' {A B C P}%type_scope
+  (j1' j2' j3' j12' j13' j23' j123')%function_scope.
+
+Definition prism' {P : Type} {a b c : P}
+  {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac)
+  {ab' : a = b} {ac' : a = c} {bc' : b = c} (abc' : ab' @ bc' = ac')
+  (k12 : ab = ab') (k13 : ac = ac') (k23 : bc = bc')
+  := abc @ k13 = (k12 @@ k23) @ abc'.
+
+Record TriJoinRecPath' {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P}
+  {f g : TriJoinRecData' j1' j2' j3'} := {
+    h12' : forall a b, j12' f a b = j12' g a b;
+    h13' : forall a c, j13' f a c = j13' g a c;
+    h23' : forall b c, j23' f b c = j23' g b c;
+    h123' : forall a b c, prism' (j123' f a b c) (j123' g a b c) (h12' a b) (h13' a c) (h23' b c);
+  }.
+
+Arguments TriJoinRecPath' {A B C P} {j1' j2' j3'} f g.
+
+(** * We can bundle and unbundle these types of data.  For unbundling, we just handle [TriJoinRecData] for now. *)
+
+Definition bundle_trijoinrecdata {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P}
+  (f : TriJoinRecData' j1' j2' j3')
+  : TriJoinRecData A B C P
+  := Build_TriJoinRecData j1' j2' j3' (j12' f) (j13' f) (j23' f) (j123' f).
+
+Definition unbundle_trijoinrecdata {A B C P : Type} (f : TriJoinRecData A B C P)
+  : TriJoinRecData' (j1 f) (j2 f) (j3 f)
+  := Build_TriJoinRecData' (j1 f) (j2 f) (j3 f) (j12 f) (j13 f) (j23 f) (j123 f).
+
+(** The proof by induction that is easily available to us here is what saves work in more complicated contexts. *)
+Definition bundle_prism {P : Type} {a b c : P}
+  {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac)
+  {ab' : a = b} {ac' : a = c} {bc' : b = c} (abc' : ab' @ bc' = ac')
+  (k12 : ab = ab') (k13 : ac = ac') (k23 : bc = bc')
+  (k123 : prism' abc abc' k12 k13 k23)
+  : prism abc abc' (equiv_p1_1q k12) (equiv_p1_1q k13) (equiv_p1_1q k23).
+Proof.
+  induction ab.
+  induction bc.
+  induction abc.
+  induction k12.
+  induction k23.
+  induction k13.
+  unfold prism' in k123.
+  induction (moveR_Vp _ _ _ k123); clear k123.
+  simpl.
+  reflexivity.
+Defined.
+
+Definition bundle_trijoinrecpath {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P}
+  {f g : TriJoinRecData' j1' j2' j3'} (h : TriJoinRecPath' f g)
+  : TriJoinRecPath (bundle_trijoinrecdata f) (bundle_trijoinrecdata g).
+Proof.
+  snrapply Build_TriJoinRecPath.
+  1, 2, 3: reflexivity.
+  1, 2, 3: intros; apply equiv_p1_1q.
+  - apply (h12' h).
+  - apply (h13' h).
+  - apply (h23' h).
+  - cbn beta zeta.
+    intros a b c.
+    apply bundle_prism, (h123' h).
+Defined.
+
+(** A tactic that helps us apply the previous result. *)
+Ltac bundle_trijoinrecpath :=
+  hnf;
+  match goal with |- TriJoinRecPath ?F ?G =>
+    refine (bundle_trijoinrecpath (f:=unbundle_trijoinrecdata F)
+                                  (g:=unbundle_trijoinrecdata G) _) end;
+  snrapply Build_TriJoinRecPath'.
+
+(** Using these paths, we can restate the beta rule for [trijoin_rec].  The statement using [TriJoinRecPath'] typechecks only because [trijoin_rec] computes definitionally on the path constructors. *)
+Definition trijoin_rec_beta' {A B C P : Type} (f : TriJoinRecData A B C P)
+  : TriJoinRecPath' (unbundle_trijoinrecdata (trijoin_rec_inv (trijoin_rec f)))
+                    (unbundle_trijoinrecdata f).
+Proof.
+  snrapply Build_TriJoinRecPath'; cbn.
+  - apply trijoin_rec_beta_join12.
+  - apply trijoin_rec_beta_join13.
+  - apply trijoin_rec_beta_join23.
+  - intros a b c.
+    unfold prism'.
+    apply moveR_pM.
+    nrapply trijoin_rec_beta_join123.
+Defined.
+
+(** We can upgrade this to an unprimed path. This says that [trijoin_rec_inv] is split surjective. *)
+Definition trijoin_rec_beta {A B C P : Type} (f : TriJoinRecData A B C P)
+  : TriJoinRecPath (trijoin_rec_inv (trijoin_rec f)) f
+  := bundle_trijoinrecpath (trijoin_rec_beta' f).
+
+(** * Next we show that [trijoin_rec_inv] is an injective map between 0-groupoids. *)
+
+(** We begin with a general purpose lemma. *)
+Definition triangle_ind {P : Type} (a : P)
+  (Q : forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c) (abc : ab @ bc = ac), Type)
+  (s : Q a a idpath idpath idpath idpath)
+  : forall b c ab ac bc abc, Q b c ab ac bc abc.
+Proof.
+  intros.
+  induction ab.
+  induction bc.
+  induction abc.
+  apply s.
+Defined.
+
+(** This lemma handles the path algebra in the last goal of the next result. *)
+Local Definition isinj_trijoin_rec_inv_helper {J P : Type} {f g : J -> P}
+  {a b c : J} {ab : a = b} {ac : a = c} {bc : b = c} {abc : ab @ bc = ac}
+  {H1 : f a = g a} {H2 : f b = g b} {H3 : f c = g c}
+  {H12 : ap f ab @ H2 = H1 @ ap g ab}
+  {H13 : ap f ac @ H3 = H1 @ ap g ac}
+  {H23 : ap f bc @ H3 = H2 @ ap g bc}
+  (H123 : prism (ap_triangle f abc) (ap_triangle g abc) H12 H13 H23)
+  : (transport_pp (fun x => f x = g x) ab bc H1 @ ap (transport (fun x => f x = g x) bc)
+       (transport_paths_FlFr' ab H1 H2 H12)) @ transport_paths_FlFr' bc H2 H3 H23
+    = transport2 (fun x => f x = g x) abc H1 @ transport_paths_FlFr' ac H1 H3 H13.
+Proof.
+  revert b c ab ac bc abc H2 H3 H12 H13 H23 H123.
+  nrapply triangle_ind; cbn.
+  unfold ap_triangle, transport_paths_FlFr', transport; cbn -[concat_pp_p].
+  generalize dependent (f a); intro fa; clear f.
+  generalize dependent (g a); intro ga; clear g a.
+  intros H1 H2 H3 H12 H13 H23.
+  rewrite ap_idmap.
+  revert H12; equiv_intro (equiv_1p_q1 (p:=H2) (q:=H1)) H12'; induction H12'.
+  revert H13; equiv_intro (equiv_1p_q1 (p:=H3) (q:=H2)) H13'; induction H13'.
+  induction H3.
+  intro H123.
+  unfold prism in H123.
+  rewrite whiskerL_1p_1 in H123.
+  cbn in *.
+  rewrite ! concat_p1 in H123.
+  induction H123.
+  reflexivity.
+Qed.
+
+(** [trijoin_rec_inv] is essentially injective, as a map between 0-groupoids. *)
+Definition isinj_trijoin_rec_inv {A B C P : Type} {f g : TriJoin A B C -> P}
+  (h : TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g))
+  : f == g.
+Proof.
+  snrapply trijoin_ind.
+  1: apply (h1 h).
+  1: apply (h2 h).
+  1: apply (h3 h).
+  1, 2, 3: intros; nrapply transport_paths_FlFr'.
+  1: apply (h12 h).
+  1: apply (h13 h).
+  1: apply (h23 h).
+  intros a b c; cbn beta.
+  apply isinj_trijoin_rec_inv_helper.
+  exact (h123 h a b c).
+Defined.
+
+(** * We now introduce several lemmas and tactics that will dispense with some routine goals. The idea is that a generic triangle can be assumed to be trivial on the first vertex, and a generic prism can be assumed to be the identity on the domain. In order to apply the [triangle_ind] and [prism_ind] lemmas that make this precise, we need to generalize various terms in the goal. *)
+
+(** This destructs a seven component term [f], tries to generalize each piece evaluated appropriately, and clears all pieces.  If called with [a], [b] and [c] all valid terms, we expect all seven components to be generalized.  But one can also call it with one of [a], [b] and [c] a dummy value (e.g. [_X_]) that causes four of the [generalize] tactics to fail.  In this case, four components will be simply cleared, and three will be generalized and cleared, so this applies when the goal only depends on three of the seven components. *)
+Ltac generalize_some f a b c :=
+  let f1 := fresh in let f2 := fresh in let f3 := fresh in
+  let f12 := fresh in let f13 := fresh in let f23 := fresh in
+  let f123 := fresh in
+  destruct f as [f1 f2 f3 f12 f13 f23 f123]; cbn;
+  try generalize (f123 a b c); clear f123;
+  try generalize (f23 b c); clear f23;
+  try generalize (f13 a c); clear f13;
+  try generalize (f12 a b); clear f12;
+  try generalize (f3 c); clear f3;
+  try generalize (f2 b); clear f2;
+  try generalize (f1 a); clear f1.
+  (* No easy way to skip the "last" one, since we don't know which will be the last to be generalized. *)
+
+(** Use this with [f : TriJoinRecData A B C P], [a : A], [b : B], [c : C]. *)
+Ltac triangle_ind f a b c :=
+  generalize_some f a b c;
+  intro f; (* [generalize_some] goes one step too far, so intro the last variable. *)
+  apply triangle_ind.
+
+(** Use this with [f : TriJoinRecData A B C P]. Two of the arguments [a], [b] and [c] should be elements of [A], [B] and [C], respectively, and the third should be a dummy value (e.g. [_X_]) that causes the generalize tactic to fail.  It applies to goals that only depend on the components of [f] involving just two of [A], [B] and [C]. *)
+Ltac triangle_ind_two f a b c :=
+  generalize_some f a b c;
+  intro f; (* [generalize_some] goes one step too far, so intro the last variable. *)
+  apply paths_ind.
+
+(** The prism analog of the function [triangle_ind] from earlier in the file. To prove something about all prisms, it's enough to prove it for the "identity" prism.  Note that we don't specialize to a prism concentrated on a single vertex, since sometimes we have to deal with a composite of two prisms. *)
+Definition prism_ind {P : Type} (a b c : P) (ab : a = b) (ac : a = c) (bc : b = c) (abc : ab @ bc = ac)
+  (Q : forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac')
+         (k1 : a = a') (k2 : b = b') (k3 : c = c')
+         (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc')
+         (k123 : prism abc abc' k12 k13 k23), Type)
+  (s : Q a b c ab ac bc abc idpath idpath idpath (equiv_p1_1q idpath) (equiv_p1_1q idpath) (equiv_p1_1q idpath) (prism_id abc))
+  : forall a' b' c' ab' ac' bc' abc' k1 k2 k3 k12 k13 k23 k123, Q a' b' c' ab' ac' bc' abc' k1 k2 k3 k12 k13 k23 k123.
+Proof.
+  intros.
+  induction k1, k2, k3.
+  revert k123.
+  revert k12; equiv_intro (equiv_p1_1q (p:=ab) (q:=ab')) k12'; induction k12'.
+  revert k13; equiv_intro (equiv_p1_1q (p:=ac) (q:=ac')) k13'; induction k13'.
+  revert k23; equiv_intro (equiv_p1_1q (p:=bc) (q:=bc')) k23'; induction k23'.
+  induction ab, bc, abc; simpl in *.
+  unfold prism; simpl.
+  equiv_intro (equiv_concat_r (concat_1p (whiskerL 1 abc') @ whiskerL_1p_1 abc')^ idpath) k123'.
+  induction k123'.
+  simpl.
+  exact s.
+Defined.
+
+(** Use this with [f g : TriJoinRecData A B C P], [h : TriJoinRecPath f g] (so [g] is the *co*domain of [h]), [a : A], [b : B], [c : C]. *)
+Ltac prism_ind g h a b c :=
+  generalize_some h a b c;
+  generalize_some g a b c;
+  apply prism_ind.
+
+(** Use this with [f g : TriJoinRecData A B C P], [h : TriJoinRecPath f g] (so [g] is the *co*domain of [h]).  Two of the arguments [a], [b] and [c] should be elements of [A], [B] and [C], respectively, and the third should be a dummy value (e.g. [_X_]) that causes the generalize tactic to fail.  It applies to goals that only depend on the components of [g] and [h] involving just two of [A], [B] and [C]. So it is dealing with one square face of the prism. *)
+Ltac prism_ind_two g h a b c :=
+  generalize_some h a b c;
+  generalize_some g a b c;
+  apply square_ind. (* From Join/Core.v *)
+
+(** * Here we start using the WildCat library to organize things. *)
+
+(** We begin by showing that [TriJoinRecData A B C P] is a 0-groupoid, one piece at a time. *)
+Global Instance isgraph_trijoinrecdata (A B C P : Type) : IsGraph (TriJoinRecData A B C P)
+  := {| Hom := TriJoinRecPath |}.
+
+Global Instance is01cat_trijoinrecdata (A B C P : Type) : Is01Cat (TriJoinRecData A B C P).
+Proof.
+  apply Build_Is01Cat.
+  - intro f.
+    bundle_trijoinrecpath.
+    1, 2, 3: reflexivity.
+    intros a b c; cbn beta.
+    (* Can finish with:  [by triangle_ind f a b c.] *)
+    unfold prism'.
+    cbn.
+    apply concat_p1_1p.
+  - intros f1 f2 f3 k2 k1.
+    snrapply Build_TriJoinRecPath; intros; cbn beta.
+    + exact (h1 k1 a @ h1 k2 a).
+    + exact (h2 k1 b @ h2 k2 b).
+    + exact (h3 k1 c @ h3 k2 c).
+    + (* Some simple path algebra works as well. *)
+      prism_ind_two f3 k2 a b _X_.
+      prism_ind_two f2 k1 a b _X_.
+      by triangle_ind_two f1 a b _X_.
+    + prism_ind_two f3 k2 a _X_ c.
+      prism_ind_two f2 k1 a _X_ c.
+      by triangle_ind_two f1 a _X_ c.
+    + prism_ind_two f3 k2 _X_ b c.
+      prism_ind_two f2 k1 _X_ b c.
+      by triangle_ind_two f1 _X_ b c.
+    + cbn beta. prism_ind f3 k2 a b c.
+      prism_ind f2 k1 a b c.
+      by triangle_ind f1 a b c.
+Defined.
+
+Global Instance is0gpd_trijoinrecdata (A B C P : Type) : Is0Gpd (TriJoinRecData A B C P).
+Proof.
+  apply Build_Is0Gpd.
+  intros f g h.
+  snrapply Build_TriJoinRecPath; intros; cbn beta.
+  + exact (h1 h a)^.
+  + exact (h2 h b)^.
+  + exact (h3 h c)^.
+  + (* Some simple path algebra works as well. *)
+    prism_ind_two g h a b _X_.
+    by triangle_ind_two f a b _X_.
+  + prism_ind_two g h a _X_ c.
+    by triangle_ind_two f a _X_ c.
+  + prism_ind_two g h _X_ b c.
+    by triangle_ind_two f _X_ b c.
+  + prism_ind g h a b c.
+    by triangle_ind f a b c.
+Defined.
+
+Definition trijoinrecdata_0gpd (A B C P : Type) : ZeroGpd
+  := Build_ZeroGpd (TriJoinRecData A B C P) _ _ _.
+
+(** * Next we show that [trijoinrecdata_0gpd A B C] is a 1-functor from [Type] to [ZeroGpd]. *)
+
+(** It's a 1-functor that lands in [ZeroGpd], and the morphisms of [ZeroGpd] are 0-functors, so it's easy to get confused about the levels. *)
+
+(** First we need to show that the induced map is a morphism in [ZeroGpd], i.e. that it is a 0-functor. *)
+Global Instance is0functor_trijoinrecdata_fun {A B C P Q : Type} (g : P -> Q)
+  : Is0Functor (@trijoinrecdata_fun A B C P Q g).
+Proof.
+  apply Build_Is0Functor.
+  intros f1 f2 h.
+  snrapply Build_TriJoinRecPath; intros; cbn.
+  1, 2, 3: apply (ap g).
+  1: apply (h1 h).
+  1: apply (h2 h).
+  1: apply (h3 h).
+  1, 2, 3: refine ((ap_pp g _ _)^ @ _ @ ap_pp g _ _); apply (ap (ap g)).
+  1: apply (h12 h). (* Or: prism_ind_12 f2 h a b. triangle_ind_12 f1 a b. reflexivity. *)
+  1: apply (h13 h).
+  1: apply (h23 h).
+  prism_ind f2 h a b c.
+  triangle_ind f1 a b c; cbn.
+  reflexivity.
+Defined.
+
+(** [trijoinrecdata_0gpd A B C] is a 0-functor from [Type] to [ZeroGpd] (one level up). *)
+Global Instance is0functor_trijoinrecdata_0gpd (A B C : Type) : Is0Functor (trijoinrecdata_0gpd A B C).
+Proof.
+  apply Build_Is0Functor.
+  intros P Q g.
+  snrapply Build_Morphism_0Gpd.
+  - exact (trijoinrecdata_fun g).
+  - apply is0functor_trijoinrecdata_fun.
+Defined.
+
+(** [trijoinrecdata_0gpd A B C] is a 1-functor from [Type] to [ZeroGpd]. *)
+Global Instance is1functor_trijoinrecdata_0gpd (A B C : Type) : Is1Functor (trijoinrecdata_0gpd A B C).
+Proof.
+  apply Build_Is1Functor.
+  (* If [g1 g2 : P -> Q] are homotopic, then the induced maps are homotopic: *)
+  - intros P Q g1 g2 h f; cbn in *.
+    snrapply Build_TriJoinRecPath; intros; cbn.
+    1, 2, 3: apply h.
+    1, 2, 3: apply concat_Ap.
+    triangle_ind f a b c; cbn.
+    by induction (h f).
+  (* The identity map [P -> P] is sent to a map homotopic to the identity. *)
+  - intros P f; cbn.
+    bundle_trijoinrecpath; intros; cbn.
+    1, 2, 3: apply ap_idmap.
+    by triangle_ind f a b c.
+  (* It respects composition. *)
+  - intros P Q R g1 g2 f; cbn.
+    bundle_trijoinrecpath; intros; cbn.
+    1, 2, 3: apply ap_compose.
+    by triangle_ind f a b c.
+Defined.
+
+Definition trijoinrecdata_0gpd_fun (A B C : Type) : Fun11 Type ZeroGpd
+  := Build_Fun11 _ _ (trijoinrecdata_0gpd A B C).
+
+(** By the Yoneda lemma, it follows from [TriJoinRecData] being a 1-functor that given [TriJoinRecData] in [J], we get a map [(J -> P) $-> (TriJoinRecData A B C P)] of 0-groupoids which is natural in [P]. Below we will specialize to the case where [J] is [TriJoin A B C] with the canonical [TriJoinRecData]. *)
+Definition trijoin_nattrans_recdata {A B C J : Type} (f : TriJoinRecData A B C J)
+  : NatTrans (opyon_0gpd J) (trijoinrecdata_0gpd_fun A B C).
+Proof.
+  snrapply Build_NatTrans.
+  - rapply opyoneda_0gpd; exact f.
+  - exact _.
+Defined.  
+
+(** Thus we get a map [(TriJoin A B C -> P) $-> (TriJoinRecData A B C P)] of 0-groupoids, natural in [P]. The underlying map is [trijoin_rec_inv A B C P]. *)
+Definition trijoin_rec_inv_nattrans (A B C : Type)
+  : NatTrans (opyon_0gpd (TriJoin A B C)) (trijoinrecdata_0gpd_fun A B C)
+  := trijoin_nattrans_recdata (trijoinrecdata_trijoin A B C).
+
+(** This natural transformation is in fact a natural equivalence of 0-groupoids. *)
+Definition trijoin_rec_inv_natequiv (A B C : Type)
+  : NatEquiv (opyon_0gpd (TriJoin A B C)) (trijoinrecdata_0gpd_fun A B C).
+Proof.
+  snrapply Build_NatEquiv'.
+  1: apply trijoin_rec_inv_nattrans.
+  intro P.
+  apply isequiv_0gpd_issurjinj.
+  apply Build_IsSurjInj.
+  - intros f; cbn in f.
+    exists (trijoin_rec f).
+    apply trijoin_rec_beta.
+  - exact (@isinj_trijoin_rec_inv A B C P).
+Defined.
+
+(** It will be handy to name the inverse natural equivalence. *)
+Definition trijoin_rec_natequiv (A B C : Type)
+  := natequiv_inverse _ _ (trijoin_rec_inv_natequiv A B C).
+
+(** [trijoin_rec_natequiv A B C P] is an equivalence of 0-groupoids whose underlying function is definitionally [trijoin_rec]. *)
+Local Definition trijoin_rec_natequiv_check (A B C P : Type)
+  : equiv_fun_0gpd (trijoin_rec_natequiv A B C P) = @trijoin_rec A B C P
+  := idpath.
+
+(** It follows that [trijoin_rec A B C P] is a 0-functor. *)
+Global Instance is0functor_trijoin_rec (A B C P : Type) : Is0Functor (@trijoin_rec A B C P).
+Proof.
+  change (Is0Functor (equiv_fun_0gpd (trijoin_rec_natequiv A B C P))).
+  exact _.
+Defined.
+
+(** And that [trijoin_rec A B C] is natural.   The [$==] in the statement is just [==], but we use WildCat notation so that we can invert and compose these with WildCat notation. *)
+Definition trijoin_rec_nat (A B C : Type) {P Q : Type} (g : P -> Q)
+  (f : TriJoinRecData A B C P)
+  : trijoin_rec (trijoinrecdata_fun g f) $== g o trijoin_rec f.
+Proof.
+  exact (isnat (trijoin_rec_natequiv A B C) g f).
+Defined.
diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v
index 53fda42df6f..b37788c093e 100644
--- a/theories/Homotopy/Suspension.v
+++ b/theories/Homotopy/Suspension.v
@@ -110,7 +110,8 @@ Proof.
   refine (transport_paths_FlFr_D
     (g := Susp_ind P (f North) (f South) (fun x : X => apD f (merid x)))
     _ _ @ _); simpl.
-  apply moveR_pM. apply (concat (concat_p1 _)), (concatR (concat_1p _)^).
+  apply moveR_pM.
+  apply equiv_p1_1q.
   apply ap, inverse. refine (Susp_ind_beta_merid _ _ _ _ _).
 Defined.
 
@@ -123,7 +124,7 @@ Proof.
   cbn.
   refine (concat_pp_p _ _ _ @ _).
   apply moveR_Vp.
-  refine (concat_1p _ @ _ @ (concat_p1 _)^).
+  apply equiv_1p_q1.
   apply (equiv_inj dp_path_transport).
   refine (dp_path_transport_apD _ _ @ _). 
   refine (_ @ (dp_path_transport_apD f (merid x))^).
@@ -135,10 +136,9 @@ Definition Susp_rec_eta_homot {X Y : Type} (f : Susp X -> Y)
 Proof.
   refine (Susp_ind _ 1 1 _).
   intro x.
-  refine ((transport_paths_FlFr _ _) @ _). apply moveR_Mp.
-  refine ((Susp_rec_beta_merid _) @ _). hott_simpl.
-  refine (_ @ (ap_V f _)). f_ap.
-  refine (inv_V _)^.
+  apply transport_paths_FlFr'.
+  apply equiv_p1_1q.
+  exact (Susp_rec_beta_merid _)^.
 Defined.
 
 Definition Susp_eta `{Funext}
diff --git a/theories/Idempotents.v b/theories/Idempotents.v
index 99a1a1286b0..ce2115bc672 100644
--- a/theories/Idempotents.v
+++ b/theories/Idempotents.v
@@ -113,7 +113,7 @@ Proof.
     exists equiv_idmap.
     exists (fun x => 1%path).
     exists (fun x => 1%path).
-    cbn. exact (fun a => concat_p1 _ @ ap_idmap (H a) @ (concat_1p _)^). }
+    cbn. exact (fun a => equiv_p1_1q (ap_idmap (H a))). }
   intros [A [r [s H]]]; cbn.
   unfold PathRetractOf.
   contr_sigsig A (equiv_idmap A); cbn.
diff --git a/theories/Metatheory/PropTrunc.v b/theories/Metatheory/PropTrunc.v
index 216b60cd829..cec2f4a45d7 100644
--- a/theories/Metatheory/PropTrunc.v
+++ b/theories/Metatheory/PropTrunc.v
@@ -1,6 +1,6 @@
 Require Import Basics Types.
 Require Import Diagrams.Sequence.
-Require Import Homotopy.Join.
+Require Import Homotopy.Join.Core.
 Require Import Colimits.Colimit Colimits.Sequential.
 
 Local Open Scope nat_scope.
diff --git a/theories/Modalities/Closed.v b/theories/Modalities/Closed.v
index d0c8782de64..c6872d96815 100644
--- a/theories/Modalities/Closed.v
+++ b/theories/Modalities/Closed.v
@@ -3,7 +3,7 @@
 Require Import HoTT.Basics HoTT.Types.
 Require Import Extensions.
 Require Import Modality Accessible Nullification Lex Topological.
-Require Import Colimits.Pushout Homotopy.Join.
+Require Import Colimits.Pushout Homotopy.Join.Core.
 
 Local Open Scope nat_scope.
 Local Open Scope path_scope.
diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
index 0af6f78e299..cc8fb2b12f8 100644
--- a/theories/Modalities/Lex.v
+++ b/theories/Modalities/Lex.v
@@ -152,7 +152,7 @@ Section LexModality.
     refine (_ @ (O_rec_beta _ _)^).
     unfold diagonal, functor_pullback, functor_sigma; cbn.
     apply ap, ap.
-    apply moveL_pV; exact (concat_1p _ @ (concat_p1 _)^).
+    apply moveL_pV; exact (concat_1p_p1 _).
   Defined.
 
   (** RSS Theorem 3.1 (xi) *)
diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index e85755b1266..81bd9c896a2 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -319,8 +319,7 @@ Proof.
   symmetry.
   apply moveR_pV.
   simpl.
-  refine (concat_p1 _ @ _ @ (concat_1p _)^).
-  nrapply ap_idmap.
+  apply equiv_p1_1q, ap_idmap.
 Defined.
 
 (** ** Funext for pointed types and direct consequences. *)
diff --git a/theories/Spaces/Spheres.v b/theories/Spaces/Spheres.v
index 9cd79384511..9e3ef01ec62 100644
--- a/theories/Spaces/Spheres.v
+++ b/theories/Spaces/Spheres.v
@@ -74,22 +74,24 @@ Global Instance isequiv_S1_to_Circle : IsEquiv (S1_to_Circle) | 0.
 Proof.
   apply isequiv_adjointify with Circle_to_S1.
   - refine (Circle_ind _ 1 _).
-    refine ((transport_paths_FFlr _ _) @ _).
-    unfold Circle_to_S1; rewrite Circle_rec_beta_loop.
-    rewrite ap_pp, ap_V.
-    unfold S1_to_Circle. simpl. rewrite 2 Susp_rec_beta_merid. simpl.
-    hott_simpl.
+    nrapply transport_paths_FFlr'; apply equiv_p1_1q.
+    refine (ap _ (Circle_rec_beta_loop _ _ _) @ _).
+    refine (ap_pp _ _ (merid South)^ @ _).
+    refine ((1 @@ ap_V _ _) @ _).
+    refine ((_ @@ (ap inverse _)) @ _). 1, 2: nrapply Susp_rec_beta_merid.
+    simpl.
+    apply concat_p1.
   - refine (Susp_ind (fun x => Circle_to_S1 (S1_to_Circle x) = x)
                      1 (merid South) _); intros x.
-    refine ((transport_paths_FFlr _ _) @ _).
+    nrapply transport_paths_FFlr'; symmetry.
     unfold S1_to_Circle; rewrite (Susp_rec_beta_merid x).
     revert x. change (Susp Empty) with (Sphere 0).
     apply (equiv_ind (S0_to_Bool ^-1)); intros x.
     case x; simpl.
-    2: apply concat_1p.
+    2: reflexivity.
+    lhs nrapply concat_1p.
     unfold Circle_to_S1; rewrite Circle_rec_beta_loop.
-    refine (whiskerR (concat_p1 _) _ @ _).
-    apply moveR_Vp. hott_simpl.
+    symmetry; apply concat_pV_p.
 Defined.
 
 Definition equiv_S1_Circle : Sphere 1 <~> Circle
@@ -122,46 +124,45 @@ Defined.
 Definition issect_TwoSphere_to_S2 : S2_to_TwoSphere o TwoSphere_to_S2 == idmap.
 Proof.
   refine (TwoSphere_ind _ 1 _). 
-  refine (_ @ (concat_p1 _)).
-  refine (_ @ (@concat_Ap (base = base) _ _
+  rhs_V rapply concat_p1.
+  rhs refine (@concat_Ap (base = base) _ _
                           (fun p => (p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))^)
                           (fun x =>
                              (transport_paths_FFlr x 1) 
                                @ ap (fun u => u @ x) (concat_p1 _)
                                @ ap (fun w => _ @ w) (inv_V x)^ 
                                @ (inv_pp _ _)^) 
-                          1 1 surf)^).
-  refine (_ @ (concat_1p _)^).
-  refine (_ @ (ap_compose (fun p => p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p)) 
+                          1 1 surf).
+  rhs rapply concat_1p.
+  rhs refine (ap_compose (fun p => p^ @ ap S2_to_TwoSphere (ap TwoSphere_to_S2 p))
                           inverse
-                          surf)^).
+                          surf).
   refine (@ap _ _ (ap inverse) 1 _ _).
-  refine (_ @ (concat2_ap_ap _ _ _)).
-  refine (_ @ (ap (fun w => inverse2 surf @@ w) 
-                  (ap_compose (ap TwoSphere_to_S2) (ap S2_to_TwoSphere) surf))^).
-  refine ((concat_Vp_inverse2 _ _ surf)^ @ _).
-  refine ((concat_p1 _) @ _). 
+  rhs_V rapply concat2_ap_ap.
+  rhs refine (ap (fun w => inverse2 surf @@ w)
+                  (ap_compose (ap TwoSphere_to_S2) (ap S2_to_TwoSphere) surf)).
+  lhs_V refine (concat_Vp_inverse2 _ _ surf).
+  lhs rapply concat_p1.
   refine (ap (fun p : 1 = 1 => inverse2 surf @@ p) _).
 
-  symmetry. refine ((ap (ap (ap S2_to_TwoSphere))
-                        (TwoSphere_rec_beta_surf (Sphere 2) North _)) @ _).
-  refine ((ap_transport (concat_pV (merid North))
+  symmetry. lhs refine ((ap (ap (ap S2_to_TwoSphere))
+                        (TwoSphere_rec_beta_surf (Sphere 2) North _))).
+  lhs refine (ap_transport (concat_pV (merid North))
                         (fun z => @ap _ _ _ z z) 
                         (ap (fun u => merid u @ (merid North)^)
-                            (merid North @ (merid South)^))) @ _).
+                            (merid North @ (merid South)^))).
   
-  refine ((ap (transport (fun z => ap S2_to_TwoSphere z = ap S2_to_TwoSphere z) 
-                         (concat_pV (merid North)))
-              (ap_compose (fun u => merid u @ (merid North)^) (ap S2_to_TwoSphere) 
-                          (merid North @ (merid South)^))^) @ _).
-  refine ((transport_paths_FlFr _ _) @ _). rewrite_moveR_Vp_p.
-  refine ((ap (fun w => _ @ w) 
-              (ap_pp_concat_pV S2_to_TwoSphere (merid North))^) @ _).
-  refine ((ap (fun w => _ @ (_ @ (_ @ w)))
-              (concat_pV_inverse2 (ap S2_to_TwoSphere (merid North)) 
-                                  _ 
-                                  (Susp_rec_beta_merid North))^) @ _).
-  refine ((@concat_Ap (Sphere 1) _ 
+  lhs_V refine (ap (transport (fun z => ap S2_to_TwoSphere z = ap S2_to_TwoSphere z)
+                      (concat_pV (merid North)))
+               (ap_compose (fun u => merid u @ (merid North)^) (ap S2_to_TwoSphere)
+                           (merid North @ (merid South)^))).
+  apply transport_paths_FlFr'; symmetry.
+  lhs_V refine (1 @@ ap_pp_concat_pV S2_to_TwoSphere (merid North)).
+  lhs_V refine (1 @@ (1 @@ (1 @@
+                              (concat_pV_inverse2 (ap S2_to_TwoSphere (merid North))
+                                  _
+                                  (Susp_rec_beta_merid North))))).
+  lhs refine (@concat_Ap (Sphere 1) _
                       (fun x => ap S2_to_TwoSphere (merid x @ (merid North)^))
                       (fun x => Susp_rec 1 1 
                                 (Susp_rec surf 1 
@@ -172,20 +173,20 @@ Proof.
                                 @ ((Susp_rec_beta_merid x 
                                    @@ inverse2 (Susp_rec_beta_merid North)) 
                                 @ 1)))
-                      North North (merid North @ (merid South)^)) @ _). f_ap.
-  { refine (_ @ (ap_pp_concat_pV _ _)).
-    refine (ap (fun w => _ @ (_ @ w)) (concat_pV_inverse2 _ _ _)). }
-  refine ((concat2_ap_ap (Susp_rec 1 1 (Susp_rec surf 1 
+                      North North (merid North @ (merid South)^)). f_ap.
+  { rhs_V refine (ap_pp_concat_pV _ _).
+    exact (1 @@ (1 @@ (concat_pV_inverse2 _ _ _))). }
+  lhs_V refine (concat2_ap_ap (Susp_rec 1 1 (Susp_rec surf 1
                                          Empty_rec)) 
                          (fun _ => 1) 
-                         (merid North @ (merid South)^))^ @ _).
-  refine ((ap (fun w => _ @@ w) (ap_const _ _)) @ _).
-  refine ((whiskerR_p1_1 _) @ _).
-  refine ((ap_pp _ (merid North) (merid South)^) @ _). 
-  refine (_ @ (concat_p1 _)). f_ap.
-  - refine (Susp_rec_beta_merid North).
-  - refine (ap_V _ _ @ _). refine (@inverse2 _ _ _ _ 1 _).
-    refine (Susp_rec_beta_merid South).
+                         (merid North @ (merid South)^)).
+  lhs refine (ap (fun w => _ @@ w) (ap_const _ _)).
+  lhs rapply whiskerR_p1_1.
+  lhs refine (ap_pp _ (merid North) (merid South)^).
+  rhs_V rapply concat_p1. f_ap.
+  - exact (Susp_rec_beta_merid North).
+  - lhs rapply ap_V. refine (@inverse2 _ _ _ _ 1 _).
+    exact (Susp_rec_beta_merid South).
 Defined.
 
 Definition issect_S2_to_TwoSphere : TwoSphere_to_S2 o S2_to_TwoSphere == idmap.
diff --git a/theories/Types/Paths.v b/theories/Types/Paths.v
index 5f3484122ce..38f067ec5fa 100644
--- a/theories/Types/Paths.v
+++ b/theories/Types/Paths.v
@@ -87,6 +87,29 @@ Proof.
   exact ((concat_1p q)^ @ (concat_p1 (1 @ q))^).
 Defined.
 
+(** Variants of the above that do the most common rearranging. We could add similar variants for the others as needed. *)
+Definition transport_paths_FlFr' {A B : Type} {f g : A -> B} {x1 x2 : A}
+  (p : x1 = x2) (q : f x1 = g x1) (r : (f x2) = (g x2))
+  (h : (ap f p) @ r = q @ (ap g p))
+  : transport (fun x => f x = g x) p q = r.
+Proof.
+  refine (transport_paths_FlFr _ _ @ _).
+  refine (concat_pp_p _ _ _ @ _).
+  apply moveR_Vp.
+  exact h^.
+Defined.
+
+Definition transport_paths_FFlr' {A B : Type} {f : A -> B} {g : B -> A} {x1 x2 : A}
+  (p : x1 = x2) (q : g (f x1) = x1) (r : g (f x2) = x2)
+  (h : (ap g (ap f p)) @ r = q @ p)
+  : transport (fun x => g (f x) = x) p q = r.
+Proof.
+  refine (transport_paths_FFlr _ _ @ _).
+  refine (concat_pp_p _ _ _ @ _).
+  apply moveR_Vp.
+  exact h^.
+Defined.
+
 (** ** Transporting in 2-path types *)
 
 Definition transport_paths2 {A : Type} {x y : A}
@@ -163,6 +186,14 @@ Definition equiv_concat_lr {A : Type} {x x' y y' : A} (p : x' = x) (q : y = y')
   : (x = y) <~> (x' = y')
   := Build_Equiv _ _ (fun r:x=y => p @ r @ q) _.
 
+Definition equiv_p1_1q {A : Type} {x y : A} {p q : x = y}
+  : p = q <~> p @ 1 = 1 @ q
+  := equiv_concat_lr (concat_p1 p) (concat_1p q)^.
+
+Definition equiv_1p_q1 {A : Type} {x y : A} {p q : x = y}
+  : p = q <~> 1 @ p = q @ 1
+  := equiv_concat_lr (concat_1p p) (concat_p1 q)^.
+
 Global Instance isequiv_whiskerL {A} {x y z : A} (p : x = y) {q r : y = z}
 : IsEquiv (@whiskerL A x y z p q r).
 Proof.