Require Import Basics Types Cubical.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import NullHomotopy.
Require Import Extensions.
Require Import Colimits.Pushout.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Pointed.Core.
Require Import WildCat.
Require Import Spaces.Nat.Core.

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.
A, B: Type
P: Join A B -> Type
P_A: forall a : A, P (joinl a)
P_B: forall b : B, P (joinr b)
P_g: forall (a : A) (b : B), transport P (jglue a b) (P_A a) = P_B b
forall x : Join A B, P x
  Proof.
A, B: Type
P: Join A B -> Type
P_A: forall a : A, P (joinl a)
P_B: forall b : B, P (joinr b)
P_g: forall (a : A) (b : B), transport P (jglue a b) (P_A a) = P_B b
forall x : Join A B, P x
    apply (Pushout_ind P P_A P_B).
A, B: Type
P: Join A B -> Type
P_A: forall a : A, P (joinl a)
P_B: forall b : B, P (joinr b)
P_g: forall (a : A) (b : B), transport P (jglue a b) (P_A a) = P_B b
forall a : A * B,
transport P (pglue a) (P_A (fst a)) = P_B (snd a)
    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] 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.
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
f == g
  Proof.
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
f == g
    snrapply Join_ind.
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
forall a : A,
(fun x : Join A B => f x = g x) (joinl a)
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
forall b : B,
(fun x : Join A B => f x = g x) (joinr b)
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
forall (a : A) (b : B),
transport (fun x : Join A B => f x = g x) 
  (jglue a b) (?P_A a) = 
?P_B b
    -
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
forall a : A,
(fun x : Join A B => f x = g x) (joinl a) exact Hl.
    -
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
forall b : B,
(fun x : Join A B => f x = g x) (joinr b) exact Hr.
    -
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
forall (a : A) (b : B),
transport (fun x : Join A B => f x = g x) (jglue a b)
  (Hl a) = Hr b intros a b.
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
a: A
b: B
transport (fun x : Join A B => f x = g x) (jglue a b)
  (Hl a) = Hr b
      nrapply transport_paths_FlFr'.
A, B, P: Type
f, g: Join A B -> P
Hl: forall a : A, f (joinl a) = g (joinl a)
Hr: forall b : B, f (joinr b) = g (joinr b)
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b =
Hl a @ ap g (jglue a b)
a: A
b: B
ap f (jglue a b) @ Hr b = Hl a @ ap g (jglue a b)
      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.
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
forall x : Join A B, g (f x) = x
  Proof.
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
forall x : Join A B, g (f x) = x
    snrapply Join_ind.
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
forall a : A,
(fun x : Join A B => g (f x) = x) (joinl a)
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
forall b : B,
(fun x : Join A B => g (f x) = x) (joinr b)
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
forall (a : A) (b : B),
transport (fun x : Join A B => g (f x) = x)
  (jglue a b) (?P_A a) = 
?P_B b
    -
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
forall a : A,
(fun x : Join A B => g (f x) = x) (joinl a) exact Hl.
    -
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
forall b : B,
(fun x : Join A B => g (f x) = x) (joinr b) exact Hr.
    -
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
forall (a : A) (b : B),
transport (fun x : Join A B => g (f x) = x)
  (jglue a b) (Hl a) = Hr b intros a b.
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
a: A
b: B
transport (fun x : Join A B => g (f x) = x)
  (jglue a b) (Hl a) = Hr b
      nrapply transport_paths_FFlr'.
A, B, P: Type
f: Join A B -> P
g: P -> Join A B
Hl: forall a : A, g (f (joinl a)) = joinl a
Hr: forall b : B, g (f (joinr b)) = joinr b
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ jglue a b
a: A
b: B
ap g (ap f (jglue a b)) @ Hr b = Hl a @ jglue a b
      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.
A, B, P: Type
P_A: A -> P
P_B: B -> P
P_g: forall (a : A) (b : B), P_A a = P_B b
Join A B -> P
  Proof.
A, B, P: Type
P_A: A -> P
P_B: B -> P
P_g: forall (a : A) (b : B), P_A a = P_B b
Join A B -> P
    apply (Pushout_rec P P_A P_B).
A, B, P: Type
P_A: A -> P
P_B: B -> P
P_g: forall (a : A) (b : B), P_A a = P_B b
forall a : A * B, P_A (fst a) = P_B (snd a)
    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.
A, B, P: Type
P_A: A -> P
P_B: B -> P
P_g: forall (a : A) (b : B), P_A a = P_B b
a: A
b: B
ap (Join_rec P_A P_B P_g) (jglue a b) = P_g a b
  Proof.
A, B, P: Type
P_A: A -> P
P_B: B -> P
P_g: forall (a : A) (b : B), P_A a = P_B b
a: A
b: B
ap (Join_rec P_A P_B P_g) (jglue a b) = P_g a b
    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.

Arguments joinl {A B}%type_scope _ , [A] B _.
Arguments joinr {A B}%type_scope _ , A [B] _.

(** * [Join_rec] gives an equivalence of 0-groupoids

  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.
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
JoinRecData A B Q
Proof.
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
JoinRecData A B Q
  snrapply Build_JoinRecData.
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
A -> Q
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
B -> Q
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
forall (a : A) (b : B), ?jl a = ?jr b
  -
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
A -> Q exact (g o jl f).
  -
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
B -> Q exact (g o jr f).
  -
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
forall (a : A) (b : B), (g o jl f) a = (g o jr f) b 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. *)

(** ** The graph structure on [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).
A, B, P: Type
jl': A -> P
jr': B -> P
f, g: forall (a : A) (b : B), jl' a = jr' b
h: forall (a : A) (b : B), f a b = g a b
JoinRecPath {| jl := jl'; jr := jr'; jg := f |}
  {| jl := jl'; jr := jr'; jg := g |}
Proof.
A, B, P: Type
jl': A -> P
jr': B -> P
f, g: forall (a : A) (b : B), jl' a = jr' b
h: forall (a : A) (b : B), f a b = g a b
JoinRecPath {| jl := jl'; jr := jr'; jg := f |}
  {| jl := jl'; jr := jr'; jg := g |}
  snrapply Build_JoinRecPath.
A, B, P: Type
jl': A -> P
jr': B -> P
f, g: forall (a : A) (b : B), jl' a = jr' b
h: forall (a : A) (b : B), f a b = g a b
forall a : A,
jl {| jl := jl'; jr := jr'; jg := f |} a =
jl {| jl := jl'; jr := jr'; jg := g |} a
A, B, P: Type
jl': A -> P
jr': B -> P
f, g: forall (a : A) (b : B), jl' a = jr' b
h: forall (a : A) (b : B), f a b = g a b
forall b : B,
jr {| jl := jl'; jr := jr'; jg := f |} b =
jr {| jl := jl'; jr := jr'; jg := g |} b
A, B, P: Type
jl': A -> P
jr': B -> P
f, g: forall (a : A) (b : B), jl' a = jr' b
h: forall (a : A) (b : B), f a b = g a b
forall (a : A) (b : B),
jg {| jl := jl'; jr := jr'; jg := f |} a b @ ?hr b =
?hl a @ jg {| jl := jl'; jr := jr'; jg := g |} a b
  1, 2: reflexivity.
A, B, P: Type
jl': A -> P
jr': B -> P
f, g: forall (a : A) (b : B), jl' a = jr' b
h: forall (a : A) (b : B), f a b = g a b
forall (a : A) (b : B),
jg {| jl := jl'; jr := jr'; jg := f |} a b @
(fun b0 : B => 1) b =
(fun a0 : A => 1) a @
jg {| jl := jl'; jr := jr'; jg := g |} a b
  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).

(** ** Lemmas and tactics about intervals and squares

  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.
P: Type
a, b: P
ab: a = b
Q: forall (a' b' : P) (ab' : a' = b') (ha : a = a')
(hb : b = b'), ab @ hb = ha @ ab' -> Type
s: Q a b ab 1 1 (equiv_p1_1q 1)
forall (a' b' : P) (ab' : a' = b') (ha : a = a')
(hb : b = b') (k : ab @ hb = ha @ ab'),
Q a' b' ab' ha hb k
Proof.
P: Type
a, b: P
ab: a = b
Q: forall (a' b' : P) (ab' : a' = b') (ha : a = a')
(hb : b = b'), ab @ hb = ha @ ab' -> Type
s: Q a b ab 1 1 (equiv_p1_1q 1)
forall (a' b' : P) (ab' : a' = b') (ha : a = a')
(hb : b = b') (k : ab @ hb = ha @ ab'),
Q a' b' ab' ha hb k
  intros.
P: Type
a, b: P
ab: a = b
Q: forall (a' b' : P) (ab' : a' = b') (ha : a = a')
(hb : b = b'), ab @ hb = ha @ ab' -> Type
s: Q a b ab 1 1 (equiv_p1_1q 1)
a', b': P
ab': a' = b'
ha: a = a'
hb: b = b'
k: ab @ hb = ha @ ab'
Q a' b' ab' ha hb k
  destruct ha, hb.
P: Type
a, b: P
ab: a = b
Q: forall (a' b' : P) (ab' : a' = b') (ha : a = a')
(hb : b = b'), ab @ hb = ha @ ab' -> Type
s: Q a b ab 1 1 (equiv_p1_1q 1)
ab': a = b
k: ab @ 1 = 1 @ ab'
Q a b ab' 1 1 k
  revert k; equiv_intro (equiv_p1_1q (p:=ab) (q:=ab')) k'; destruct k'.
P: Type
a, b: P
ab: a = b
Q: forall (a' b' : P) (ab' : a' = b') (ha : a = a')
(hb : b = b'), ab @ hb = ha @ ab' -> Type
s: Q a b ab 1 1 (equiv_p1_1q 1)
Q a b ab 1 1 (equiv_p1_1q 1)
  destruct ab.
P: Type
a: P
Q: forall (a' b' : P) (ab' : a' = b') (ha : a = a')
(hb : a = b'), 1 @ hb = ha @ ab' -> Type
s: Q a a 1 1 1 (equiv_p1_1q 1)
Q a a 1 1 1 (equiv_p1_1q 1)
  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.

(** ** Use 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).
A, B, P: Type
Is01Cat (JoinRecData A B P)
Proof.
A, B, P: Type
Is01Cat (JoinRecData A B P)
  apply Build_Is01Cat.
A, B, P: Type
forall a : JoinRecData A B P, a $-> a
A, B, P: Type
forall a b c : JoinRecData A B P,
(b $-> c) -> (a $-> b) -> a $-> c
  -
A, B, P: Type
forall a : JoinRecData A B P, a $-> a intro f.
A, B, P: Type
f: JoinRecData A B P
f $-> f
    bundle_joinrecpath.
A, B, P: Type
f: JoinRecData A B P
forall (a : A) (b : B), jg f a b = jg f a b
    reflexivity.
  -
A, B, P: Type
forall a b c : JoinRecData A B P,
(b $-> c) -> (a $-> b) -> a $-> c intros f1 f2 f3 h2 h1.
A, B, P: Type
f1, f2, f3: JoinRecData A B P
h2: f2 $-> f3
h1: f1 $-> f2
f1 $-> f3
    snrapply Build_JoinRecPath; intros; cbn beta.
A, B, P: Type
f1, f2, f3: JoinRecData A B P
h2: f2 $-> f3
h1: f1 $-> f2
a: A
jl f1 a = jl f3 a
A, B, P: Type
f1, f2, f3: JoinRecData A B P
h2: f2 $-> f3
h1: f1 $-> f2
b: B
jr f1 b = jr f3 b
A, B, P: Type
f1, f2, f3: JoinRecData A B P
h2: f2 $-> f3
h1: f1 $-> f2
a: A
b: B
jg f1 a b @ ?Goal0 = ?Goal @ jg f3 a b
    +
A, B, P: Type
f1, f2, f3: JoinRecData A B P
h2: f2 $-> f3
h1: f1 $-> f2
a: A
jl f1 a = jl f3 a exact (hl h1 a @ hl h2 a).
    +
A, B, P: Type
f1, f2, f3: JoinRecData A B P
h2: f2 $-> f3
h1: f1 $-> f2
b: B
jr f1 b = jr f3 b exact (hr h1 b @ hr h2 b).
    + (* Some simple path algebra works as well. *)
A, B, P: Type
f1, f2, f3: JoinRecData A B P
h2: f2 $-> f3
h1: f1 $-> f2
a: A
b: B
jg f1 a b @ (hr h1 b @ hr h2 b) =
(hl h1 a @ hl h2 a) @ jg f3 a b
      square_ind f3 h2 a b.
A, B, P: Type
f1, f2: JoinRecData A B P
h1: f1 $-> f2
a: A
b: B
jg f1 a b @ (hr h1 b @ 1) = (hl h1 a @ 1) @ jg f2 a b
      square_ind f2 h1 a b.
A, B, P: Type
f1: JoinRecData A B P
a: A
b: B
jg f1 a b @ (1 @ 1) = (1 @ 1) @ jg f1 a b
      by interval_ind f1 a b.
Defined.

Global Instance is0gpd_joinrecdata (A B P : Type) : Is0Gpd (JoinRecData A B P).
A, B, P: Type
Is0Gpd (JoinRecData A B P)
Proof.
A, B, P: Type
Is0Gpd (JoinRecData A B P)
  apply Build_Is0Gpd.
A, B, P: Type
forall a b : JoinRecData A B P, (a $-> b) -> b $-> a
  intros f g h.
A, B, P: Type
f, g: JoinRecData A B P
h: f $-> g
g $-> f
  snrapply Build_JoinRecPath; intros; cbn beta.
A, B, P: Type
f, g: JoinRecData A B P
h: f $-> g
a: A
jl g a = jl f a
A, B, P: Type
f, g: JoinRecData A B P
h: f $-> g
b: B
jr g b = jr f b
A, B, P: Type
f, g: JoinRecData A B P
h: f $-> g
a: A
b: B
jg g a b @ ?Goal0 = ?Goal @ jg f a b
  +
A, B, P: Type
f, g: JoinRecData A B P
h: f $-> g
a: A
jl g a = jl f a exact (hl h a)^.
  +
A, B, P: Type
f, g: JoinRecData A B P
h: f $-> g
b: B
jr g b = jr f b exact (hr h b)^.
  + (* Some simple path algebra works as well. *)
A, B, P: Type
f, g: JoinRecData A B P
h: f $-> g
a: A
b: B
jg g a b @ (hr h b)^ = (hl h a)^ @ jg f a b
    square_ind g h a b.
A, B, P: Type
f: JoinRecData A B P
a: A
b: B
jg f a b @ 1^ = 1^ @ jg f a b
    by interval_ind f a b.
Defined.

Definition joinrecdata_0gpd (A B P : Type) : ZeroGpd
  := Build_ZeroGpd (JoinRecData A B P) _ _ _.

(** ** [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).
A, B, P, Q: Type
g: P -> Q
Is0Functor (joinrecdata_fun g)
Proof.
A, B, P, Q: Type
g: P -> Q
Is0Functor (joinrecdata_fun g)
  apply Build_Is0Functor.
A, B, P, Q: Type
g: P -> Q
forall a b : JoinRecData A B P,
(a $-> b) ->
joinrecdata_fun g a $-> joinrecdata_fun g b
  intros f1 f2 h.
A, B, P, Q: Type
g: P -> Q
f1, f2: JoinRecData A B P
h: f1 $-> f2
joinrecdata_fun g f1 $-> joinrecdata_fun g f2
  snrapply Build_JoinRecPath; intros; cbn.
A, B, P, Q: Type
g: P -> Q
f1, f2: JoinRecData A B P
h: f1 $-> f2
a: A
g (jl f1 a) = g (jl f2 a)
A, B, P, Q: Type
g: P -> Q
f1, f2: JoinRecData A B P
h: f1 $-> f2
b: B
g (jr f1 b) = g (jr f2 b)
A, B, P, Q: Type
g: P -> Q
f1, f2: JoinRecData A B P
h: f1 $-> f2
a: A
b: B
ap g (jg f1 a b) @ ?Goal0 = ?Goal @ ap g (jg f2 a b)
  -
A, B, P, Q: Type
g: P -> Q
f1, f2: JoinRecData A B P
h: f1 $-> f2
a: A
g (jl f1 a) = g (jl f2 a) exact (ap g (hl h a)).
  -
A, B, P, Q: Type
g: P -> Q
f1, f2: JoinRecData A B P
h: f1 $-> f2
b: B
g (jr f1 b) = g (jr f2 b) exact (ap g (hr h b)).
  -
A, B, P, Q: Type
g: P -> Q
f1, f2: JoinRecData A B P
h: f1 $-> f2
a: A
b: B
ap g (jg f1 a b) @ ap g (hr h b) =
ap g (hl h a) @ ap g (jg f2 a b) square_ind f2 h a b.
A, B, P, Q: Type
g: P -> Q
f1: JoinRecData A B P
a: A
b: B
ap g (jg f1 a b) @ ap g 1 = ap g 1 @ ap g (jg f1 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).
A, B: Type
Is0Functor (joinrecdata_0gpd A B)
Proof.
A, B: Type
Is0Functor (joinrecdata_0gpd A B)
  apply Build_Is0Functor.
A, B: Type
forall a b : Type,
(a $-> b) ->
joinrecdata_0gpd A B a $-> joinrecdata_0gpd A B b
  intros P Q g.
A, B, P, Q: Type
g: P $-> Q
joinrecdata_0gpd A B P $-> joinrecdata_0gpd A B Q
  snrapply Build_Morphism_0Gpd.
A, B, P, Q: Type
g: P $-> Q
joinrecdata_0gpd A B P -> joinrecdata_0gpd A B Q
A, B, P, Q: Type
g: P $-> Q
Is0Functor ?fun_0gpd
  -
A, B, P, Q: Type
g: P $-> Q
joinrecdata_0gpd A B P -> joinrecdata_0gpd A B Q exact (joinrecdata_fun g).
  -
A, B, P, Q: Type
g: P $-> Q
Is0Functor (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).
A, B: Type
Is1Functor (joinrecdata_0gpd A B)
Proof.
A, B: Type
Is1Functor (joinrecdata_0gpd A B)
  apply Build_Is1Functor.
A, B: Type
forall (a b : Type) (f g : a $-> b),
f $== g ->
fmap (joinrecdata_0gpd A B) f $==
fmap (joinrecdata_0gpd A B) g
A, B: Type
forall a : Type,
fmap (joinrecdata_0gpd A B) (Id a) $==
Id (joinrecdata_0gpd A B a)
A, B: Type
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
fmap (joinrecdata_0gpd A B) (g $o f) $==
fmap (joinrecdata_0gpd A B) g $o
fmap (joinrecdata_0gpd A B) f
  (* If [g1 g2 : P -> Q] are homotopic, then the induced maps are homotopic: *)
  -
A, B: Type
forall (a b : Type) (f g : a $-> b),
f $== g ->
fmap (joinrecdata_0gpd A B) f $==
fmap (joinrecdata_0gpd A B) g intros P Q g1 g2 h f; cbn in *.
A, B, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: JoinRecData A B P
JoinRecPath (joinrecdata_fun g1 f)
  (joinrecdata_fun g2 f)
    snrapply Build_JoinRecPath; intros; cbn.
A, B, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: JoinRecData A B P
a: A
g1 (jl f a) = g2 (jl f a)
A, B, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: JoinRecData A B P
b: B
g1 (jr f b) = g2 (jr f b)
A, B, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: JoinRecData A B P
a: A
b: B
ap g1 (jg f a b) @ ?Goal2 = ?Goal1 @ ap g2 (jg f a b)
    1, 2: apply h.
A, B, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: JoinRecData A B P
a: A
b: B
ap g1 (jg f a b) @ h (jr f b) =
h (jl f a) @ ap g2 (jg f a b)
    interval_ind f a b; cbn.
A, B, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
a: A
b: B
f: P
1 @ h f = h f @ 1
    apply concat_1p_p1.
  (* The identity map [P -> P] is sent to a map homotopic to the identity. *)
  -
A, B: Type
forall a : Type,
fmap (joinrecdata_0gpd A B) (Id a) $==
Id (joinrecdata_0gpd A B a) intros P f; cbn.
A, B, P: Type
f: joinrecdata_0gpd A B P
JoinRecPath (joinrecdata_fun idmap f) f
    bundle_joinrecpath; intros; cbn.
A, B, P: Type
f: joinrecdata_0gpd A B P
a: A
b: B
ap idmap (jg f a b) = jg f a b
    apply ap_idmap.
  (* It respects composition. *)
  -
A, B: Type
forall (a b c : Type) (f : a $-> b) (g : b $-> c),
fmap (joinrecdata_0gpd A B) (g $o f) $==
fmap (joinrecdata_0gpd A B) g $o
fmap (joinrecdata_0gpd A B) f intros P Q R g1 g2 f; cbn.
A, B, P, Q, R: Type
g1: P $-> Q
g2: Q $-> R
f: joinrecdata_0gpd A B P
JoinRecPath
  (joinrecdata_fun (fun x : P => g2 (g1 x)) f)
  (joinrecdata_fun g2 (joinrecdata_fun g1 f))
    bundle_joinrecpath; intros; cbn.
A, B, P, Q, R: Type
g1: P $-> Q
g2: Q $-> R
f: joinrecdata_0gpd A B P
a: A
b: B
ap (fun x : P => g2 (g1 x)) (jg f a b) =
ap g2 (ap g1 (jg f a b))
    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).
A, B, J: Type
f: JoinRecData A B J
NatTrans (opyon_0gpd J) (joinrecdata_0gpd_fun A B)
Proof.
A, B, J: Type
f: JoinRecData A B J
NatTrans (opyon_0gpd J) (joinrecdata_0gpd_fun A B) 
  snrapply Build_NatTrans.
A, B, J: Type
f: JoinRecData A B J
opyon_0gpd J $=> joinrecdata_0gpd_fun A B
A, B, J: Type
f: JoinRecData A B J
Is1Natural (opyon_0gpd J) (joinrecdata_0gpd_fun A B)
  ?alpha
  1: rapply opyoneda_0gpd.
A, B, J: Type
f: JoinRecData A B J
joinrecdata_0gpd_fun A B J
A, B, J: Type
f: JoinRecData A B J
Is1Natural (opyon_0gpd J) (joinrecdata_0gpd_fun A B)
  (opyoneda_0gpd J (joinrecdata_0gpd_fun A B) ?Goal)
  2: exact _.
A, B, J: Type
f: JoinRecData A B J
joinrecdata_0gpd_fun A B J
  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).
A, B: Type
NatEquiv (opyon_0gpd (Join A B))
  (joinrecdata_0gpd_fun A B)
Proof.
A, B: Type
NatEquiv (opyon_0gpd (Join A B))
  (joinrecdata_0gpd_fun A B)
  snrapply Build_NatEquiv'.
A, B: Type
NatTrans (opyon_0gpd (Join A B))
  (joinrecdata_0gpd_fun A B)
A, B: Type
forall a : Type, CatIsEquiv (?alpha a)
  1: apply join_rec_inv_nattrans.
A, B: Type
forall a : Type,
CatIsEquiv (join_rec_inv_nattrans A B a)
  intro P.
A, B, P: Type
CatIsEquiv (join_rec_inv_nattrans A B P)
  apply isequiv_0gpd_issurjinj.
A, B, P: Type
IsSurjInj (join_rec_inv_nattrans A B P)
  apply Build_IsSurjInj.
A, B, P: Type
SplEssSurj (join_rec_inv_nattrans A B P)
A, B, P: Type
forall x y : opyon_0gpd (Join A B) P,
join_rec_inv_nattrans A B P x $==
join_rec_inv_nattrans A B P y -> x $== y
  -
A, B, P: Type
SplEssSurj (join_rec_inv_nattrans A B P) intros f; cbn in f.
A, B, P: Type
f: JoinRecData A B P
{a : opyon_0gpd (Join A B) P &
join_rec_inv_nattrans A B P a $== f}
    exists (join_rec f).
A, B, P: Type
f: JoinRecData A B P
join_rec_inv_nattrans A B P (join_rec f) $== f
    apply join_rec_beta.
  -
A, B, P: Type
forall x y : opyon_0gpd (Join A B) P,
join_rec_inv_nattrans A B P x $==
join_rec_inv_nattrans A B P y -> x $== y 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).
A, B, P: Type
Is0Functor join_rec
Proof.
A, B, P: Type
Is0Functor join_rec
  change (Is0Functor (equiv_fun_0gpd (join_rec_natequiv A B P))).
A, B, P: Type
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.
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
join_rec (joinrecdata_fun g f) $== g o join_rec f
Proof.
A, B, P, Q: Type
g: P -> Q
f: JoinRecData A B P
join_rec (joinrecdata_fun g f) $== g o join_rec f
  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).
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.
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
    destruct p, q.
A, B: Type
a: A
b: B
ap joinl 1 @ jglue a b = jglue a b @ ap joinr 1
    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').
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.
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')
    destruct p, q.
A, B: Type
a: A
b: B
PathSquare (ap joinl 1) (ap joinr 1) (jglue a b)
  (jglue a b)
    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).
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.
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)
    destruct p, q.
A, B: Type
a: A
b: B
PathSquare (jglue a b) (jglue a b) (ap joinl 1)
  (ap joinr 1)
    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')
    : ap joinl p @ (jglue a' b) = jglue a b.
A, B: Type
a, a': A
b: B
p: a = a'
ap joinl p @ jglue a' b = jglue a b
  Proof.
A, B: Type
a, a': A
b: B
p: a = a'
ap joinl p @ jglue a' b = jglue a b
    destruct p.
A, B: Type
a: A
b: B
ap joinl 1 @ jglue a b = jglue a b
    apply concat_1p.
  Defined.

  Definition triangle_h' {a a' : A} (b : B) (p : a = a')
    : jglue a b @ (jglue a' b)^ = ap joinl p.
A, B: Type
a, a': A
b: B
p: a = a'
jglue a b @ (jglue a' b)^ = ap joinl p
  Proof.
A, B: Type
a, a': A
b: B
p: a = a'
jglue a b @ (jglue a' b)^ = ap joinl p
    destruct p.
A, B: Type
a: A
b: B
jglue a b @ (jglue a b)^ = ap joinl 1
    apply concat_pV.
  Defined.

  Definition triangle_v (a : A) {b b' : B} (p : b = b')
    : jglue a b @ ap joinr p = jglue a b'.
A, B: Type
a: A
b, b': B
p: b = b'
jglue a b @ ap joinr p = jglue a b'
  Proof.
A, B: Type
a: A
b, b': B
p: b = b'
jglue a b @ ap joinr p = jglue a b'
    destruct p.
A, B: Type
a: A
b: B
jglue a b @ ap joinr 1 = jglue a b
    apply concat_p1.
  Defined.

  Definition triangle_v' (a : A) {b b' : B} (p : b = b')
    : (jglue a b)^ @ jglue a b' = ap joinr p.
A, B: Type
a: A
b, b': B
p: b = b'
(jglue a b)^ @ jglue a b' = ap joinr p
  Proof.
A, B: Type
a: A
b, b': B
p: b = b'
(jglue a b)^ @ jglue a b' = ap joinr p
    destruct p.
A, B: Type
a: A
b: B
(jglue a b)^ @ jglue a b = ap joinr 1
    apply concat_Vp.
  Defined.

  (** For just one of the above, we give a rule for how it behaves on inverse paths. *)
  Definition triangle_v_V (a : A) {b b' : B} (p : b = b')
    : triangle_v a p^ = (1 @@ ap_V joinr p) @ moveR_pV _ _ _ (triangle_v a p)^.
A, B: Type
a: A
b, b': B
p: b = b'
triangle_v a p^ =
(1 @@ ap_V joinr p) @
moveR_pV (ap joinr p) (jglue a b) (jglue a b')
  (triangle_v a p)^
  Proof.
A, B: Type
a: A
b, b': B
p: b = b'
triangle_v a p^ =
(1 @@ ap_V joinr p) @
moveR_pV (ap joinr p) (jglue a b) (jglue a b')
  (triangle_v a p)^
    destruct p; cbn.
A, B: Type
a: A
b: B
concat_p1 (jglue a b) =
1 @
((concat_p1 (jglue a b) @ (concat_p1 (jglue a b))^) @
 concat_p1 (jglue a b))
    rhs nrapply concat_1p.
A, B: Type
a: A
b: B
concat_p1 (jglue a b) =
(concat_p1 (jglue a b) @ (concat_p1 (jglue a b))^) @
concat_p1 (jglue a b)
    symmetry; apply concat_pV_p.
  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')
    : jglue a b @ (jglue a' b)^ = jglue a b' @ (jglue a' b')^.
A, B: Type
a, a': A
b, b': B
p: a = a'
jglue a b @ (jglue a' b)^ =
jglue a b' @ (jglue a' b')^
  Proof.
A, B: Type
a, a': A
b, b': B
p: a = a'
jglue a b @ (jglue a' b)^ =
jglue a b' @ (jglue a' b')^
    destruct p.
A, B: Type
a: A
b, b': B
jglue a b @ (jglue a b)^ = jglue a b' @ (jglue a b')^
    exact (concat_pV _ @ (concat_pV _)^).
  Defined.

  Definition diamond_h_sq {a a' : A} (b b' : B) (p : a = a')
    : Diamond a a' b b'.
A, B: Type
a, a': A
b, b': B
p: a = a'
Diamond a a' b b'
  Proof.
A, B: Type
a, a': A
b, b': B
p: a = a'
Diamond a a' b b'
    by apply sq_path, diamond_h.
  Defined.

  Definition diamond_v (a a' : A) {b b' : B} (p : b = b')
    : jglue a b @ (jglue a' b)^ = jglue a b' @ (jglue a' b')^.
A, B: Type
a, a': A
b, b': B
p: b = b'
jglue a b @ (jglue a' b)^ =
jglue a b' @ (jglue a' b')^
  Proof.
A, B: Type
a, a': A
b, b': B
p: b = b'
jglue a b @ (jglue a' b)^ =
jglue a b' @ (jglue a' b')^
    by destruct p.
  Defined.

  Definition diamond_v_sq (a a' : A) {b b' : B} (p : b = b')
    : Diamond a a' b b'.
A, B: Type
a, a': A
b, b': B
p: b = b'
Diamond a a' b b'
  Proof.
A, B: Type
a, a': A
b, b': B
p: b = b'
Diamond a a' b b'
    by apply sq_path, diamond_v.
  Defined.

  Lemma diamond_symm (a : A) (b : B)
    : diamond_v_sq a a 1 = diamond_h_sq b b 1.
A, B: Type
a: A
b: B
diamond_v_sq a a 1 = diamond_h_sq b b 1
  Proof.
A, B: Type
a: A
b: B
diamond_v_sq a a 1 = diamond_h_sq b b 1
    unfold diamond_v_sq, diamond_h_sq, diamond_v, diamond_h.
A, B: Type
a: A
b: B
sq_path 1 =
sq_path
  (concat_pV (jglue a b) @ (concat_pV (jglue a b))^)
    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_sq a' a 1) (diamond_h_sq a a' 1).
A: Type
a, a': A
p: a = a'
DPath (fun x : A => Diamond a' x a x) p
  (diamond_v_sq a' a 1) (diamond_h_sq a a' 1)
Proof.
A: Type
a, a': A
p: a = a'
DPath (fun x : A => Diamond a' x a x) p
  (diamond_v_sq a' a 1) (diamond_h_sq a a' 1)
  destruct p.
A: Type
a: A
DPath (fun x : A => Diamond a x a x) 1
  (diamond_v_sq a a 1) (diamond_h_sq a a 1)
  apply diamond_symm.
Defined.

(** * Functoriality of Join. *)
Section FunctorJoin.

  (** In some cases, we'll need to refer to the recursion data that defines [functor_join], so we make it a separate definition. *)
  Definition functor_join_recdata {A B C D} (f : A -> C) (g : B -> D)
    : JoinRecData A B (Join C D)
    := {| jl := joinl o f; jr := joinr o g; jg := fun a b => jglue (f a) (g b); |}.

  Definition functor_join {A B C D} (f : A -> C) (g : B -> D)
    : Join A B -> Join C D
    := join_rec (functor_join_recdata f g).

  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_jg _ 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.
A, B, C, D, E, F: Type
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.
A, B, C, D, E, F: Type
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
    snrapply Join_ind_FlFr.
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
forall a : A,
functor_join (h o f) (i o g) (joinl a) =
(fun x : Join A B =>
 functor_join h i (functor_join f g x)) (joinl a)
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
forall b : B,
functor_join (h o f) (i o g) (joinr b) =
(fun x : Join A B =>
 functor_join h i (functor_join f g x)) (joinr b)
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
forall (a : A) (b : B),
ap (functor_join (h o f) (i o g)) (jglue a b) @ ?Hr b =
?Hl a @
ap
  (fun x : Join A B =>
   functor_join h i (functor_join f g x)) (jglue a b)
    1,2: reflexivity.
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
forall (a : A) (b : B),
ap (functor_join (h o f) (i o g)) (jglue a b) @
(fun b0 : B => 1) b =
(fun a0 : A => 1) a @
ap
  (fun x : Join A B =>
   functor_join h i (functor_join f g x)) (jglue a b)
    intros a b.
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
a: A
b: B
ap (functor_join (h o f) (i o g)) (jglue a b) @
(fun b : B => 1) b =
(fun a : A => 1) a @
ap
  (fun x : Join A B =>
   functor_join h i (functor_join f g x)) (jglue a b)
    simpl.
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
a: A
b: B
ap
  (functor_join (fun x : A => h (f x))
     (fun x : B => i (g x))) (jglue a b) @ 1 =
1 @
ap
  (fun x : Join A B =>
   functor_join h i (functor_join f g x)) (jglue a b)
    apply equiv_p1_1q.
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
a: A
b: B
ap
  (functor_join (fun x : A => h (f x))
     (fun x : B => i (g x))) (jglue a b) =
ap
  (fun x : Join A B =>
   functor_join h i (functor_join f g x)) (jglue a b)
    lhs nrapply functor_join_beta_jglue; symmetry.
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
a: A
b: B
ap
  (fun x : Join A B =>
   functor_join h i (functor_join f g x)) (jglue a b) =
jglue (h (f a)) (i (g b))
    lhs nrapply (ap_compose (functor_join f g) _ (jglue a b)).
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
a: A
b: B
ap (functor_join h i)
  (ap (functor_join f g) (jglue a b)) =
jglue (h (f a)) (i (g b))
    lhs nrefine (ap _ (functor_join_beta_jglue _ _ _ _)).
A, B, C, D, E, F: Type
f: A -> C
g: B -> D
h: C -> E
i: D -> F
a: A
b: B
ap (functor_join h i) (jglue (f a) (g b)) =
jglue (h (f a)) (i (g b))
    apply functor_join_beta_jglue.
  Defined.

  Definition functor_join_idmap {A B}
    : functor_join idmap idmap == (idmap : Join A B -> Join A B).
A, B: Type
functor_join idmap idmap ==
(idmap : Join A B -> Join A B)
  Proof.
A, B: Type
functor_join idmap idmap ==
(idmap : Join A B -> Join A B)
    snrapply Join_ind_FlFr.
A, B: Type
forall a : A,
functor_join idmap idmap (joinl a) = idmap (joinl a)
A, B: Type
forall b : B,
functor_join idmap idmap (joinr b) = idmap (joinr b)
A, B: Type
forall (a : A) (b : B),
ap (functor_join idmap idmap) (jglue a b) @ ?Hr b =
?Hl a @ ap idmap (jglue a b)
    1,2: reflexivity.
A, B: Type
forall (a : A) (b : B),
ap (functor_join idmap idmap) (jglue a b) @
(fun b0 : B => 1) b =
(fun a0 : A => 1) a @ ap idmap (jglue a b)
    intros a b.
A, B: Type
a: A
b: B
ap (functor_join idmap idmap) (jglue a b) @
(fun b : B => 1) b =
(fun a : A => 1) a @ ap idmap (jglue a b)
    simpl.
A, B: Type
a: A
b: B
ap (functor_join idmap idmap) (jglue a b) @ 1 =
1 @ ap idmap (jglue a b)
    apply equiv_p1_1q.
A, B: Type
a: A
b: B
ap (functor_join idmap idmap) (jglue a b) =
ap idmap (jglue a b)
    lhs nrapply functor_join_beta_jglue.
A, B: Type
a: A
b: B
jglue a b = ap idmap (jglue a b)
    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'.
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
functor_join f g == functor_join f' g'
  Proof.
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
functor_join f g == functor_join f' g'
    srapply Join_ind_FlFr.
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
forall a : A,
functor_join f g (joinl a) =
functor_join f' g' (joinl a)
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
forall b : B,
functor_join f g (joinr b) =
functor_join f' g' (joinr b)
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
forall (a : A) (b : B),
ap (functor_join f g) (jglue a b) @ ?Hr b =
?Hl a @ ap (functor_join f' g') (jglue a b)
    -
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
forall a : A,
functor_join f g (joinl a) =
functor_join f' g' (joinl a) simpl; intros; apply ap, h.
    -
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
forall b : B,
functor_join f g (joinr b) =
functor_join f' g' (joinr b) simpl; intros; apply ap, k.
    -
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
forall (a : A) (b : B),
ap (functor_join f g) (jglue a b) @
((fun b0 : B => ap joinr (k b0))
 :
 forall b0 : B,
 functor_join f g (joinr b0) =
 functor_join f' g' (joinr b0)) b =
((fun a0 : A => ap joinl (h a0))
 :
 forall a0 : A,
 functor_join f g (joinl a0) =
 functor_join f' g' (joinl a0)) a @
ap (functor_join f' g') (jglue a b) intros a b; cbn beta.
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
a: A
b: B
ap (functor_join f g) (jglue a b) @ ap joinr (k b) =
ap joinl (h a) @ ap (functor_join f' g') (jglue a b)
      lhs nrapply (functor_join_beta_jglue _ _ _ _ @@ 1).
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
a: A
b: B
jglue (f a) (g b) @ ap joinr (k b) =
ap joinl (h a) @ ap (functor_join f' g') (jglue a b)
      symmetry.
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
a: A
b: B
ap joinl (h a) @ ap (functor_join f' g') (jglue a b) =
jglue (f a) (g b) @ ap joinr (k b)
      lhs nrapply (1 @@ functor_join_beta_jglue _ _ _ _).
A, B, C, D: Type
f, f': A -> C
g, g': B -> D
h: f == f'
k: g == g'
a: A
b: B
ap joinl (h a) @ jglue (f' a) (g' b) =
jglue (f a) (g b) @ ap joinr (k b)
      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).
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
IsEquiv (functor_join f g)
  Proof.
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
IsEquiv (functor_join f g)
    snrapply isequiv_adjointify.
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
Join C D -> Join A B
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join f g o ?g == idmap
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
?g o functor_join f g == idmap
    -
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
Join C D -> Join A B apply (functor_join f^-1 g^-1).
    -
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join f g o functor_join f^-1 g^-1 == idmap etransitivity.
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join f g o functor_join f^-1 g^-1 == ?Goal
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
?Goal == idmap
      1: symmetry; apply functor_join_compose.
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join (fun x : C => f (f^-1 x))
  (fun x : D => g (g^-1 x)) == idmap
      etransitivity.
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join (fun x : C => f (f^-1 x))
  (fun x : D => g (g^-1 x)) == ?Goal
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
?Goal == idmap
      1: exact (functor2_join (eisretr f) (eisretr g)).
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join idmap idmap == idmap
      apply functor_join_idmap.
    -
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join f^-1 g^-1 o functor_join f g == idmap etransitivity.
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join f^-1 g^-1 o functor_join f g == ?Goal
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
?Goal == idmap
      1: symmetry; apply functor_join_compose.
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join (fun x : A => f^-1 (f x))
  (fun x : B => g^-1 (g x)) == idmap
      etransitivity.
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join (fun x : A => f^-1 (f x))
  (fun x : B => g^-1 (g x)) == ?Goal
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
?Goal == idmap
      1: exact (functor2_join (eissect f) (eissect g)).
A, B, C, D: Type
f: A -> C
IsEquiv0: IsEquiv f
g: B -> D
IsEquiv1: IsEquiv g
functor_join idmap idmap == idmap
      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) _.

  Global Instance is0bifunctor_join : Is0Bifunctor Join.
Is0Bifunctor Join
  Proof.
Is0Bifunctor Join
    snrapply Build_Is0Bifunctor'.
Is01Cat Type
Is01Cat Type
Is0Functor (uncurry Join)
    1,2: exact _.
Is0Functor (uncurry Join)
    apply Build_Is0Functor.
forall a b : Type * Type,
(a $-> b) -> uncurry Join a $-> uncurry Join b
    intros A B [f g].
A, B: (Type * Type)%type
f: fst A $-> fst B
g: snd A $-> snd B
uncurry Join A $-> uncurry Join B
    exact (functor_join f g).
  Defined.

  Global Instance is1bifunctor_join : Is1Bifunctor Join.
Is1Bifunctor Join
  Proof.
Is1Bifunctor Join
    snrapply Build_Is1Bifunctor'.
Is1Functor (uncurry Join)
    nrapply Build_Is1Functor.
forall (a b : Type * Type) (f g : a $-> b),
f $== g ->
fmap (uncurry Join) f $== fmap (uncurry Join) g
forall a : Type * Type,
fmap (uncurry Join) (Id a) $== Id (uncurry Join a)
forall (a b c : Type * Type) (f : a $-> b)
(g : b $-> c),
fmap (uncurry Join) (g $o f) $==
fmap (uncurry Join) g $o fmap (uncurry Join) f
    -
forall (a b : Type * Type) (f g : a $-> b),
f $== g ->
fmap (uncurry Join) f $== fmap (uncurry Join) g intros A B f g [p q].
A, B: (Type * Type)%type
f, g: A $-> B
p: fst f $-> fst g
q: snd f $-> snd g
fmap (uncurry Join) f $== fmap (uncurry Join) g
      exact (functor2_join p q).
    -
forall a : Type * Type,
fmap (uncurry Join) (Id a) $== Id (uncurry Join a) intros A; exact functor_join_idmap.
    -
forall (a b c : Type * Type) (f : a $-> b)
(g : b $-> c),
fmap (uncurry Join) (g $o f) $==
fmap (uncurry Join) g $o fmap (uncurry Join) f intros A B C [f g] [h k].
A, B, C: (Type * Type)%type
f: fst A $-> fst B
g: snd A $-> snd B
h: fst B $-> fst C
k: snd B $-> snd C
fmap (uncurry Join) ((h, k) $o (f, g)) $==
fmap (uncurry Join) (h, k) $o
fmap (uncurry Join) (f, g)
      exact (functor_join_compose f g h k).
  Defined.

End FunctorJoin.

(** * Symmetry of Join

  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.
A, B, P: Type
joinrecdata_0gpd A B P $-> joinrecdata_0gpd B A P
  Proof.
A, B, P: Type
joinrecdata_0gpd A B P $-> joinrecdata_0gpd B A P
    snrapply Build_Morphism_0Gpd.
A, B, P: Type
joinrecdata_0gpd A B P -> joinrecdata_0gpd B A P
A, B, P: Type
Is0Functor ?fun_0gpd
    (* The map of types [JoinRecData A B P -> JoinRecData B A P]: *)
    -
A, B, P: Type
joinrecdata_0gpd A B P -> joinrecdata_0gpd B A P intros [fl fr fg].
A, B, P: Type
fl: A -> P
fr: B -> P
fg: forall (a : A) (b : B), fl a = fr b
joinrecdata_0gpd B A P
      snrapply (Build_JoinRecData fr fl).
A, B, P: Type
fl: A -> P
fr: B -> P
fg: forall (a : A) (b : B), fl a = fr b
forall (a : B) (b : A), fr a = fl b
      intros b a; exact (fg a b)^.
    (* It respects the paths. *)
    -
A, B, P: Type
Is0Functor
  (fun X : joinrecdata_0gpd A B P =>
   (fun (fl : A -> P) (fr : B -> P)
      (fg : forall (a : A) (b : B), fl a = fr b) =>
    {|
      jl := fr;
      jr := fl;
      jg := fun (b : B) (a : A) => (fg a b)^
    |}) (jl X) (jr X) (jg X)) apply Build_Is0Functor.
A, B, P: Type
forall a b : joinrecdata_0gpd A B P,
(a $-> b) ->
{|
  jl := jr a;
  jr := jl a;
  jg := fun (b0 : B) (a0 : A) => (jg a a0 b0)^
|} $->
{|
  jl := jr b;
  jr := jl b;
  jg := fun (b0 : B) (a0 : A) => (jg b a0 b0)^
|}
      intros f g h; simpl.
A, B, P: Type
f, g: joinrecdata_0gpd A B P
h: f $-> g
JoinRecPath
  {|
    jl := jr f;
    jr := jl f;
    jg := fun (b : B) (a : A) => (jg f a b)^
  |}
  {|
    jl := jr g;
    jr := jl g;
    jg := fun (b : B) (a : A) => (jg g a b)^
  |}
      snrapply Build_JoinRecPath; simpl.
A, B, P: Type
f, g: joinrecdata_0gpd A B P
h: f $-> g
forall a : B, jr f a = jr g a
A, B, P: Type
f, g: joinrecdata_0gpd A B P
h: f $-> g
forall b : A, jl f b = jl g b
A, B, P: Type
f, g: joinrecdata_0gpd A B P
h: f $-> g
forall (a : B) (b : A),
(jg f b a)^ @ ?Goal0 b = ?Goal a @ (jg g b a)^
      1, 2: intros; apply h.
A, B, P: Type
f, g: joinrecdata_0gpd A B P
h: f $-> g
forall (a : B) (b : A),
(jg f b a)^ @ (fun b0 : A => let X := hl h in X b0) b =
(fun a0 : B => let X := hr h in X a0) a @ (jg g b a)^
      intros b a.
A, B, P: Type
f, g: joinrecdata_0gpd A B P
h: f $-> g
b: B
a: A
(jg f a b)^ @ (fun b : A => let X := hl h in X b) a =
(fun a : B => let X := hr h in X a) b @ (jg g a b)^
      square_ind g h a b.
A, B, P: Type
f: joinrecdata_0gpd A B P
b: B
a: A
(jg f a b)^ @ 1 = 1 @ (jg f 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 _.
A, B, P: Type
joinrecdata_sym B A P $o joinrecdata_sym A B P $==
Id (joinrecdata_0gpd A B P)
  Proof.
A, B, P: Type
joinrecdata_sym B A P $o joinrecdata_sym A B P $==
Id (joinrecdata_0gpd A B P)
    intro f; simpl.
A, B, P: Type
f: joinrecdata_0gpd A B P
JoinRecPath
  {|
    jl := jl f;
    jr := jr f;
    jg := fun (b : A) (a : B) => ((jg f b a)^)^
  |} f
    bundle_joinrecpath.
A, B, P: Type
f: joinrecdata_0gpd A B P
forall (a : A) (b : B),
jg
  {|
    jl := jl f;
    jr := jr f;
    jg := fun (b0 : A) (a0 : B) => ((jg f b0 a0)^)^
  |} a b = jg f a b
    intros a b; simpl.
A, B, P: Type
f: joinrecdata_0gpd A B P
a: A
b: B
((jg f a b)^)^ = jg f a b
    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).
A, B: Type
NatEquiv (joinrecdata_0gpd_fun A B)
  (joinrecdata_0gpd_fun B A)
  Proof.
A, B: Type
NatEquiv (joinrecdata_0gpd_fun A B)
  (joinrecdata_0gpd_fun B A)
    snrapply Build_NatEquiv.
A, B: Type
forall a : Type,
joinrecdata_0gpd_fun A B a $<~>
joinrecdata_0gpd_fun B A a
A, B: Type
Is1Natural (joinrecdata_0gpd_fun A B)
  (joinrecdata_0gpd_fun B A) (fun a : Type => ?e a)
    (* An equivalence of 0-groupoids for each [P]: *)
    -
A, B: Type
forall a : Type,
joinrecdata_0gpd_fun A B a $<~>
joinrecdata_0gpd_fun B A a intro P.
A, B, P: Type
joinrecdata_0gpd_fun A B P $<~>
joinrecdata_0gpd_fun B A P
      snrapply cate_adjointify.
A, B, P: Type
joinrecdata_0gpd_fun A B P $->
joinrecdata_0gpd_fun B A P
A, B, P: Type
joinrecdata_0gpd_fun B A P $->
joinrecdata_0gpd_fun A B P
A, B, P: Type
?f $o ?g $== Id (joinrecdata_0gpd_fun B A P)
A, B, P: Type
?g $o ?f $== Id (joinrecdata_0gpd_fun A B P)
      1, 2: apply joinrecdata_sym.
A, B, P: Type
joinrecdata_sym A B P $o joinrecdata_sym B A P $==
Id (joinrecdata_0gpd_fun B A P)
A, B, P: Type
joinrecdata_sym B A P $o joinrecdata_sym A B P $==
Id (joinrecdata_0gpd_fun A B P)
      1, 2: apply joinrecdata_sym_inv.
    (* Naturality: *)
    -
A, B: Type
Is1Natural (joinrecdata_0gpd_fun A B)
  (joinrecdata_0gpd_fun B A)
  (fun a : Type =>
   (fun P : Type =>
    cate_adjointify (joinrecdata_sym A B P)
      (joinrecdata_sym B A P)
      (joinrecdata_sym_inv B A P)
      (joinrecdata_sym_inv A B P)) a) intros P Q g f; simpl.
A, B, P, Q: Type
g: P $-> Q
f: joinrecdata_0gpd_fun A B P
JoinRecPath
  {|
    jl := fun x : B => g (jr f x);
    jr := fun x : A => g (jl f x);
    jg := fun (b : B) (a : A) => (ap g (jg f a b))^
  |}
  (joinrecdata_fun g
     {|
       jl := jr f;
       jr := jl f;
       jg := fun (b : B) (a : A) => (jg f a b)^
     |})
      bundle_joinrecpath.
A, B, P, Q: Type
g: P $-> Q
f: joinrecdata_0gpd_fun A B P
forall (a : B) (b : A),
jg
  {|
    jl := fun x : B => g (jr f x);
    jr := fun x : A => g (jl f x);
    jg :=
      fun (b0 : B) (a0 : A) => (ap g (jg f a0 b0))^
  |} a b =
jg
  (joinrecdata_fun g
     {|
       jl := jr f;
       jr := jl f;
       jg := fun (b0 : B) (a0 : A) => (jg f a0 b0)^
     |}) a b
      intros b a; simpl.
A, B, P, Q: Type
g: P $-> Q
f: joinrecdata_0gpd_fun A B P
b: B
a: A
(ap g (jg f a b))^ = ap g (jg f a b)^
      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.
A, B: Type
Join A B <~> Join B A
  Proof.
A, B: Type
Join A B <~> Join B A
    rapply (opyon_equiv_0gpd (A:=Type)).
A, B: Type
opyon1_0gpd (Join B A) $<~> opyon1_0gpd (Join A B)
    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.
A, B: Type
join_sym A B == equiv_join_sym' A B
  Proof.
A, B: Type
join_sym A B == equiv_join_sym' A B
    symmetry.
A, B: Type
equiv_join_sym' A B == join_sym A B
    (** Both sides are [join_rec] applied to [JoinRecData]: *)
    rapply (fmap join_rec).
A, B: Type
natequiv_compose (joinrecdata_sym_natequiv B A)
  (join_rec_inv_natequiv B A) (Join B A)
  (Id (Join B A)) $-> join_sym_recdata A B
    bundle_joinrecpath; intros; cbn.
A, B: Type
a: A
b: B
(ap idmap (jglue b a))^ = (jglue b a)^
    refine (ap inverse _).
A, B: Type
a: A
b: B
ap idmap (jglue b a) = jglue b a
    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).

  Global Instance isequiv_join_sym A B : IsEquiv (join_sym A B)
    := equiv_isequiv (equiv_join_sym A B).

  (** 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.
A, B: Type
join_sym A B o join_sym B A == idmap
  Proof.
A, B: Type
join_sym A B o join_sym B A == idmap
    snrapply (Join_ind_FFlr (join_sym B A)).
A, B: Type
forall a : B,
join_sym A B (join_sym B A (joinl a)) = joinl a
A, B: Type
forall b : A,
join_sym A B (join_sym B A (joinr b)) = joinr b
A, B: Type
forall (a : B) (b : A),
ap (join_sym A B) (ap (join_sym B A) (jglue a b)) @
?Hr b = ?Hl a @ jglue a b
    -
A, B: Type
forall a : B,
join_sym A B (join_sym B A (joinl a)) = joinl a reflexivity.
    -
A, B: Type
forall b : A,
join_sym A B (join_sym B A (joinr b)) = joinr b reflexivity.
    -
A, B: Type
forall (a : B) (b : A),
ap (join_sym A B) (ap (join_sym B A) (jglue a b)) @
(fun b0 : A => 1) b = (fun a0 : B => 1) a @ jglue a b intros a b; cbn beta.
A, B: Type
a: B
b: A
ap (join_sym A B) (ap (join_sym B A) (jglue a b)) @ 1 =
1 @ jglue a b
      apply equiv_p1_1q.
A, B: Type
a: B
b: A
ap (join_sym A B) (ap (join_sym B A) (jglue a b)) =
jglue a b
      refine (ap _ (join_rec_beta_jg _ a b) @ _); cbn.
A, B: Type
a: B
b: A
ap (join_sym A B) (jglue b a)^ = jglue a b
      refine (ap_V _ (jglue b a) @ _).
A, B: Type
a: B
b: A
(ap (join_sym A B) (jglue b a))^ = jglue a b
      refine (ap inverse (join_rec_beta_jg _ b a) @ _).
A, B: Type
a: B
b: A
(jg (join_sym_recdata A B) b a)^ = jglue a b
      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. *)

  (** We give a direct proof that [join_sym] is natural. *)
  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.
A, B, A', B': Type
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.
A, B, A', B': Type
f: A -> A'
g: B -> B'
join_sym A' B' o functor_join f g ==
functor_join g f o join_sym A B
    snrapply Join_ind_FlFr.
A, B, A', B': Type
f: A -> A'
g: B -> B'
forall a : A,
(fun x : Join A B =>
 join_sym A' B' (functor_join f g x)) (joinl a) =
(fun x : Join A B => functor_join g f (join_sym A B x))
  (joinl a)
A, B, A', B': Type
f: A -> A'
g: B -> B'
forall b : B,
(fun x : Join A B =>
 join_sym A' B' (functor_join f g x)) (joinr b) =
(fun x : Join A B => functor_join g f (join_sym A B x))
  (joinr b)
A, B, A', B': Type
f: A -> A'
g: B -> B'
forall (a : A) (b : B),
ap
  (fun x : Join A B =>
   join_sym A' B' (functor_join f g x)) (jglue a b) @
?Hr b =
?Hl a @
ap
  (fun x : Join A B =>
   functor_join g f (join_sym A B x)) (jglue a b)
    1, 2: reflexivity.
A, B, A', B': Type
f: A -> A'
g: B -> B'
forall (a : A) (b : B),
ap
  (fun x : Join A B =>
   join_sym A' B' (functor_join f g x)) (jglue a b) @
(fun b0 : B => 1) b =
(fun a0 : A => 1) a @
ap
  (fun x : Join A B =>
   functor_join g f (join_sym A B x)) (jglue a b)
    intros a b; cbn beta.
A, B, A', B': Type
f: A -> A'
g: B -> B'
a: A
b: B
ap
  (fun x : Join A B =>
   join_sym A' B' (functor_join f g x)) (jglue a b) @
1 =
1 @
ap
  (fun x : Join A B =>
   functor_join g f (join_sym A B x)) (jglue a b)
    apply equiv_p1_1q.
A, B, A', B': Type
f: A -> A'
g: B -> B'
a: A
b: B
ap
  (fun x : Join A B =>
   join_sym A' B' (functor_join f g x)) (jglue a b) =
ap
  (fun x : Join A B =>
   functor_join g f (join_sym A B x)) (jglue a b)
    lhs nrefine (ap_compose' (functor_join f g) _ (jglue a b)).
A, B, A', B': Type
f: A -> A'
g: B -> B'
a: A
b: B
ap (join_sym A' B')
  (ap (functor_join f g) (jglue a b)) =
ap
  (fun x : Join A B =>
   functor_join g f (join_sym A B x)) (jglue a b)
    lhs nrefine (ap _ (functor_join_beta_jglue _ _ _ _)).
A, B, A', B': Type
f: A -> A'
g: B -> B'
a: A
b: B
ap (join_sym A' B') (jglue (f a) (g b)) =
ap
  (fun x : Join A B =>
   functor_join g f (join_sym A B x)) (jglue a b)
    lhs nrapply join_sym_beta_jglue.
A, B, A', B': Type
f: A -> A'
g: B -> B'
a: A
b: B
(jglue (g b) (f a))^ =
ap
  (fun x : Join A B =>
   functor_join g f (join_sym A B x)) (jglue a b)
    symmetry.
A, B, A', B': Type
f: A -> A'
g: B -> B'
a: A
b: B
ap
  (fun x : Join A B =>
   functor_join g f (join_sym A B x)) (jglue a b) =
(jglue (g b) (f a))^
    lhs nrefine (ap_compose' (join_sym A B) _ (jglue a b)).
A, B, A', B': Type
f: A -> A'
g: B -> B'
a: A
b: B
ap (functor_join g f) (ap (join_sym A B) (jglue a b)) =
(jglue (g b) (f a))^
    lhs nrefine (ap _ (join_sym_beta_jglue a b)).
A, B, A', B': Type
f: A -> A'
g: B -> B'
a: A
b: B
ap (functor_join g f) (jglue b a)^ =
(jglue (g b) (f a))^
    refine (ap_V _ (jglue b a) @ ap inverse _).
A, B, A', B': Type
f: A -> A'
g: B -> B'
a: A
b: B
ap (functor_join g f) (jglue b a) = jglue (g b) (f a)
    apply functor_join_beta_jglue.
  Defined.

End JoinSym.

(** * Other miscellaneous results about joins *)

(** 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).
A, B: Type
Contr0: Contr A
Contr (Join A B)
  Proof.
A, B: Type
Contr0: Contr A
Contr (Join A B)
    apply (Build_Contr _ (joinl (center A))).
A, B: Type
Contr0: Contr A
forall y : Join A B, joinl (center A) = y
    snrapply Join_ind.
A, B: Type
Contr0: Contr A
forall a : A, joinl (center A) = joinl a
A, B: Type
Contr0: Contr A
forall b : B, joinl (center A) = joinr b
A, B: Type
Contr0: Contr A
forall (a : A) (b : B),
transport (paths (joinl (center A))) 
  (jglue a b) (?P_A a) = 
?P_B b
    -
A, B: Type
Contr0: Contr A
forall a : A, joinl (center A) = joinl a intros a; apply ap, contr.
    -
A, B: Type
Contr0: Contr A
forall b : B, joinl (center A) = joinr b intros b; apply jglue.
    -
A, B: Type
Contr0: Contr A
forall (a : A) (b : B),
transport (paths (joinl (center A))) (jglue a b)
  ((fun a0 : A => ap joinl (contr a0)) a) =
(fun b0 : B => jglue (center A) b0) b intros a b; cbn.
A, B: Type
Contr0: Contr A
a: A
b: B
transport (paths (joinl (center A))) (jglue a b)
  (ap joinl (contr a)) = jglue (center A) b
      lhs nrapply transport_paths_r.
A, B: Type
Contr0: Contr A
a: A
b: B
ap joinl (contr a) @ jglue a b = jglue (center A) b
      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).
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
IsHProp (Join A B)
  Proof.
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
IsHProp (Join A B)
    apply hprop_inhabited_contr.
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
Join A B -> Contr (Join A B)
    snrapply Join_rec.
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
A -> Contr (Join A B)
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
B -> Contr (Join A B)
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
forall (a : A) (b : B), ?P_A a = ?P_B b
    -
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
A -> Contr (Join A B) intros a; apply contr_join.
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
a: A
Contr A
      exact (contr_inhabited_hprop A a).
    -
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
B -> Contr (Join A B) intros b; refine (contr_equiv (Join B A) (equiv_join_sym B A)).
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
b: B
Contr (Join B A)
      apply contr_join.
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
b: B
Contr B
      exact (contr_inhabited_hprop B b).
    (* The two proofs of contractibility are equal because [Contr] is an [HProp].  This uses [Funext]. *)
    -
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
forall (a : A) (b : B),
(fun a0 : A => contr_join A B) a =
(fun b0 : B =>
 contr_equiv (Join B A) (equiv_join_sym B A)) b 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).
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
(Join A B -> P) <~> (B -> P)
  Proof.
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
(Join A B -> P) <~> (B -> P)
    apply equiv_iff_hprop.
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
(Join A B -> P) -> B -> P
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
(B -> P) -> Join A B -> P
    1: exact (fun f => f o joinr).
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
(B -> P) -> Join A B -> P
    intros g.
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
g: B -> P
Join A B -> P
    snrapply Join_rec.
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
g: B -> P
A -> P
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
g: B -> P
B -> P
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
g: B -> P
forall (a : A) (b : B), ?P_A a = ?P_B b
    1,2: assumption.
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
g: B -> P
forall (a : A) (b : B), f a = g b
    intros a b.
H: Funext
A, B, P: Type
IsHProp0: IsHProp P
f: A -> P
g: B -> P
a: A
b: B
f a = g 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.
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
Join A B <~> hor A B
  Proof.
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
Join A B <~> hor A B
    apply equiv_iff_hprop.
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
Join A B -> hor A B
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
hor A B -> Join A B
    -
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
Join A B -> hor A B exact (Join_rec (fun a => tr (inl a)) (fun b => tr (inr b)) (fun _ _ => path_ishprop _ _)).
    -
H: Funext
A, B: Type
IsHProp0: IsHProp A
IsHProp1: IsHProp B
hor A B -> Join A B apply Trunc_rec, push.
  Defined.

  (** Joins add connectivity *)
  Global Instance isconnected_join `{Funext} {m n : trunc_index}
         (A B : Type) `{IsConnected m A} `{IsConnected n B}
    : IsConnected (m +2+ n) (Join A B).
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
IsConnected (Tr (m +2+ n)) (Join A B)
  Proof.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
IsConnected (Tr (m +2+ n)) (Join A B)
    apply isconnected_from_elim; intros C ? k.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
NullHomotopy k
    pose @istrunc_inO_tr.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
NullHomotopy k
    pose proof (istrunc_extension_along_conn
                  (fun b:B => tt) (fun _ => C) (k o joinr)).
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  (ExtensionAlong (fun _ : B => tt) (unit_name C)
     (k o joinr))
NullHomotopy k
    unfold ExtensionAlong in *.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
NullHomotopy k
    transparent assert (f : (A -> {s : Unit -> C &
                                   forall x, s tt = k (joinr x)})).
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= ?Goal: A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
NullHomotopy k
    {
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)} intros a; exists (fun _ => k (joinl a)); intros b.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
a: A
b: B
k (joinl a) = k (joinr b)
      exact (ap k (jglue a b)). }
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
NullHomotopy k
    assert (h := isconnected_elim
                   m {s : Unit -> C & forall x : B, s tt = k (joinr x)} f).
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
h: NullHomotopy f
NullHomotopy k
    unfold NullHomotopy in *; destruct h as [[c g] h].
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
{y : C & forall x : Join A B, k x = y}
    exists (c tt).
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
forall x : Join A B, k x = c tt
    snrapply Join_ind.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
forall a : A,
(fun x : Join A B => k x = c tt) (joinl a)
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
forall b : B,
(fun x : Join A B => k x = c tt) (joinr b)
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
forall (a : A) (b : B),
transport (fun x : Join A B => k x = c tt) (jglue a b)
  (?P_A a) = ?P_B b
    -
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
forall a : A,
(fun x : Join A B => k x = c tt) (joinl a) intros a; cbn.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
a: A
k (joinl a) = c tt exact (ap10 (h a)..1 tt).
    -
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
forall b : B,
(fun x : Join A B => k x = c tt) (joinr b) intros b; cbn.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
b: B
k (joinr b) = c tt exact ((g b)^).
    -
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
forall (a : A) (b : B),
transport (fun x : Join A B => k x = c tt) (jglue a b)
  ((fun a0 : A =>
    ap10 (h a0) ..1 tt
    :
    (fun x : Join A B => k x = c tt) (joinl a0)) a) =
(fun b0 : B =>
 (g b0)^ : (fun x : Join A B => k x = c tt) (joinr b0))
  b intros a b.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
a: A
b: B
transport (fun x : Join A B => k x = c tt) (jglue a b)
  ((fun a : A =>
    ap10 (h a) ..1 tt
    :
    (fun x : Join A B => k x = c tt) (joinl a)) a) =
(fun b : B =>
 (g b)^ : (fun x : Join A B => k x = c tt) (joinr b))
  b
      rewrite transport_paths_FlFr, ap_const, concat_p1; cbn.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: In (Tr (m +2+ n)) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
In (Tr n) A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
f:= fun a : A =>
(unit_name (k (joinl a));
fun b : B => ap k (jglue a b)): A ->
{s : Unit -> C & forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
h: forall x : A, f x = (c; g)
a: A
b: B
(ap k (jglue a b))^ @ ap10 (h a) ..1 tt = (g b)^
      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 *.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: IsTrunc (m +2+ n) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
IsTrunc n A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
a: A
b: B
ha1: unit_name (k (joinl a)) = c
ha2: transport (fun s : Unit -> C => forall x : B, s tt = k (joinr x)) ha1
(fun b : B => ap k (jglue a b)) = g
(ap k (jglue a b))^ @ ap10 ha1 tt = (g b)^
      rewrite <- (inv_V (ap10 ha1 tt)).
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: IsTrunc (m +2+ n) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
IsTrunc n A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
a: A
b: B
ha1: unit_name (k (joinl a)) = c
ha2: transport (fun s : Unit -> C => forall x : B, s tt = k (joinr x)) ha1
(fun b : B => ap k (jglue a b)) = g
(ap k (jglue a b))^ @ ((ap10 ha1 tt)^)^ = (g b)^
      rewrite <- inv_pp.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: IsTrunc (m +2+ n) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
IsTrunc n A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
a: A
b: B
ha1: unit_name (k (joinl a)) = c
ha2: transport (fun s : Unit -> C => forall x : B, s tt = k (joinr x)) ha1
(fun b : B => ap k (jglue a b)) = g
((ap10 ha1 tt)^ @ ap k (jglue a b))^ = (g b)^
      apply inverse2.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: IsTrunc (m +2+ n) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
IsTrunc n A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
a: A
b: B
ha1: unit_name (k (joinl a)) = c
ha2: transport (fun s : Unit -> C => forall x : B, s tt = k (joinr x)) ha1
(fun b : B => ap k (jglue a b)) = g
(ap10 ha1 tt)^ @ ap k (jglue a b) = g b
      refine (_ @ apD10 ha2 b); clear ha2.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: IsTrunc (m +2+ n) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
IsTrunc n A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
a: A
b: B
ha1: unit_name (k (joinl a)) = c
(ap10 ha1 tt)^ @ ap k (jglue a b) =
transport
  (fun s : Unit -> C =>
   forall x : B, s tt = k (joinr x)) ha1
  (fun b : B => ap k (jglue a b)) b
      rewrite transport_forall_constant, transport_paths_FlFr.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: IsTrunc (m +2+ n) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
IsTrunc n A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
a: A
b: B
ha1: unit_name (k (joinl a)) = c
(ap10 ha1 tt)^ @ ap k (jglue a b) =
((ap (fun x : Unit -> C => x tt) ha1)^ @
 ap k (jglue a b)) @
ap (fun _ : Unit -> C => k (joinr b)) ha1
      rewrite ap_const, concat_p1.
H: Funext
m, n: trunc_index
A, B: Type
H0: IsConnected (Tr m) A
H1: IsConnected (Tr n) B
C: Type
H2: IsTrunc (m +2+ n) C
k: Join A B -> C
i:= @istrunc_inO_tr: forall (n : trunc_index) (A : Type),
IsTrunc n A -> IsTrunc n A
X: IsTrunc m
  {s : Unit -> C &
  forall x : B, s tt = k (joinr x)}
c: Unit -> C
g: forall x : B, c tt = k (joinr x)
a: A
b: B
ha1: unit_name (k (joinl a)) = c
(ap10 ha1 tt)^ @ ap k (jglue a b) =
(ap (fun x : Unit -> C => x tt) ha1)^ @
ap k (jglue a b)
      reflexivity.
  Defined.

End JoinTrunc.

(** Join with Empty *)
Section JoinEmpty.

  Definition equiv_join_empty_right A : Join A Empty <~> A.
A: Type
Join A Empty <~> A
  Proof.
A: Type
Join A Empty <~> A
    snrapply equiv_adjointify.
A: Type
Join A Empty -> A
A: Type
A -> Join A Empty
A: Type
?f o ?g == idmap
A: Type
?g o ?f == idmap
    -
A: Type
Join A Empty -> A apply join_rec; snrapply (Build_JoinRecData idmap); contradiction.
    -
A: Type
A -> Join A Empty exact joinl.
    -
A: Type
join_rec
  {|
    jl := idmap;
    jr :=
      fun H : Empty =>
      Empty_rect (fun _ : Empty => A) H;
    jg :=
      fun (a : A) (b : Empty) =>
      Empty_rect
        (fun b0 : Empty =>
         a = Empty_rect (fun _ : Empty => A) b0) b
  |} o joinl == idmap reflexivity.
    -
A: Type
joinl
o join_rec
    {|
      jl := idmap;
      jr :=
        fun H : Empty =>
        Empty_rect (fun _ : Empty => A) H;
      jg :=
        fun (a : A) (b : Empty) =>
        Empty_rect
          (fun b0 : Empty =>
           a = Empty_rect (fun _ : Empty => A) b0) b
    |} == idmap snrapply Join_ind; [reflexivity| |]; contradiction.
  Defined.

  Definition equiv_join_empty_left A : Join Empty A <~> A
    := equiv_join_empty_right _ oE equiv_join_sym _ _.

  Global Instance join_right_unitor : RightUnitor Join Empty.
RightUnitor Join Empty
  Proof.
RightUnitor Join Empty
    snrapply Build_NatEquiv.
forall a : Type, flip Join Empty a $<~> idmap a
Is1Natural (flip Join Empty) idmap
  (fun a : Type => ?e a)
    -
forall a : Type, flip Join Empty a $<~> idmap a apply equiv_join_empty_right.
    -
Is1Natural (flip Join Empty) idmap
  (fun a : Type => equiv_join_empty_right a) intros A B f.
A, B: Type
f: A $-> B
equiv_join_empty_right B $o fmap (flip Join Empty) f $==
fmap idmap f $o equiv_join_empty_right A
      cbn -[equiv_join_empty_right].
A, B: Type
f: A $-> B
(fun x : flip Join Empty A =>
 equiv_join_empty_right B (functor_join f idmap x)) ==
(fun x : flip Join Empty A =>
 f (equiv_join_empty_right A x))
      snrapply Join_ind_FlFr.
A, B: Type
f: A $-> B
forall a : A,
(fun x : flip Join Empty A =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinl a) =
(fun x : flip Join Empty A =>
 f (equiv_join_empty_right A x)) (joinl a)
A, B: Type
f: A $-> B
forall b : Empty,
(fun x : flip Join Empty A =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinr b) =
(fun x : flip Join Empty A =>
 f (equiv_join_empty_right A x)) (joinr b)
A, B: Type
f: A $-> B
forall (a : A) (b : Empty),
ap
  (fun x : flip Join Empty A =>
   equiv_join_empty_right B (functor_join f idmap x))
  (jglue a b) @ ?Hr b =
?Hl a @
ap
  (fun x : flip Join Empty A =>
   f (equiv_join_empty_right A x)) (jglue a b)
      +
A, B: Type
f: A $-> B
forall a : A,
(fun x : flip Join Empty A =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinl a) =
(fun x : flip Join Empty A =>
 f (equiv_join_empty_right A x)) (joinl a) intro a.
A, B: Type
f: A $-> B
a: A
(fun x : flip Join Empty A =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinl a) =
(fun x : flip Join Empty A =>
 f (equiv_join_empty_right A x)) (joinl a)
        reflexivity.
      +
A, B: Type
f: A $-> B
forall b : Empty,
(fun x : flip Join Empty A =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinr b) =
(fun x : flip Join Empty A =>
 f (equiv_join_empty_right A x)) (joinr b) intros [].
      +
A, B: Type
f: A $-> B
forall (a : A) (b : Empty),
ap
  (fun x : flip Join Empty A =>
   equiv_join_empty_right B (functor_join f idmap x))
  (jglue a b) @
(fun b0 : Empty =>
 match
   b0 as e
   return
     (equiv_join_empty_right B
        (functor_join f idmap (joinr e)) =
      f (equiv_join_empty_right A (joinr e)))
 with
 end) b =
(fun a0 : A => 1) a @
ap
  (fun x : flip Join Empty A =>
   f (equiv_join_empty_right A x)) (jglue a b) intros a [].
  Defined.

  Global Instance join_left_unitor : LeftUnitor Join Empty.
LeftUnitor Join Empty
  Proof.
LeftUnitor Join Empty
    snrapply Build_NatEquiv.
forall a : Type, Join Empty a $<~> idmap a
Is1Natural (Join Empty) idmap (fun a : Type => ?e a)
    -
forall a : Type, Join Empty a $<~> idmap a apply equiv_join_empty_left.
    -
Is1Natural (Join Empty) idmap
  (fun a : Type => equiv_join_empty_left a) intros A B f x.
A, B: Type
f: A $-> B
x: Join Empty A
(equiv_join_empty_left B $o fmap (Join Empty) f) x =
(fmap idmap f $o equiv_join_empty_left A) x
      cbn -[equiv_join_empty_right].
A, B: Type
f: A $-> B
x: Join Empty A
equiv_join_empty_right B
  (join_sym Empty B (functor_join idmap f x)) =
f (equiv_join_empty_right A (join_sym Empty A x))
      rhs_V rapply (isnat_natequiv join_right_unitor).
A, B: Type
f: A $-> B
x: Join Empty A
equiv_join_empty_right B
  (join_sym Empty B (functor_join idmap f x)) =
(join_right_unitor B $o fmap (flip Join Empty) f)
  (join_sym Empty A x)
      cbn -[equiv_join_empty_right].
A, B: Type
f: A $-> B
x: Join Empty A
equiv_join_empty_right B
  (join_sym Empty B (functor_join idmap f x)) =
equiv_join_empty_right B
  (functor_join f idmap (join_sym Empty A x))
      apply ap, join_sym_nat.
  Defined.

End JoinEmpty.

Arguments equiv_join_empty_right : simpl never.

(** Iterated Join powers of a type. *)
Section JoinPower.

  (** The join of [n.+1] copies of a type. This is convenient because it produces [A] definitionally when [n] is [0]. We annotate the universes to reduce universe variables. *)
  Definition iterated_join (A : Type@{u}) (n : nat) : Type@{u}
    := nat_iter n (Join A) A.

  (** The join of [n] copies of a type. This is sometimes convenient for proofs by induction as it gives a trivial base case. *)
  Definition join_power (A : Type@{u}) (n : nat) : Type@{u}
    := nat_iter n (Join A) (Empty : Type@{u}).

  Definition equiv_join_powers (A : Type) (n : nat) : join_power A n.+1 <~> iterated_join A n.
A: Type
n: nat
join_power A n.+1 <~> iterated_join A n
  Proof.
A: Type
n: nat
join_power A n.+1 <~> iterated_join A n
    induction n as [|n IHn]; simpl.
A: Type
Join A Empty <~> A
A: Type
n: nat
IHn: join_power A n.+1 <~> iterated_join A n
Join A (Join A (join_power A n)) <~>
Join A (iterated_join A n)
    -
A: Type
Join A Empty <~> A exact (equiv_join_empty_right A).
    -
A: Type
n: nat
IHn: join_power A n.+1 <~> iterated_join A n
Join A (Join A (join_power A n)) <~>
Join A (iterated_join A n) exact (equiv_functor_join equiv_idmap IHn).
  Defined.

End JoinPower.