From HoTT Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Cubical.DPath Cubical.PathSquare.
Require Import Homotopy.NullHomotopy.
Require Import Extensions.
Require Import Colimits.Pushout.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Pointed.Core.
From HoTT.WildCat Require Import Core Universe Equiv EquivGpd
  ZeroGroupoid Yoneda FunctorCat NatTrans Bifunctor Monoidal.
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
    snapply (Join_ind _ Hl 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
    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.

  Definition Join_ind_Flr {A B : Type} (f : Join A B -> Join A B)
    (Hl : forall a, f (joinl a) = joinl a)
    (Hr : forall b, f (joinr b) = joinr b)
    (Hglue : forall a b, ap f (jglue a b) @ Hr b = Hl a @ jglue a b)
    : forall x, f x = x.
A, B: Type
f: Join A B -> Join A B
Hl: forall a : A, f (joinl a) = joinl a
Hr: forall b : B, f (joinr b) = joinr b
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b = Hl a @ jglue a b
forall x : Join A B, f x = x
  Proof.
A, B: Type
f: Join A B -> Join A B
Hl: forall a : A, f (joinl a) = joinl a
Hr: forall b : B, f (joinr b) = joinr b
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b = Hl a @ jglue a b
forall x : Join A B, f x = x
    snapply (Join_ind _ Hl Hr).
A, B: Type
f: Join A B -> Join A B
Hl: forall a : A, f (joinl a) = joinl a
Hr: forall b : B, f (joinr b) = joinr b
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b = Hl a @ jglue a b
forall (a : A) (b : B),
transport (fun x : Join A B => f x = x) (jglue a b)
  (Hl a) = Hr b
    intros a b.
A, B: Type
f: Join A B -> Join A B
Hl: forall a : A, f (joinl a) = joinl a
Hr: forall b : B, f (joinr b) = joinr b
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b = Hl a @ jglue a b
a: A
b: B
transport (fun x : Join A B => f x = x) (jglue a b)
  (Hl a) = Hr b
    transport_paths Flr.
A, B: Type
f: Join A B -> Join A B
Hl: forall a : A, f (joinl a) = joinl a
Hr: forall b : B, f (joinr b) = joinr b
Hglue: forall (a : A) (b : B),
ap f (jglue a b) @ Hr b = Hl a @ jglue a b
a: A
b: B
ap f (jglue a b) @ Hr b = Hl a @ 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
    snapply (Join_ind _ Hl 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
    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_ind_FFlFr {A B C P : Type}
    (f : Join A B -> C) (g : C -> P) (h : Join A B -> P)
    (Hl : forall a, g (f (joinl a)) = h (joinl a))
    (Hr : forall b, g (f (joinr b)) = h (joinr b))
    (Hglue : forall a b, ap g (ap f (jglue a b)) @ Hr b = Hl a @ ap h (jglue a b))
    : g o f == h.
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, g (f (joinl a)) = h (joinl a)
Hr: forall b : B, g (f (joinr b)) = h (joinr b)
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ ap h (jglue a b)
g o f == h
  Proof.
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, g (f (joinl a)) = h (joinl a)
Hr: forall b : B, g (f (joinr b)) = h (joinr b)
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ ap h (jglue a b)
g o f == h
    snapply (Join_ind _ Hl Hr).
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, g (f (joinl a)) = h (joinl a)
Hr: forall b : B, g (f (joinr b)) = h (joinr b)
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ ap h (jglue a b)
forall (a : A) (b : B),
transport (fun x : Join A B => (g o f) x = h x)
  (jglue a b) (Hl a) = Hr b
    intros a b; cbn beta.
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, g (f (joinl a)) = h (joinl a)
Hr: forall b : B, g (f (joinr b)) = h (joinr b)
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ ap h (jglue a b)
a: A
b: B
transport (fun x : Join A B => g (f x) = h x)
  (jglue a b) (Hl a) = Hr b
    transport_paths FFlFr.
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, g (f (joinl a)) = h (joinl a)
Hr: forall b : B, g (f (joinr b)) = h (joinr b)
Hglue: forall (a : A) (b : B),
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ ap h (jglue a b)
a: A
b: B
ap g (ap f (jglue a b)) @ Hr b =
Hl a @ ap h (jglue a b)
    apply Hglue.
  Defined.

  Definition Join_ind_FlFFr {A B C P : Type}
    (f : Join A B -> C) (g : C -> P) (h : Join A B -> P)
    (Hl : forall a, h (joinl a) = g (f (joinl a)))
    (Hr : forall b, h (joinr b) = g (f (joinr b)))
    (Hglue : forall a b, ap h (jglue a b) @ Hr b = Hl a @ ap g (ap f (jglue a b)))
    : h == g o f.
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, h (joinl a) = g (f (joinl a))
Hr: forall b : B, h (joinr b) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap h (jglue a b) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
h == g o f
  Proof.
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, h (joinl a) = g (f (joinl a))
Hr: forall b : B, h (joinr b) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap h (jglue a b) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
h == g o f
    snapply (Join_ind _ Hl Hr).
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, h (joinl a) = g (f (joinl a))
Hr: forall b : B, h (joinr b) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap h (jglue a b) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
forall (a : A) (b : B),
transport (fun x : Join A B => h x = (g o f) x)
  (jglue a b) (Hl a) = Hr b
    intros a b; cbn beta.
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, h (joinl a) = g (f (joinl a))
Hr: forall b : B, h (joinr b) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap h (jglue a b) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
a: A
b: B
transport (fun x : Join A B => h x = g (f x))
  (jglue a b) (Hl a) = Hr b
    transport_paths FlFFr.
A, B, C, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> P
Hl: forall a : A, h (joinl a) = g (f (joinl a))
Hr: forall b : B, h (joinr b) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap h (jglue a b) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
a: A
b: B
ap h (jglue a b) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
    apply Hglue.
  Defined.

  Definition Join_ind_FFlFFr {A B C D P : Type}
    (f : Join A B -> C) (g : C -> P) (h : Join A B -> D) (i : D -> P)
    (Hl : forall a, i (h (joinl a)) = g (f (joinl a)))
    (Hr : forall b, i (h (joinr b)) = g (f (joinr b)))
    (Hglue : forall a b, ap i (ap h (jglue a b)) @ Hr b = Hl a @ ap g (ap f (jglue a b)))
    : i o h == g o f.
A, B, C, D, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> D
i: D -> P
Hl: forall a : A, i (h (joinl a)) = g (f (joinl a))
Hr: forall b : B, i (h (joinr b)) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap i (ap h (jglue a b)) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
i o h == g o f
  Proof.
A, B, C, D, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> D
i: D -> P
Hl: forall a : A, i (h (joinl a)) = g (f (joinl a))
Hr: forall b : B, i (h (joinr b)) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap i (ap h (jglue a b)) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
i o h == g o f
    snapply (Join_ind _ Hl Hr).
A, B, C, D, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> D
i: D -> P
Hl: forall a : A, i (h (joinl a)) = g (f (joinl a))
Hr: forall b : B, i (h (joinr b)) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap i (ap h (jglue a b)) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
forall (a : A) (b : B),
transport (fun x : Join A B => (i o h) x = (g o f) x)
  (jglue a b) (Hl a) = Hr b
    intros a b; cbn beta.
A, B, C, D, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> D
i: D -> P
Hl: forall a : A, i (h (joinl a)) = g (f (joinl a))
Hr: forall b : B, i (h (joinr b)) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap i (ap h (jglue a b)) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
a: A
b: B
transport (fun x : Join A B => i (h x) = g (f x))
  (jglue a b) (Hl a) = Hr b
    transport_paths FFlFFr.
A, B, C, D, P: Type
f: Join A B -> C
g: C -> P
h: Join A B -> D
i: D -> P
Hl: forall a : A, i (h (joinl a)) = g (f (joinl a))
Hr: forall b : B, i (h (joinr b)) = g (f (joinr b))
Hglue: forall (a : A) (b : B),
ap i (ap h (jglue a b)) @ Hr b =
Hl a @ ap g (ap f (jglue a b))
a: A
b: B
ap i (ap h (jglue a b)) @ Hr b =
Hl a @ ap g (ap f (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
    exact (Pushout_rec_beta_pglue _ _ _ _ (a, b)).
  Defined.

  (** If [A] is pointed, 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] _.

(** ** Zigzags in joins *)

(** These paths are very common, so we give them names and prove a few results about them. *)
Definition zigzag {A B : Type} (a a' : A) (b : B)
  : joinl a = joinl a'
  := jglue a b @ (jglue a' b)^.

Definition zagzig {A B : Type} (a : A) (b b' : B)
  : joinr b = joinr b'
  := (jglue a b)^ @ jglue a b'.

Definition zigzag_zigzag {A B : Type} (a a' : A) (b : B)
  : zigzag a a' b @ zigzag a' a b = 1
  := concat_pp_p _ _ _ @ (1 @@ concat_V_pp _ _) @ concat_pV _.

Definition zigzag_inv {A B : Type} (a a' : A) (b : B)
  : (zigzag a a' b)^ = zigzag a' a b
  := inv_pp _ _ @ (inv_V _ @@ 1).

(** And we give a beta rule for zigzags. *)
Definition Join_rec_beta_zigzag {A B P : Type} (P_A : A -> P)
  (P_B : B -> P) (P_g : forall a b, P_A a = P_B b) a a' b
  : ap (Join_rec P_A P_B P_g) (zigzag a a' b) = P_g 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': A
b: B
ap (Join_rec P_A P_B P_g) (zigzag a a' b) =
P_g 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': A
b: B
ap (Join_rec P_A P_B P_g) (zigzag a a' b) =
P_g a b @ (P_g a' b)^
  lhs napply ap_pV.
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': A
b: B
ap (Join_rec P_A P_B P_g) (jglue a b) @
(ap (Join_rec P_A P_B P_g) (jglue a' b))^ =
P_g a b @ (P_g a' b)^
  exact (Join_rec_beta_jglue _ _ _ a b @@ inverse2 (Join_rec_beta_jglue _ _ _ a' b)).
Defined.

(** * [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
  snapply 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 |}
  snapply 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. *)
Instance isgraph_joinrecdata (A B P : Type) : IsGraph (JoinRecData A B P)
  := {| Hom := JoinRecPath |}.

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
    snapply 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.

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
  snapply 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. *)
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
  snapply 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). *)
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
  exact (Build_Fun01 (joinrecdata_fun g)).
Defined.

(** [joinrecdata_0gpd A B] is a 1-functor from [Type] to [ZeroGpd]. *)
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)
    snapply 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: Graph.graph_carrier
  (zerogpd_graph (joinrecdata_0gpd A B P))
JoinRecPath (joinrecdata_fun idmap f) f
    bundle_joinrecpath; intros; cbn.
A, B, P: Type
f: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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) 
  snapply 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)
  snapply 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 : Graph.graph_carrier
       (zerogpd_graph (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
: Graph.graph_carrier
    (zerogpd_graph (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 : Graph.graph_carrier
       (zerogpd_graph (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. *)
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.

(** We restate the previous two results using [Join_rec] for convenience. *)
Definition Join_rec_homotopic (A B : Type) {P : Type}
  (fl  : A -> P) (fr  : B -> P) (fg  : forall a b, fl  a = fr  b)
  (fl' : A -> P) (fr' : B -> P) (fg' : forall a b, fl' a = fr' b)
  (hl : forall a, fl a = fl' a)
  (hr : forall b, fr b = fr' b)
  (hg : forall a b, fg a b @ hr b = hl a @ fg' a b)
  : Join_rec fl fr fg == Join_rec fl' fr' fg'
  := fmap join_rec (Build_JoinRecPath _ _ _
      {| jl:=fl; jr:=fr; jg:=fg |} {| jl:=fl'; jr:=fr'; jg:=fg' |} hl hr hg).

Definition Join_rec_nat (A B : Type) {P Q : Type} (g : P -> Q)
  (fl : A -> P) (fr : B -> P) (fg : forall a b, fl a = fr b)
  : Join_rec (g o fl) (g o fr) (fun a b => ap g (fg a b)) == g o Join_rec fl fr fg
  := join_rec_nat _ _ g {| jl:=fl; jr:=fr; jg:=fg |}.

(** * 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')
    : zigzag a a' b = ap joinl p.
A, B: Type
a, a': A
b: B
p: a = a'
zigzag a a' b = ap joinl p
  Proof.
A, B: Type
a, a': A
b: B
p: a = a'
zigzag a a' b = ap joinl p
    destruct p.
A, B: Type
a: A
b: B
zigzag a 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')
    : zagzig a b b' = ap joinr p.
A, B: Type
a: A
b, b': B
p: b = b'
zagzig a b b' = ap joinr p
  Proof.
A, B: Type
a: A
b, b': B
p: b = b'
zagzig a b b' = ap joinr p
    destruct p.
A, B: Type
a: A
b: B
zagzig a b 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 napply 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')
    : zigzag a a' b = zigzag a a' b'.
A, B: Type
a, a': A
b, b': B
p: a = a'
zigzag a a' b = zigzag a a' b'
  Proof.
A, B: Type
a, a': A
b, b': B
p: a = a'
zigzag a a' b = zigzag a a' b'
    destruct p.
A, B: Type
a: A
b, b': B
zigzag a a b = zigzag a 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')
    : zigzag a a' b = zigzag a a' b'
    := ap (zigzag a a') p.

  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 (ap (zigzag a a) 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_beta_zigzag {A B C D : Type} (f : A -> C) (g : B -> D)
    (a a' : A) (b : B)
    : ap (functor_join f g) (zigzag a a' b) = zigzag (f a) (f a') (g b)
    := Join_rec_beta_zigzag _ _ _ a 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
    snapply Join_ind_FlFFr.
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) =
functor_join h i (functor_join f g (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) =
functor_join h i (functor_join f g (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 (functor_join h i)
  (ap (functor_join f g) (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 (functor_join h i)
  (ap (functor_join f g) (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 (functor_join h i)
  (ap (functor_join f g) (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 (functor_join h i)
  (ap (functor_join f g) (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 (functor_join h i)
  (ap (functor_join f g) (jglue a b))
    lhs napply 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 (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))
    napply (functor_join_beta_jglue _ _ (f a) (g b)).
  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)
    snapply 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 napply 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 napply (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 napply (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.

  #[export] 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)
    snapply 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 exact (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
      exact 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) _.

  #[export] Instance is0bifunctor_join : Is0Bifunctor Join.
Is0Bifunctor Join
  Proof.
Is0Bifunctor Join
    snapply 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.

  #[export] Instance is1bifunctor_join : Is1Bifunctor Join.
Is1Bifunctor Join
  Proof.
Is1Bifunctor Join
    snapply Build_Is1Bifunctor'.
Is1Functor (uncurry Join)
    napply 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 warm-up 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
    snapply Build_Fun01'.
A, B, P: Type
Graph.graph_carrier
  (zerogpd_graph (joinrecdata_0gpd A B P)) ->
Graph.graph_carrier
  (zerogpd_graph (joinrecdata_0gpd B A P))
A, B, P: Type
forall
a
 b : Graph.graph_carrier
       (zerogpd_graph (joinrecdata_0gpd A B P)),
(a $-> b) -> ?F a $-> ?F b
    (* The map of types [JoinRecData A B P -> JoinRecData B A P]: *)
    -
A, B, P: Type
Graph.graph_carrier
  (zerogpd_graph (joinrecdata_0gpd A B P)) ->
Graph.graph_carrier
  (zerogpd_graph (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
Graph.graph_carrier
  (zerogpd_graph (joinrecdata_0gpd B A P))
      snapply (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
forall
a
 b : Graph.graph_carrier
       (zerogpd_graph (joinrecdata_0gpd A B P)),
(a $-> b) ->
(fun
   X : Graph.graph_carrier
         (zerogpd_graph (joinrecdata_0gpd A B P)) =>
 (fun (fl : A -> P) (fr : B -> P)
    (fg : forall (a0 : A) (b0 : B), fl a0 = fr b0) =>
  {|
    jl := fr;
    jr := fl;
    jg := fun (b0 : B) (a0 : A) => (fg a0 b0)^
  |}) (jl X) (jr X) (jg X)) a $->
(fun
   X : Graph.graph_carrier
         (zerogpd_graph (joinrecdata_0gpd A B P)) =>
 (fun (fl : A -> P) (fr : B -> P)
    (fg : forall (a0 : A) (b0 : B), fl a0 = fr b0) =>
  {|
    jl := fr;
    jr := fl;
    jg := fun (b0 : B) (a0 : A) => (fg a0 b0)^
  |}) (jl X) (jr X) (jg X)) b intros f g h; simpl.
A, B, P: Type
f, g: Graph.graph_carrier
  (zerogpd_graph (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)^
  |}
      snapply Build_JoinRecPath; simpl.
A, B, P: Type
f, g: Graph.graph_carrier
  (zerogpd_graph (joinrecdata_0gpd A B P))
h: f $-> g
forall a : B, jr f a = jr g a
A, B, P: Type
f, g: Graph.graph_carrier
  (zerogpd_graph (joinrecdata_0gpd A B P))
h: f $-> g
forall b : A, jl f b = jl g b
A, B, P: Type
f, g: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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)
    snapply 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
      snapply 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) snapply Build_Is1Natural.
A, B: Type
forall (a a' : Type) (f : a $-> a'),
(fun a0 : Type =>
 cate_fun
   ((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)) a0)) a' $o
fmap (joinrecdata_0gpd A B) f $==
fmap (joinrecdata_0gpd B A) f $o
(fun a0 : Type =>
 cate_fun
   ((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)) a0)) a
      intros P Q g f; simpl.
A, B, P, Q: Type
g: P $-> Q
f: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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: Graph.graph_carrier
  (zerogpd_graph (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
    tapply (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]: *)
    tapply (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).

  #[export] 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
    snapply (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
    snapply Join_ind_FFlFFr.
A, B, A', B': Type
f: A -> A'
g: B -> B'
forall a : A,
join_sym A' B' (functor_join f g (joinl a)) =
functor_join g f (join_sym A B (joinl a))
A, B, A', B': Type
f: A -> A'
g: B -> B'
forall b : B,
join_sym A' B' (functor_join f g (joinr b)) =
functor_join g f (join_sym A B (joinr b))
A, B, A', B': Type
f: A -> A'
g: B -> B'
forall (a : A) (b : B),
ap (join_sym A' B')
  (ap (functor_join f g) (jglue a b)) @ ?Hr b =
?Hl a @
ap (functor_join g f) (ap (join_sym A B) (jglue a b))
    1, 2: reflexivity.
A, B, A', B': Type
f: A -> A'
g: B -> B'
forall (a : A) (b : B),
ap (join_sym A' B')
  (ap (functor_join f g) (jglue a b)) @
(fun b0 : B => 1) b =
(fun a0 : A => 1) a @
ap (functor_join g f) (ap (join_sym A B) (jglue a b))
    intros a b; cbn beta.
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)) @ 1 =
1 @
ap (functor_join g f) (ap (join_sym A B) (jglue a b))
    apply equiv_p1_1q.
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 (functor_join g f) (ap (join_sym A B) (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 (functor_join g f) (ap (join_sym A B) (jglue a b))
    lhs napply 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 (functor_join g f) (ap (join_sym A B) (jglue a b))
    symmetry.
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 *)
  #[export] 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
    snapply 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 napply 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 *)
  #[export] 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)
    snapply 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
    snapply 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 *)
  #[export] 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
    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
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
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
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
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
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 : NullHomotopy 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
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 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
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
    {
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
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 f rapply (isconnected_elim m).
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
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)}
In (Tr m)
  {s : Unit -> C & forall x : B, s tt = k (joinr x)}
      rapply (istrunc_extension_along_conn (n:=n)). }
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
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
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
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
    snapply 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
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
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
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
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 beta.
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
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
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 beta.
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
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
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
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
      transport_paths Fl.
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
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
ap10 (h a) ..1 tt = ap k (jglue a b) @ (g b)^
      apply moveL_pV, moveR_Mp.
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
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
g b = (ap10 (h a) ..1 tt)^ @ ap k (jglue a b)
      lhs_V napply (apD10 (h a)..2 b); simpl.
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
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 s : Unit -> C =>
   forall x : B, s tt = k (joinr x)) (h a) ..1
  (fun b : B => ap k (jglue a b)) b =
(ap10 (h a) ..1 tt)^ @ ap k (jglue a b)
      lhs napply transport_forall_constant.
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
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 : Unit -> C => x tt = k (joinr b))
  (h a) ..1 (ap k (jglue a b)) =
(ap10 (h a) ..1 tt)^ @ ap k (jglue a b)
      napply transport_paths_Fl.
  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
    snapply 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; snapply (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 snapply Join_ind; [reflexivity| |]; contradiction.
  Defined.

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

  #[export] Instance join_right_unitor : RightUnitor Join Empty.
RightUnitor Join Empty
  Proof.
RightUnitor Join Empty
    snapply 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 exact equiv_join_empty_right.
    -
Is1Natural (flip Join Empty) idmap
  (fun a : Type => equiv_join_empty_right a) snapply Build_Is1Natural.
forall (a a' : Type) (f : a $-> a'),
(fun a0 : Type => cate_fun (equiv_join_empty_right a0))
  a' $o fmap (flip Join Empty) f $==
fmap idmap f $o
(fun a0 : Type => cate_fun (equiv_join_empty_right a0))
  a
      intros A B f.
A, B: Type
f: A $-> B
(fun a : Type => cate_fun (equiv_join_empty_right a))
  B $o fmap (flip Join Empty) f $==
fmap idmap f $o
(fun a : Type => cate_fun (equiv_join_empty_right a))
  A
      cbn -[equiv_join_empty_right].
A, B: Type
f: A $-> B
(fun x : Join A Empty =>
 equiv_join_empty_right B (functor_join f idmap x)) ==
(fun x : Join A Empty =>
 f (equiv_join_empty_right A x))
      snapply Join_ind_FlFr.
A, B: Type
f: A $-> B
forall a : A,
(fun x : Join A Empty =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinl a) =
(fun x : Join A Empty =>
 f (equiv_join_empty_right A x)) (joinl a)
A, B: Type
f: A $-> B
forall b : Empty,
(fun x : Join A Empty =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinr b) =
(fun x : Join A Empty =>
 f (equiv_join_empty_right A x)) (joinr b)
A, B: Type
f: A $-> B
forall (a : A) (b : Empty),
ap
  (fun x : Join A Empty =>
   equiv_join_empty_right B (functor_join f idmap x))
  (jglue a b) @ ?Hr b =
?Hl a @
ap
  (fun x : Join A Empty =>
   f (equiv_join_empty_right A x)) (jglue a b)
      +
A, B: Type
f: A $-> B
forall a : A,
(fun x : Join A Empty =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinl a) =
(fun x : Join A Empty =>
 f (equiv_join_empty_right A x)) (joinl a) intro a.
A, B: Type
f: A $-> B
a: A
(fun x : Join A Empty =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinl a) =
(fun x : Join A Empty =>
 f (equiv_join_empty_right A x)) (joinl a)
        reflexivity.
      +
A, B: Type
f: A $-> B
forall b : Empty,
(fun x : Join A Empty =>
 equiv_join_empty_right B (functor_join f idmap x))
  (joinr b) =
(fun x : Join A Empty =>
 f (equiv_join_empty_right A x)) (joinr b) intros [].
      +
A, B: Type
f: A $-> B
forall (a : A) (b : Empty),
ap
  (fun x : Join A Empty =>
   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 : Join A Empty =>
   f (equiv_join_empty_right A x)) (jglue a b) intros a [].
  Defined.

  #[export] Instance join_left_unitor : LeftUnitor Join Empty.
LeftUnitor Join Empty
  Proof.
LeftUnitor Join Empty
    snapply 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 exact equiv_join_empty_left.
    -
Is1Natural (Join Empty) idmap
  (fun a : Type => equiv_join_empty_left a) snapply Build_Is1Natural.
forall (a a' : Type) (f : a $-> a'),
(fun a0 : Type => cate_fun (equiv_join_empty_left a0))
  a' $o fmap (Join Empty) f $==
fmap idmap f $o
(fun a0 : Type => cate_fun (equiv_join_empty_left a0))
  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.

(** ** Double recursion for Join *)

Section Rec2.
  Context {A B C D : Type} (P : Type)
    (P_AC : A -> C -> P) (P_AD : A -> D -> P) (P_BC : B -> C -> P) (P_BD : B -> D -> P)
    (P_gAx : forall a c d, P_AC a c = P_AD a d)
    (P_gBx : forall b c d, P_BC b c = P_BD b d)
    (P_gxC : forall c a b, P_AC a c = P_BC b c)
    (P_gxD : forall d a b, P_AD a d = P_BD b d)
    (P_g : forall a b c d, P_gAx a c d @ P_gxD d a b = P_gxC c a b @ P_gBx b c d).

  Definition Join_rec2 : Join A B -> Join C D -> P.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
Join A B -> Join C D -> P
  Proof.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
Join A B -> Join C D -> P
    intros x y; revert x.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
y: Join C D
Join A B -> P
    snapply Join_rec.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
y: Join C D
A -> P
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
y: Join C D
B -> P
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
y: Join C D
forall (a : A) (b : B), ?P_A a = ?P_B b
    1: intros a; exact (Join_rec (P_AC a) (P_AD a) (P_gAx a) y).
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
y: Join C D
B -> P
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
y: Join C D
forall (a : A) (b : B),
(fun a0 : A =>
 Join_rec (P_AC a0) (P_AD a0) (P_gAx a0) y) a = 
?P_B b
    1: intros b; exact (Join_rec (P_BC b) (P_BD b) (P_gBx b) y).
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
y: Join C D
forall (a : A) (b : B),
(fun a0 : A =>
 Join_rec (P_AC a0) (P_AD a0) (P_gAx a0) y) a =
(fun b0 : B =>
 Join_rec (P_BC b0) (P_BD b0) (P_gBx b0) y) b
    intros a b.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
y: Join C D
a: A
b: B
(fun a : A => Join_rec (P_AC a) (P_AD a) (P_gAx a) y)
  a =
(fun b : B => Join_rec (P_BC b) (P_BD b) (P_gBx b) y)
  b
    revert y.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
forall y : Join C D,
(fun a : A => Join_rec (P_AC a) (P_AD a) (P_gAx a) y)
  a =
(fun b : B => Join_rec (P_BC b) (P_BD b) (P_gBx b) y)
  b
    snapply Join_ind_FlFr.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
forall a0 : C,
(fun x : Join C D =>
 (fun a : A => Join_rec (P_AC a) (P_AD a) (P_gAx a) x)
   a) (joinl a0) =
(fun x : Join C D =>
 (fun b : B => Join_rec (P_BC b) (P_BD b) (P_gBx b) x)
   b) (joinl a0)
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
forall b0 : D,
(fun x : Join C D =>
 (fun a : A => Join_rec (P_AC a) (P_AD a) (P_gAx a) x)
   a) (joinr b0) =
(fun x : Join C D =>
 (fun b : B => Join_rec (P_BC b) (P_BD b) (P_gBx b) x)
   b) (joinr b0)
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
forall (a0 : C) (b0 : D),
ap
  (fun x : Join C D =>
   (fun a : A =>
    Join_rec (P_AC a) (P_AD a) (P_gAx a) x) a)
  (jglue a0 b0) @ ?Hr b0 =
?Hl a0 @
ap
  (fun x : Join C D =>
   (fun b : B =>
    Join_rec (P_BC b) (P_BD b) (P_gBx b) x) b)
  (jglue a0 b0)
    1: intros c; exact (P_gxC c a b).
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
forall b0 : D,
(fun x : Join C D =>
 (fun a : A => Join_rec (P_AC a) (P_AD a) (P_gAx a) x)
   a) (joinr b0) =
(fun x : Join C D =>
 (fun b : B => Join_rec (P_BC b) (P_BD b) (P_gBx b) x)
   b) (joinr b0)
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
forall (a0 : C) (b0 : D),
ap
  (fun x : Join C D =>
   (fun a : A =>
    Join_rec (P_AC a) (P_AD a) (P_gAx a) x) a)
  (jglue a0 b0) @ ?Hr b0 =
(fun c : C => P_gxC c a b) a0 @
ap
  (fun x : Join C D =>
   (fun b : B =>
    Join_rec (P_BC b) (P_BD b) (P_gBx b) x) b)
  (jglue a0 b0)
    1: intros d; exact (P_gxD d a b).
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
forall (a0 : C) (b0 : D),
ap
  (fun x : Join C D =>
   (fun a : A =>
    Join_rec (P_AC a) (P_AD a) (P_gAx a) x) a)
  (jglue a0 b0) @ (fun d : D => P_gxD d a b) b0 =
(fun c : C => P_gxC c a b) a0 @
ap
  (fun x : Join C D =>
   (fun b : B =>
    Join_rec (P_BC b) (P_BD b) (P_gBx b) x) b)
  (jglue a0 b0)
    intros c d.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
c: C
d: D
ap
  (fun x : Join C D =>
   (fun a : A =>
    Join_rec (P_AC a) (P_AD a) (P_gAx a) x) a)
  (jglue c d) @ (fun d : D => P_gxD d a b) d =
(fun c : C => P_gxC c a b) c @
ap
  (fun x : Join C D =>
   (fun b : B =>
    Join_rec (P_BC b) (P_BD b) (P_gBx b) x) b)
  (jglue c d)
    simpl.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
c: C
d: D
ap
  (fun x : Join C D =>
   Join_rec (P_AC a) (P_AD a) (P_gAx a) x) (jglue c d) @
P_gxD d a b =
P_gxC c a b @
ap
  (fun x : Join C D =>
   Join_rec (P_BC b) (P_BD b) (P_gBx b) x) (jglue c d)
    lhs napply whiskerR.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
c: C
d: D
ap
  (fun x : Join C D =>
   Join_rec (P_AC a) (P_AD a) (P_gAx a) x) (jglue c d) =
?Goal
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
c: C
d: D
?Goal @ P_gxD d a b =
P_gxC c a b @
ap
  (fun x : Join C D =>
   Join_rec (P_BC b) (P_BD b) (P_gBx b) x) 
  (jglue c d)
    1: apply Join_rec_beta_jglue.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
c: C
d: D
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @
ap
  (fun x : Join C D =>
   Join_rec (P_BC b) (P_BD b) (P_gBx b) x) (jglue c d)
    rhs napply whiskerL.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
c: C
d: D
P_gAx a c d @ P_gxD d a b = P_gxC c a b @ ?Goal
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
c: C
d: D
ap
  (fun x : Join C D =>
   Join_rec (P_BC b) (P_BD b) (P_gBx b) x) 
  (jglue c d) = ?Goal
    2: apply Join_rec_beta_jglue.
A, B, C, D, P: Type
P_AC: A -> C -> P
P_AD: A -> D -> P
P_BC: B -> C -> P
P_BD: B -> D -> P
P_gAx: forall (a : A) (c : C) (d : D),
P_AC a c = P_AD a d
P_gBx: forall (b : B) (c : C) (d : D),
P_BC b c = P_BD b d
P_gxC: forall (c : C) (a : A) (b : B),
P_AC a c = P_BC b c
P_gxD: forall (d : D) (a : A) (b : B),
P_AD a d = P_BD b d
P_g: forall (a : A) (b : B) (c : C) 
(d : D),
P_gAx a c d @ P_gxD d a b =
P_gxC c a b @ P_gBx b c d
a: A
b: B
c: C
d: D
P_gAx a c d @ P_gxD d a b = P_gxC c a b @ P_gBx b c d
    exact (P_g a b c d).
  Defined.

End Rec2.