JoinAssoc.v

Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** * The associativity of [Join]

  We use the recursion principle for the triple join (from TriJoin.v) to prove the associativity of Join.  We'll use the common technique of combining symmetry and a twist equivalence.  Temporarily writing * for Join, symmetry says that [A * B <~> B * A] and the twist says that [A * (B * C) <~> B * (A * C)].  From these we get a composite equivalence [A * (B * C) <~> A * (C * B) <~> C * (A * B) <~> (A * B) * C].  One advantage of this approach is that both symmetry and the twist are their own inverses, so there are fewer maps to define and fewer composites to prove are homotopic to the identity. Symmetry is proved in Join/Core.v. *)

(** ** The twist equivalence [TriJoin A B C <~> TriJoin B A C]

  We prove the twist equivalence using the Yoneda lemma.  The idea is that [TriJoin A B C -> P] is equivalent (as a 0-groupoid) to [TriJoinRecData A B C P], and the latter is very symmetrical by construction, which makes it easy to show that it is equivalent to [TriJoinRecData B A C P].  Going back along the first equivalence gets us to [TriJoin B A C -> P].  These equivalences are natural in [P], so the twist equivalence follows from the Yoneda lemma. *)

(** First we define a map of 0-groupoids that will underlie the natural equivalence. *)
Definition trijoinrecdata_twist (A B C P : Type)
  : trijoinrecdata_0gpd A B C P $-> trijoinrecdata_0gpd B A C P.A, B, C, P: Type
trijoinrecdata_0gpd A B C P $->
trijoinrecdata_0gpd B A C P
Proof.A, B, C, P: Type
trijoinrecdata_0gpd A B C P $->
trijoinrecdata_0gpd B A C P
  snrapply Build_Morphism_0Gpd.A, B, C, P: Type
trijoinrecdata_0gpd A B C P ->
trijoinrecdata_0gpd B A C P
A, B, C, P: Type
Is0Functor ?fun_0gpd
  (* The map of types [TriJoinRecData A B C P -> TriJoinRecData B A C P]: *)
  -A, B, C, P: Type
trijoinrecdata_0gpd A B C P ->
trijoinrecdata_0gpd B A C P cbn.A, B, C, P: Type
TriJoinRecData A B C P -> TriJoinRecData B A C P
    intros [f1 f2 f3 f12 f13 f23 f123].A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
TriJoinRecData B A C P
    snrapply (Build_TriJoinRecData f2 f1 f3).A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
forall (a : B) (b : A), f2 a = f1 b
A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
forall (a : B) (c : C), f2 a = f3 c
A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
forall (b : A) (c : C), f1 b = f3 c
A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
forall (a : B) (b : A) (c : C),
?j12 a b @ ?j23 b c = ?j13 a c
    +A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
forall (a : B) (b : A), f2 a = f1 b intros b a; exact (f12 a b)^.
    +A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
forall (a : B) (c : C), f2 a = f3 c exact f23.
    +A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
forall (b : A) (c : C), f1 b = f3 c exact f13.
    +A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
forall (a : B) (b : A) (c : C),
(fun (b0 : B) (a0 : A) => (f12 a0 b0)^) a b @ f13 b c =
f23 a c intros a b c; cbn beta.A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
a: B
b: A
c: C
(f12 b a)^ @ f13 b c = f23 a c
      apply moveR_Vp.A, B, C, P: Type
f1: A -> P
f2: B -> P
f3: C -> P
f12: forall (a : A) (b : B), f1 a = f2 b
f13: forall (a : A) (c : C), f1 a = f3 c
f23: forall (b : B) (c : C), f2 b = f3 c
f123: forall (a : A) (b : B) (c : C),
f12 a b @ f23 b c = f13 a c
a: B
b: A
c: C
f13 b c = f12 b a @ f23 a c
      symmetry; apply f123.
  (* It respects the paths. *)
  -A, B, C, P: Type
Is0Functor
  ((fun X : TriJoinRecData A B C P =>
    (fun (f1 : A -> P) (f2 : B -> P) 
       (f3 : C -> P)
       (f12 : forall (a : A) (b : B), f1 a = f2 b)
       (f13 : forall (a : A) (c : C), f1 a = f3 c)
       (f23 : forall (b : B) (c : C), f2 b = f3 c)
       (f123 : forall (a : A) 
               (b : B) (c : C),
               f12 a b @ f23 b c = f13 a c) =>
     {|
       j1 := f2;
       j2 := f1;
       j3 := f3;
       j12 := fun (b : B) (a : A) => (f12 a b)^;
       j13 := f23;
       j23 := f13;
       j123 :=
         fun (a : B) (b : A) (c : C) =>
         moveR_Vp (f13 b c) 
           (f23 a c) (f12 b a) 
           (f123 b a c)^
         :
         (fun (b0 : B) (a0 : A) => (f12 a0 b0)^) a b @
         f13 b c = f23 a c
     |}) (j1 X) (j2 X) (j3 X) 
      (j12 X) (j13 X) (j23 X) 
      (j123 X))
   :
   trijoinrecdata_0gpd A B C P ->
   trijoinrecdata_0gpd B A C P) apply Build_Is0Functor.A, B, C, P: Type
forall a b : trijoinrecdata_0gpd A B C P,
(a $-> b) ->
{|
  j1 := j2 a;
  j2 := j1 a;
  j3 := j3 a;
  j12 := fun (b0 : B) (a0 : A) => (j12 a a0 b0)^;
  j13 := j23 a;
  j23 := j13 a;
  j123 :=
    fun (a0 : B) (b0 : A) (c : C) =>
    moveR_Vp (j13 a b0 c) 
      (j23 a a0 c) (j12 a b0 a0) 
      (j123 a b0 a0 c)^
|} $->
{|
  j1 := j2 b;
  j2 := j1 b;
  j3 := j3 b;
  j12 := fun (b0 : B) (a0 : A) => (j12 b a0 b0)^;
  j13 := j23 b;
  j23 := j13 b;
  j123 :=
    fun (a0 : B) (b0 : A) (c : C) =>
    moveR_Vp (j13 b b0 c) 
      (j23 b a0 c) (j12 b b0 a0) 
      (j123 b b0 a0 c)^
|}
    intros f g h; cbn in *.A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
TriJoinRecPath
  {|
    j1 := j2 f;
    j2 := j1 f;
    j3 := j3 f;
    j12 := fun (b : B) (a : A) => (j12 f a b)^;
    j13 := j23 f;
    j23 := j13 f;
    j123 :=
      fun (a : B) (b : A) (c : C) =>
      moveR_Vp (j13 f b c) 
        (j23 f a c) (j12 f b a) 
        (j123 f b a c)^
  |}
  {|
    j1 := j2 g;
    j2 := j1 g;
    j3 := j3 g;
    j12 := fun (b : B) (a : A) => (j12 g a b)^;
    j13 := j23 g;
    j23 := j13 g;
    j123 :=
      fun (a : B) (b : A) (c : C) =>
      moveR_Vp (j13 g b c) 
        (j23 g a c) (j12 g b a) 
        (j123 g b a c)^
  |}
    snrapply Build_TriJoinRecPath; intros; simpl.A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
j2 f a = j2 g a
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
b: A
j1 f b = j1 g b
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
c: C
j3 f c = j3 g c
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
b: A
(j12 f b a)^ @ ?Goal0 = ?Goal @ (j12 g b a)^
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
c: C
j23 f a c @ ?Goal1 = ?Goal @ j23 g a c
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
b: A
c: C
j13 f b c @ ?Goal1 = ?Goal0 @ j13 g b c
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
b: A
c: C
prism
  (moveR_Vp (j13 f b c) (j23 f a c) 
     (j12 f b a) (j123 f b a c)^)
  (moveR_Vp (j13 g b c) (j23 g a c) 
     (j12 g b a) (j123 g b a c)^) 
  ?Goal2 ?Goal3 ?Goal4
    1, 2, 3, 5, 6: apply h.A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
b: A
(j12 f b a)^ @ (let X := h1 h in X b) =
(let X := h2 h in X a) @ (j12 g b a)^
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
b: A
c: C
prism
  (moveR_Vp (j13 f b c) (j23 f a c) 
     (j12 f b a) (j123 f b a c)^)
  (moveR_Vp (j13 g b c) (j23 g a c) 
     (j12 g b a) (j123 g b a c)^) 
  ?Goal (let X := h23 h in X a c)
  (let X := h13 h in X b c)
    +A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
b: A
(j12 f b a)^ @ (let X := h1 h in X b) =
(let X := h2 h in X a) @ (j12 g b a)^ cbn zeta.A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
b: A
(j12 f b a)^ @ h1 h b = h2 h a @ (j12 g b a)^
      prism_ind_two g h b a _X_; cbn beta.A, B, C, P: Type
f: TriJoinRecData A B C P
a: B
b: A
(j12 f b a)^ @ 1 = 1 @ (j12 f b a)^
      apply concat_p1_1p.
    +A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
b: A
c: C
prism
  (moveR_Vp (j13 f b c) (j23 f a c) 
     (j12 f b a) (j123 f b a c)^)
  (moveR_Vp (j13 g b c) (j23 g a c) 
     (j12 g b a) (j123 g b a c)^)
  ((fun (H : forall a : A, j1 f a = j1 g a)
      (H0 : forall b : B, j2 f b = j2 g b)
      (H1 : forall c : C, j3 f c = j3 g c)
      (H2 : forall (a : A) 
            (b : B),
            j12 f a b @ H0 b = H a @ j12 g a b)
      (H3 : forall (a : A) 
            (c : C),
            j13 f a c @ H1 c = H a @ j13 g a c)
      (H4 : forall (b : B) 
            (c : C),
            j23 f b c @ H1 c = H0 b @ j23 g b c)
      (H5 : forall (a : A) 
            (b : B) (c : C),
            prism (j123 f a b c) 
              (j123 g a b c) 
              (H2 a b) (H3 a c) 
              (H4 b c)) =>
    (fun (H6 : A -> P) (H7 : B -> P) 
       (H8 : C -> P)
       (H9 : forall (a : A) (b : B), H6 a = H7 b)
       (H10 : forall (a : A) (c : C), H6 a = H8 c)
       (H11 : forall (b : B) (c : C), H7 b = H8 c)
       (H12 : forall (a : A) 
              (b : B) (c : C),
              H9 a b @ H11 b c = H10 a c) =>
     square_ind (j1 f b) 
       (j2 f a) (j12 f b a)
       (fun (a' b' : P) (ab' : a' = b')
          (ha : j1 f b = a') 
          (hb : j2 f a = b')
          (_ : j12 f b a @ hb = ha @ ab') =>
        (j12 f b a)^ @ ha = hb @ ab'^)
       (concat_p1_1p (j12 f b a)^
        :
        (j12 f b a)^ @ 1 = 1 @ (j12 f b a)^) 
       (H6 b) (H7 a) (H9 b a)
     :
     forall
     (p : j1 f b =
          j1
            {|
              j1 := H6;
              j2 := H7;
              j3 := H8;
              j12 := H9;
              j13 := H10;
              j23 := H11;
              j123 := H12
            |} b)
     (p0 : j2 f a =
           j2
             {|
               j1 := H6;
               j2 := H7;
               j3 := H8;
               j12 := H9;
               j13 := H10;
               j23 := H11;
               j123 := H12
             |} a),
     j12 f b a @ p0 =
     p @
     j12
       {|
         j1 := H6;
         j2 := H7;
         j3 := H8;
         j12 := H9;
         j13 := H10;
         j23 := H11;
         j123 := H12
       |} b a -> (j12 f b a)^ @ p = p0 @ (H9 b a)^)
      (j1 g) (j2 g) (j3 g) 
      (j12 g) (j13 g) (j23 g) 
      (j123 g) (H b) (H0 a) 
      (H2 b a)
    :
    (j12 f b a)^ @
    h1
      {|
        h1 := H;
        h2 := H0;
        h3 := H1;
        h12 := H2;
        h13 := H3;
        h23 := H4;
        h123 := H5
      |} b =
    h2
      {|
        h1 := H;
        h2 := H0;
        h3 := H1;
        h12 := H2;
        h13 := H3;
        h23 := H4;
        h123 := H5
      |} a @ (j12 g b a)^) 
     (h1 h) (h2 h) (h3 h) 
     (h12 h) (h13 h) (h23 h) 
     (h123 h)
   :
   (j12 f b a)^ @ (let X := h1 h in X b) =
   (let X := h2 h in X a) @ (j12 g b a)^)
  (let X := h23 h in X a c) 
  (let X := h13 h in X b c) cbn beta zeta.A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: TriJoinRecPath f g
a: B
b: A
c: C
prism
  (moveR_Vp (j13 f b c) (j23 f a c) 
     (j12 f b a) (j123 f b a c)^)
  (moveR_Vp (j13 g b c) (j23 g a c) 
     (j12 g b a) (j123 g b a c)^)
  (square_ind (j1 f b) (j2 f a) 
     (j12 f b a)
     (fun (a' b' : P) (ab' : a' = b')
        (ha : j1 f b = a') 
        (hb : j2 f a = b')
        (_ : j12 f b a @ hb = ha @ ab') =>
      (j12 f b a)^ @ ha = hb @ ab'^)
     (concat_p1_1p (j12 f b a)^) 
     (j1 g b) (j2 g a) (j12 g b a) 
     (h1 h b) (h2 h a) (h12 h b a)) 
  (h23 h a c) (h13 h b c)
      prism_ind g h b a c; cbn beta.A, B, C, P: Type
f: TriJoinRecData A B C P
a: B
b: A
c: C
prism
  (moveR_Vp (j13 f b c) (j23 f a c) 
     (j12 f b a) (j123 f b a c)^)
  (moveR_Vp (j13 f b c) (j23 f a c) 
     (j12 f b a) (j123 f b a c)^)
  (square_ind (j1 f b) (j2 f a) 
     (j12 f b a)
     (fun (a' b' : P) (ab' : a' = b')
        (ha : j1 f b = a') 
        (hb : j2 f a = b')
        (_ : j12 f b a @ hb = ha @ ab') =>
      (j12 f b a)^ @ ha = hb @ ab'^)
     (concat_p1_1p (j12 f b a)^) 
     (j1 f b) (j2 f a) (j12 f b a) 1 1 
     (equiv_p1_1q 1)) (equiv_p1_1q 1) 
  (equiv_p1_1q 1)
      by triangle_ind f b a c.
Defined.

(** This map is its own inverse in the 1-category of 0-groupoids. *)
Definition trijoinrecdata_twist_inv (A B C P : Type)
  : trijoinrecdata_twist B A C P $o trijoinrecdata_twist A B C P $== Id _.A, B, C, P: Type
trijoinrecdata_twist B A C P $o
trijoinrecdata_twist A B C P $==
Id (trijoinrecdata_0gpd A B C P)
Proof.A, B, C, P: Type
trijoinrecdata_twist B A C P $o
trijoinrecdata_twist A B C P $==
Id (trijoinrecdata_0gpd A B C P)
  intro f; simpl.A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
TriJoinRecPath
  {|
    j1 := j1 f;
    j2 := j2 f;
    j3 := j3 f;
    j12 := fun (b : A) (a : B) => ((j12 f b a)^)^;
    j13 := j13 f;
    j23 := j23 f;
    j123 :=
      fun (a : A) (b : B) (c : C) =>
      moveR_Vp (j23 f b c) (j13 f a c) (j12 f a b)^
        (moveR_Vp (j13 f a c) (j23 f b c) (j12 f a b)
           (j123 f a b c)^)^
  |} f
  bundle_trijoinrecpath.A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
forall (a : A) (b : B),
j12'
  (unbundle_trijoinrecdata
     {|
       j1 := j1 f;
       j2 := j2 f;
       j3 := j3 f;
       j12 :=
         fun (b0 : A) (a0 : B) => ((j12 f b0 a0)^)^;
       j13 := j13 f;
       j23 := j23 f;
       j123 :=
         fun (a0 : A) (b0 : B) (c : C) =>
         moveR_Vp (j23 f b0 c) (j13 f a0 c)
           (j12 f a0 b0)^
           (moveR_Vp (j13 f a0 c) (j23 f b0 c)
              (j12 f a0 b0) (j123 f a0 b0 c)^)^
     |}) a b = j12' (unbundle_trijoinrecdata f) a b
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
forall (a : A) (c : C),
j13'
  (unbundle_trijoinrecdata
     {|
       j1 := j1 f;
       j2 := j2 f;
       j3 := j3 f;
       j12 := fun (b : A) (a0 : B) => ((j12 f b a0)^)^;
       j13 := j13 f;
       j23 := j23 f;
       j123 :=
         fun (a0 : A) (b : B) (c0 : C) =>
         moveR_Vp (j23 f b c0) (j13 f a0 c0)
           (j12 f a0 b)^
           (moveR_Vp (j13 f a0 c0) (j23 f b c0)
              (j12 f a0 b) (j123 f a0 b c0)^)^
     |}) a c = j13' (unbundle_trijoinrecdata f) a c
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
forall (b : B) (c : C),
j23'
  (unbundle_trijoinrecdata
     {|
       j1 := j1 f;
       j2 := j2 f;
       j3 := j3 f;
       j12 := fun (b0 : A) (a : B) => ((j12 f b0 a)^)^;
       j13 := j13 f;
       j23 := j23 f;
       j123 :=
         fun (a : A) (b0 : B) (c0 : C) =>
         moveR_Vp (j23 f b0 c0) (j13 f a c0)
           (j12 f a b0)^
           (moveR_Vp (j13 f a c0) (j23 f b0 c0)
              (j12 f a b0) (j123 f a b0 c0)^)^
     |}) b c = j23' (unbundle_trijoinrecdata f) b c
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
forall (a : A) (b : B) (c : C),
prism'
  (j123'
     (unbundle_trijoinrecdata
        {|
          j1 := j1 f;
          j2 := j2 f;
          j3 := j3 f;
          j12 :=
            fun (b0 : A) (a0 : B) => ((j12 f b0 a0)^)^;
          j13 := j13 f;
          j23 := j23 f;
          j123 :=
            fun (a0 : A) (b0 : B) (c0 : C) =>
            moveR_Vp (j23 f b0 c0) (j13 f a0 c0)
              (j12 f a0 b0)^
              (moveR_Vp (j13 f a0 c0) (j23 f b0 c0)
                 (j12 f a0 b0) (j123 f a0 b0 c0)^)^
        |}) a b c)
  (j123' (unbundle_trijoinrecdata f) a b c)
  (?h12' a b) (?h13' a c) (?h23' b c)
  all: intros; cbn.A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
b: B
((j12 f a b)^)^ = j12 f a b
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
c: C
j13 f a c = j13 f a c
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
b: B
c: C
j23 f b c = j23 f b c
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
b: B
c: C
prism'
  (moveR_Vp (j23 f b c) (j13 f a c) (j12 f a b)^
     (moveR_Vp (j13 f a c) (j23 f b c) (j12 f a b)
        (j123 f a b c)^)^) (j123 f a b c) ?Goal ?Goal0
  ?Goal1
  -A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
b: B
((j12 f a b)^)^ = j12 f a b apply inv_V.
  -A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
c: C
j13 f a c = j13 f a c reflexivity.
  -A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
b: B
c: C
j23 f b c = j23 f b c reflexivity.
  -A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
b: B
c: C
prism'
  (moveR_Vp (j23 f b c) (j13 f a c) (j12 f a b)^
     (moveR_Vp (j13 f a c) (j23 f b c) (j12 f a b)
        (j123 f a b c)^)^) (j123 f a b c)
  (inv_V (j12 f a b)) 1 1 by triangle_ind f a b c.
Defined.

(** We get the twist natural equivalence on [TriJoinRecData]. *)
Definition trijoinrecdata_twist_natequiv (A B C : Type)
  : NatEquiv (trijoinrecdata_0gpd_fun A B C) (trijoinrecdata_0gpd_fun B A C).A, B, C: Type
NatEquiv (trijoinrecdata_0gpd_fun A B C)
  (trijoinrecdata_0gpd_fun B A C)
Proof.A, B, C: Type
NatEquiv (trijoinrecdata_0gpd_fun A B C)
  (trijoinrecdata_0gpd_fun B A C)
  snrapply Build_NatEquiv.A, B, C: Type
forall a : Type,
trijoinrecdata_0gpd_fun A B C a $<~>
trijoinrecdata_0gpd_fun B A C a
A, B, C: Type
Is1Natural (trijoinrecdata_0gpd_fun A B C)
  (trijoinrecdata_0gpd_fun B A C)
  (fun a : Type => ?e a)
  (* An equivalence of 0-groupoids for each [P]: *)
  -A, B, C: Type
forall a : Type,
trijoinrecdata_0gpd_fun A B C a $<~>
trijoinrecdata_0gpd_fun B A C a intro P.A, B, C, P: Type
trijoinrecdata_0gpd_fun A B C P $<~>
trijoinrecdata_0gpd_fun B A C P
    snrapply cate_adjointify.A, B, C, P: Type
trijoinrecdata_0gpd_fun A B C P $->
trijoinrecdata_0gpd_fun B A C P
A, B, C, P: Type
trijoinrecdata_0gpd_fun B A C P $->
trijoinrecdata_0gpd_fun A B C P
A, B, C, P: Type
?f $o ?g $== Id (trijoinrecdata_0gpd_fun B A C P)
A, B, C, P: Type
?g $o ?f $== Id (trijoinrecdata_0gpd_fun A B C P)
    1, 2: apply trijoinrecdata_twist.A, B, C, P: Type
trijoinrecdata_twist A B C P $o
trijoinrecdata_twist B A C P $==
Id (trijoinrecdata_0gpd_fun B A C P)
A, B, C, P: Type
trijoinrecdata_twist B A C P $o
trijoinrecdata_twist A B C P $==
Id (trijoinrecdata_0gpd_fun A B C P)
    1, 2: apply trijoinrecdata_twist_inv.
  (* Naturality: *)
  -A, B, C: Type
Is1Natural (trijoinrecdata_0gpd_fun A B C)
  (trijoinrecdata_0gpd_fun B A C)
  (fun a : Type =>
   (fun P : Type =>
    cate_adjointify (trijoinrecdata_twist A B C P)
      (trijoinrecdata_twist B A C P)
      (trijoinrecdata_twist_inv B A C P)
      (trijoinrecdata_twist_inv A B C P)) a) intros P Q g f; simpl.A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
TriJoinRecPath
  {|
    j1 := fun x : B => g (j2 f x);
    j2 := fun x : A => g (j1 f x);
    j3 := fun x : C => g (j3 f x);
    j12 := fun (b : B) (a : A) => (ap g (j12 f a b))^;
    j13 := fun (b : B) (c : C) => ap g (j23 f b c);
    j23 := fun (a : A) (c : C) => ap g (j13 f a c);
    j123 :=
      fun (a : B) (b : A) (c : C) =>
      moveR_Vp (ap g (j13 f b c)) (ap g (j23 f a c))
        (ap g (j12 f b a))
        (ap_triangle g (j123 f b a c))^
  |}
  (trijoinrecdata_fun g
     {|
       j1 := j2 f;
       j2 := j1 f;
       j3 := j3 f;
       j12 := fun (b : B) (a : A) => (j12 f a b)^;
       j13 := j23 f;
       j23 := j13 f;
       j123 :=
         fun (a : B) (b : A) (c : C) =>
         moveR_Vp (j13 f b c) (j23 f a c) (j12 f b a)
           (j123 f b a c)^
     |})
    bundle_trijoinrecpath.A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
forall (a : B) (b : A),
j12'
  (unbundle_trijoinrecdata
     {|
       j1 := fun x : B => g (j2 f x);
       j2 := fun x : A => g (j1 f x);
       j3 := fun x : C => g (j3 f x);
       j12 :=
         fun (b0 : B) (a0 : A) =>
         (ap g (j12 f a0 b0))^;
       j13 :=
         fun (b0 : B) (c : C) => ap g (j23 f b0 c);
       j23 :=
         fun (a0 : A) (c : C) => ap g (j13 f a0 c);
       j123 :=
         fun (a0 : B) (b0 : A) (c : C) =>
         moveR_Vp (ap g (j13 f b0 c))
           (ap g (j23 f a0 c)) (ap g (j12 f b0 a0))
           (ap_triangle g (j123 f b0 a0 c))^
     |}) a b =
j12'
  (unbundle_trijoinrecdata
     (trijoinrecdata_fun g
        {|
          j1 := j2 f;
          j2 := j1 f;
          j3 := j3 f;
          j12 :=
            fun (b0 : B) (a0 : A) => (j12 f a0 b0)^;
          j13 := j23 f;
          j23 := j13 f;
          j123 :=
            fun (a0 : B) (b0 : A) (c : C) =>
            moveR_Vp (j13 f b0 c) (j23 f a0 c)
              (j12 f b0 a0) (j123 f b0 a0 c)^
        |})) a b
A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
forall (a : B) (c : C),
j13'
  (unbundle_trijoinrecdata
     {|
       j1 := fun x : B => g (j2 f x);
       j2 := fun x : A => g (j1 f x);
       j3 := fun x : C => g (j3 f x);
       j12 :=
         fun (b : B) (a0 : A) => (ap g (j12 f a0 b))^;
       j13 :=
         fun (b : B) (c0 : C) => ap g (j23 f b c0);
       j23 :=
         fun (a0 : A) (c0 : C) => ap g (j13 f a0 c0);
       j123 :=
         fun (a0 : B) (b : A) (c0 : C) =>
         moveR_Vp (ap g (j13 f b c0))
           (ap g (j23 f a0 c0)) (ap g (j12 f b a0))
           (ap_triangle g (j123 f b a0 c0))^
     |}) a c =
j13'
  (unbundle_trijoinrecdata
     (trijoinrecdata_fun g
        {|
          j1 := j2 f;
          j2 := j1 f;
          j3 := j3 f;
          j12 := fun (b : B) (a0 : A) => (j12 f a0 b)^;
          j13 := j23 f;
          j23 := j13 f;
          j123 :=
            fun (a0 : B) (b : A) (c0 : C) =>
            moveR_Vp (j13 f b c0) (j23 f a0 c0)
              (j12 f b a0) (j123 f b a0 c0)^
        |})) a c
A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
forall (b : A) (c : C),
j23'
  (unbundle_trijoinrecdata
     {|
       j1 := fun x : B => g (j2 f x);
       j2 := fun x : A => g (j1 f x);
       j3 := fun x : C => g (j3 f x);
       j12 :=
         fun (b0 : B) (a : A) => (ap g (j12 f a b0))^;
       j13 :=
         fun (b0 : B) (c0 : C) => ap g (j23 f b0 c0);
       j23 :=
         fun (a : A) (c0 : C) => ap g (j13 f a c0);
       j123 :=
         fun (a : B) (b0 : A) (c0 : C) =>
         moveR_Vp (ap g (j13 f b0 c0))
           (ap g (j23 f a c0)) (ap g (j12 f b0 a))
           (ap_triangle g (j123 f b0 a c0))^
     |}) b c =
j23'
  (unbundle_trijoinrecdata
     (trijoinrecdata_fun g
        {|
          j1 := j2 f;
          j2 := j1 f;
          j3 := j3 f;
          j12 := fun (b0 : B) (a : A) => (j12 f a b0)^;
          j13 := j23 f;
          j23 := j13 f;
          j123 :=
            fun (a : B) (b0 : A) (c0 : C) =>
            moveR_Vp (j13 f b0 c0) (j23 f a c0)
              (j12 f b0 a) (j123 f b0 a c0)^
        |})) b c
A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
forall (a : B) (b : A) (c : C),
prism'
  (j123'
     (unbundle_trijoinrecdata
        {|
          j1 := fun x : B => g (j2 f x);
          j2 := fun x : A => g (j1 f x);
          j3 := fun x : C => g (j3 f x);
          j12 :=
            fun (b0 : B) (a0 : A) =>
            (ap g (j12 f a0 b0))^;
          j13 :=
            fun (b0 : B) (c0 : C) =>
            ap g (j23 f b0 c0);
          j23 :=
            fun (a0 : A) (c0 : C) =>
            ap g (j13 f a0 c0);
          j123 :=
            fun (a0 : B) (b0 : A) (c0 : C) =>
            moveR_Vp (ap g (j13 f b0 c0))
              (ap g (j23 f a0 c0))
              (ap g (j12 f b0 a0))
              (ap_triangle g (j123 f b0 a0 c0))^
        |}) a b c)
  (j123'
     (unbundle_trijoinrecdata
        (trijoinrecdata_fun g
           {|
             j1 := j2 f;
             j2 := j1 f;
             j3 := j3 f;
             j12 :=
               fun (b0 : B) (a0 : A) => (j12 f a0 b0)^;
             j13 := j23 f;
             j23 := j13 f;
             j123 :=
               fun (a0 : B) (b0 : A) (c0 : C) =>
               moveR_Vp (j13 f b0 c0) (j23 f a0 c0)
                 (j12 f b0 a0) (j123 f b0 a0 c0)^
           |})) a b c) (?h12' a b) (?h13' a c)
  (?h23' b c)
    all: intros; cbn.A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
a: B
b: A
(ap g (j12 f b a))^ = ap g (j12 f b a)^
A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
a: B
c: C
ap g (j23 f a c) = ap g (j23 f a c)
A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
b: A
c: C
ap g (j13 f b c) = ap g (j13 f b c)
A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
a: B
b: A
c: C
prism'
  (moveR_Vp (ap g (j13 f b c)) (ap g (j23 f a c))
     (ap g (j12 f b a))
     (ap_triangle g (j123 f b a c))^)
  (ap_triangle g
     (moveR_Vp (j13 f b c) (j23 f a c) (j12 f b a)
        (j123 f b a c)^)) ?Goal ?Goal0 ?Goal1
    +A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
a: B
b: A
(ap g (j12 f b a))^ = ap g (j12 f b a)^ symmetry; apply ap_V.
    +A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
a: B
c: C
ap g (j23 f a c) = ap g (j23 f a c) reflexivity.
    +A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
b: A
c: C
ap g (j13 f b c) = ap g (j13 f b c) reflexivity.
    +A, B, C, P, Q: Type
g: P $-> Q
f: trijoinrecdata_0gpd_fun A B C P
a: B
b: A
c: C
prism'
  (moveR_Vp (ap g (j13 f b c)) (ap g (j23 f a c))
     (ap g (j12 f b a))
     (ap_triangle g (j123 f b a c))^)
  (ap_triangle g
     (moveR_Vp (j13 f b c) (j23 f a c) (j12 f b a)
        (j123 f b a c)^)) (ap_V g (j12 f b a))^ 1 1 by triangle_ind f b a c.
Defined.

(** Combining with the recursion equivalence [trijoin_rec_inv_natequiv] and its inverse gives the twist natural equivalence between the representable functors. *)
Definition trijoinrecdata_fun_twist (A B C : Type)
  : NatEquiv (opyon_0gpd (TriJoin A B C)) (opyon_0gpd (TriJoin B A C))
  := natequiv_compose (trijoin_rec_natequiv B A C)
      (natequiv_compose (trijoinrecdata_twist_natequiv A B C) (trijoin_rec_inv_natequiv A B C)).

(** The Yoneda lemma for 0-groupoid valued functors therefore gives us an equivalence between the representing objects.  We mark this with a prime, since we'll use a homotopic map with a slightly simpler definition. *)
Definition equiv_trijoin_twist' (A B C : Type)
  : TriJoin A B C <~> TriJoin B A C.A, B, C: Type
TriJoin A B C <~> TriJoin B A C
Proof.A, B, C: Type
TriJoin A B C <~> TriJoin B A C
  rapply (opyon_equiv_0gpd (A:=Type)).A, B, C: Type
opyon1_0gpd (TriJoin B A C) $<~>
opyon1_0gpd (TriJoin A B C)
  apply trijoinrecdata_fun_twist.
Defined.

(** It has the nice property that the underlying function of the inverse is again [equiv_trijoin_twist'], with arguments permuted. *)
Local Definition trijoin_twist_check1 (A B C : Type)
  : (equiv_trijoin_twist' A B C)^-1 = equiv_fun (equiv_trijoin_twist' B A C)
  := idpath.

(** The definition we end up with is almost the same as the obvious one, but has some extra [ap idmap]s in it. *)
Local Definition twijoin_twist_check2 (A B C : Type)
  : equiv_fun (equiv_trijoin_twist' A B C)
    = trijoin_rec {| j1 := join2; j2 := join1; j3 := join3;
      j12 := fun (b : A) (a : B) => (ap idmap (join12 a b))^;
      j13 := fun (b : A) (c : C) => ap idmap (join23 b c);
      j23 := fun (a : B) (c : C) => ap idmap (join13 a c);
      j123 := fun (a : A) (b : B) (c : C) =>
               moveR_Vp _ _ _ (ap_triangle idmap (join123 b a c))^ |}
  := idpath.

(** The next two give the obvious definition. *)
Definition trijoin_twist_recdata (A B C : Type)
  : TriJoinRecData A B C (TriJoin B A C)
  := Build_TriJoinRecData join2 join1 join3
      (fun a b => (join12 b a)^) join23 join13
      (fun a b c => moveR_Vp _ _ _ (join123 b a c)^).

Definition trijoin_twist (A B C : Type)
  : TriJoin A B C -> TriJoin B A C
  := trijoin_rec (trijoin_twist_recdata A B C).

(** As an aside, note that [trijoin_twist] computes nicely on [joinr]. *)
Local Definition trijoin_twist_joinr (A B C : Type)
  : trijoin_twist A B C o joinr = functor_join idmap joinr
  := idpath.

(** The obvious definition is homotopic to the definition via the Yoneda lemma. *)
Definition trijoin_twist_homotopic (A B C : Type)
  : trijoin_twist A B C == equiv_trijoin_twist' A B C.A, B, C: Type
trijoin_twist A B C == equiv_trijoin_twist' A B C
Proof.A, B, C: Type
trijoin_twist A B C == equiv_trijoin_twist' A B C
  symmetry.A, B, C: Type
equiv_trijoin_twist' A B C == trijoin_twist A B C
  (** Both sides are [trijoin_rec] applied to [TriJoinRecData]: *)
  rapply (fmap trijoin_rec).A, B, C: Type
natequiv_compose (trijoinrecdata_twist_natequiv B A C)
  (trijoin_rec_inv_natequiv B A C) (TriJoin B A C)
  (Id (TriJoin B A C)) $-> trijoin_twist_recdata A B C
  bundle_trijoinrecpath; intros; cbn.A, B, C: Type
a: A
b: B
(ap idmap (join12 b a))^ = (join12 b a)^
A, B, C: Type
a: A
c: C
ap idmap (join23 a c) = join23 a c
A, B, C: Type
b: B
c: C
ap idmap (join13 b c) = join13 b c
A, B, C: Type
a: A
b: B
c: C
prism'
  (moveR_Vp (ap idmap (join13 b c))
     (ap idmap (join23 a c)) (ap idmap (join12 b a))
     (ap_triangle idmap (join123 b a c))^)
  (moveR_Vp (join13 b c) (join23 a c) (join12 b a)
     (join123 b a c)^) ?Goal ?Goal0 ?Goal1
  1: refine (ap inverse _).A, B, C: Type
a: A
b: B
ap idmap (join12 b a) = join12 b a
A, B, C: Type
a: A
c: C
ap idmap (join23 a c) = join23 a c
A, B, C: Type
b: B
c: C
ap idmap (join13 b c) = join13 b c
A, B, C: Type
a: A
b: B
c: C
prism'
  (moveR_Vp (ap idmap (join13 b c))
     (ap idmap (join23 a c)) (ap idmap (join12 b a))
     (ap_triangle idmap (join123 b a c))^)
  (moveR_Vp (join13 b c) (join23 a c) (join12 b a)
     (join123 b a c)^) (ap inverse ?Goal2) ?Goal
  ?Goal0
  1, 2, 3: apply ap_idmap.A, B, C: Type
a: A
b: B
c: C
prism'
  (moveR_Vp (ap idmap (join13 b c))
     (ap idmap (join23 a c)) (ap idmap (join12 b a))
     (ap_triangle idmap (join123 b a c))^)
  (moveR_Vp (join13 b c) (join23 a c) (join12 b a)
     (join123 b a c)^)
  (ap inverse (ap_idmap (join12 b a)))
  (ap_idmap (join23 a c)) (ap_idmap (join13 b c))
  generalize (join123 b a c).A, B, C: Type
a: A
b: B
c: C
forall p : join12 b a @ join23 a c = join13 b c,
prism'
  (moveR_Vp (ap idmap (join13 b c))
     (ap idmap (join23 a c)) (ap idmap (join12 b a))
     (ap_triangle idmap p)^)
  (moveR_Vp (join13 b c) (join23 a c) (join12 b a) p^)
  (ap inverse (ap_idmap (join12 b a)))
  (ap_idmap (join23 a c)) (ap_idmap (join13 b c))
  generalize (join23 (A:=B) a c).A, B, C: Type
a: A
b: B
c: C
forall (p : join2 a = join3 c)
(p0 : join12 b a @ p = join13 b c),
prism'
  (moveR_Vp (ap idmap (join13 b c)) (ap idmap p)
     (ap idmap (join12 b a)) (ap_triangle idmap p0)^)
  (moveR_Vp (join13 b c) p (join12 b a) p0^)
  (ap inverse (ap_idmap (join12 b a))) (ap_idmap p)
  (ap_idmap (join13 b c))
  generalize (join13 (B:=A) b c).A, B, C: Type
a: A
b: B
c: C
forall (p : join1 b = join3 c)
(p0 : join2 a = join3 c) (p1 : join12 b a @ p0 = p),
prism'
  (moveR_Vp (ap idmap p) (ap idmap p0)
     (ap idmap (join12 b a)) (ap_triangle idmap p1)^)
  (moveR_Vp p p0 (join12 b a) p1^)
  (ap inverse (ap_idmap (join12 b a))) (ap_idmap p0)
  (ap_idmap p)
  generalize (join12 (C:=C) b a).A, B, C: Type
a: A
b: B
c: C
forall (p : join1 b = join2 a)
(p0 : join1 b = join3 c) (p1 : join2 a = join3 c)
(p2 : p @ p1 = p0),
prism'
  (moveR_Vp (ap idmap p0) (ap idmap p1) (ap idmap p)
     (ap_triangle idmap p2)^) (moveR_Vp p0 p1 p p2^)
  (ap inverse (ap_idmap p)) (ap_idmap p1)
  (ap_idmap p0)
  generalize (join3 (A:=B) (B:=A) c).A, B, C: Type
a: A
b: B
c: C
forall (t : TriJoin B A C) (p : join1 b = join2 a)
(p0 : join1 b = t) (p1 : join2 a = t)
(p2 : p @ p1 = p0),
prism'
  (moveR_Vp (ap idmap p0) (ap idmap p1) (ap idmap p)
     (ap_triangle idmap p2)^) (moveR_Vp p0 p1 p p2^)
  (ap inverse (ap_idmap p)) (ap_idmap p1)
  (ap_idmap p0)
  generalize (join2 (A:=B) (C:=C) a).A, B, C: Type
a: A
b: B
c: C
forall (t t0 : TriJoin B A C) (p : join1 b = t)
(p0 : join1 b = t0) (p1 : t = t0) (p2 : p @ p1 = p0),
prism'
  (moveR_Vp (ap idmap p0) (ap idmap p1) (ap idmap p)
     (ap_triangle idmap p2)^) (moveR_Vp p0 p1 p p2^)
  (ap inverse (ap_idmap p)) (ap_idmap p1)
  (ap_idmap p0)
  generalize (join1 (B:=A) (C:=C) b).A, B, C: Type
a: A
b: B
c: C
forall (t t0 t1 : TriJoin B A C) (p : t = t0)
(p0 : t = t1) (p1 : t0 = t1) (p2 : p @ p1 = p0),
prism'
  (moveR_Vp (ap idmap p0) (ap idmap p1) (ap idmap p)
     (ap_triangle idmap p2)^) (moveR_Vp p0 p1 p p2^)
  (ap inverse (ap_idmap p)) (ap_idmap p1)
  (ap_idmap p0)
  intros k1 k2 k3 k12 k13 k23 k123.A, B, C: Type
a: A
b: B
c: C
k1, k2, k3: TriJoin B A C
k12: k1 = k2
k13: k1 = k3
k23: k2 = k3
k123: k12 @ k23 = k13
prism'
  (moveR_Vp (ap idmap k13) (ap idmap k23)
     (ap idmap k12) (ap_triangle idmap k123)^)
  (moveR_Vp k13 k23 k12 k123^)
  (ap inverse (ap_idmap k12)) (ap_idmap k23)
  (ap_idmap k13)
  induction k12, k23, k123.A, B, C: Type
a: A
b: B
c: C
k1: TriJoin B A C
prism'
  (moveR_Vp (ap idmap (1 @ 1)) 
     (ap idmap 1) (ap idmap 1) 
     (ap_triangle idmap 1)^) 
  (moveR_Vp (1 @ 1) 1 1 1^) 
  (ap inverse (ap_idmap 1)) 
  (ap_idmap 1) (ap_idmap (1 @ 1))
  reflexivity.
Defined.

(** Therefore the obvious definition is also an equivalence, and the inverse function can also be chosen to be [trijoin_twist]. *)
Definition equiv_trijoin_twist (A B C : Type)
  : TriJoin A B C <~> TriJoin B A C
  := equiv_homotopic_inverse (equiv_trijoin_twist' A B C)
                            (trijoin_twist_homotopic A B C)
                            (trijoin_twist_homotopic B A C).

(** ** The associativity of [Join] *)

(** [trijoin_twist] corresponds to the permutation (1,2).  The equivalence corresponding to the permutation (2,3) also plays a key role, so we name it here. *)
Definition trijoin_id_sym A B C : TriJoin A B C <~> TriJoin A C B
  := equiv_functor_join equiv_idmap (equiv_join_sym B C).

Arguments trijoin_id_sym : simpl never.

Definition join_assoc A B C : Join A (Join B C) <~> Join (Join A B) C.A, B, C: Type
Join A (Join B C) <~> Join (Join A B) C
Proof.A, B, C: Type
Join A (Join B C) <~> Join (Join A B) C
  refine (_ oE trijoin_id_sym _ _ _).A, B, C: Type
TriJoin A C B <~> Join (Join A B) C
  refine (_ oE equiv_trijoin_twist _ _ _).A, B, C: Type
TriJoin C A B <~> Join (Join A B) C
  apply equiv_join_sym.
Defined.

Arguments join_assoc : simpl never.

(** As a consequence, we get associativity of powers. *)
Corollary join_join_power A n m
  : Join (join_power A n) (join_power A m) <~> join_power A (n + m)%nat.A: Type
n, m: nat
Join (join_power A n) (join_power A m) <~>
join_power A (n + m)
Proof.A: Type
n, m: nat
Join (join_power A n) (join_power A m) <~>
join_power A (n + m)
  induction n as [|n IHn].A: Type
m: nat
Join (join_power A 0) (join_power A m) <~>
join_power A (0 + m)
A: Type
n, m: nat
IHn: Join (join_power A n) (join_power A m) <~> join_power A (n + m)
Join (join_power A n.+1) (join_power A m) <~>
join_power A (n.+1 + m)
  1: exact (equiv_join_empty_left _).A: Type
n, m: nat
IHn: Join (join_power A n) (join_power A m) <~> join_power A (n + m)
Join (join_power A n.+1) (join_power A m) <~>
join_power A (n.+1 + m)
  simpl.A: Type
n, m: nat
IHn: Join (join_power A n) (join_power A m) <~> join_power A (n + m)
Join (Join A (join_power A n)) (join_power A m) <~>
Join A (join_power A (n + m)) refine (_ oE (join_assoc _ _ _)^-1%equiv).A: Type
n, m: nat
IHn: Join (join_power A n) (join_power A m) <~> join_power A (n + m)
Join A (Join (join_power A n) (join_power A m)) <~>
Join A (join_power A (n + m))
  exact (equiv_functor_join equiv_idmap IHn).
Defined.

(** ** Naturality of [trijoin_twist] *)

(** Our goal is to prove that [trijoin_twist A' B' C' o functor_join f (functor_join g h)] is homotopic to [functor_join g (functor_join f h) o trijoin_twist A B C]. *)

(** We first give a way to write anything of the form [trijoin_rec f o trijoin_twist A B C] as [trijoin_rec] applied to some [TriJoinRecData]. *)
Definition trijoin_rec_trijoin_twist {A B C P} (f : TriJoinRecData B A C P)
  : trijoin_rec f o trijoin_twist A B C == trijoin_rec (trijoinrecdata_twist _ _ _ _ f).A, B, C, P: Type
f: TriJoinRecData B A C P
trijoin_rec f o trijoin_twist A B C ==
trijoin_rec (trijoinrecdata_twist B A C P f)
Proof.A, B, C, P: Type
f: TriJoinRecData B A C P
trijoin_rec f o trijoin_twist A B C ==
trijoin_rec (trijoinrecdata_twist B A C P f)
  (* We first replace [trijoin_twist] with [equiv_trijoin_twist']. *)
  transitivity (trijoin_rec f o equiv_trijoin_twist' A B C).A, B, C, P: Type
f: TriJoinRecData B A C P
trijoin_rec f o trijoin_twist A B C ==
trijoin_rec f o equiv_trijoin_twist' A B C
A, B, C, P: Type
f: TriJoinRecData B A C P
trijoin_rec f o equiv_trijoin_twist' A B C ==
trijoin_rec (trijoinrecdata_twist B A C P f)
  1: exact (fun x => ap (trijoin_rec f) (trijoin_twist_homotopic A B C x)).A, B, C, P: Type
f: TriJoinRecData B A C P
trijoin_rec f o equiv_trijoin_twist' A B C ==
trijoin_rec (trijoinrecdata_twist B A C P f)
  (* The LHS is now the twist natural transformation applied to [Id], followed by postcomposition; naturality states that that is the same as the natural trans applied to [trijoin_rec f]. *)
  refine ((isnat_natequiv (trijoinrecdata_fun_twist B A C) (trijoin_rec f) _)^$ $@ _).A, B, C, P: Type
f: TriJoinRecData B A C P
(trijoinrecdata_fun_twist B A C P $o
 fmap (opyon_0gpd (TriJoin B A C)) (trijoin_rec f))
  (Id (TriJoin B A C)) $==
trijoin_rec (trijoinrecdata_twist B A C P f)
  (* The LHS simplifies to [trijoinrecdata_fun_twist] applied to [trijoin_rec f].  The former is a composite of [trijoin_rec], [trijoinrecdata_twist] and [trijoin_rec_inv], so we can write the LHS as: *)
  change (?L $== ?R) with (trijoin_rec (trijoinrecdata_twist B A C P (trijoin_rec_inv (trijoin_rec f))) $== R).A, B, C, P: Type
f: TriJoinRecData B A C P
trijoin_rec
  (trijoinrecdata_twist B A C P
     (trijoin_rec_inv (trijoin_rec f))) $==
trijoin_rec (trijoinrecdata_twist B A C P f)
  refine (fmap trijoin_rec _).A, B, C, P: Type
f: TriJoinRecData B A C P
trijoinrecdata_twist B A C P
  (trijoin_rec_inv (trijoin_rec f)) $->
trijoinrecdata_twist B A C P f
  refine (fmap (trijoinrecdata_twist B A C P) _).A, B, C, P: Type
f: TriJoinRecData B A C P
trijoin_rec_inv (trijoin_rec f) $-> f
  apply trijoin_rec_beta.
Defined.

(** Naturality of [trijoin_twist].  This version uses [functor_trijoin] and simply combines previous results. *)
Definition trijoin_twist_nat' {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
  : trijoin_twist A' B' C' o functor_trijoin f g h
    == functor_trijoin g f h o trijoin_twist A B C.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
trijoin_twist A' B' C' o functor_trijoin f g h ==
functor_trijoin g f h o trijoin_twist A B C
Proof.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
trijoin_twist A' B' C' o functor_trijoin f g h ==
functor_trijoin g f h o trijoin_twist A B C
  intro x.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: TriJoin A B C
trijoin_twist A' B' C' (functor_trijoin f g h x) =
functor_trijoin g f h (trijoin_twist A B C x)
  rhs nrapply trijoin_rec_trijoin_twist.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: TriJoin A B C
trijoin_twist A' B' C' (functor_trijoin f g h x) =
trijoin_rec
  (trijoinrecdata_twist B A C (TriJoin B' A' C')
     (trijoinrecdata_tricomp
        (trijoinrecdata_trijoin B' A' C') g f h)) x
  nrapply trijoin_rec_functor_trijoin.
Defined.

(** And now a version using [functor_join]. *)
Definition trijoin_twist_nat {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
  : trijoin_twist A' B' C' o functor_join f (functor_join g h)
    == functor_join g (functor_join f h) o trijoin_twist A B C.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
trijoin_twist A' B' C'
o functor_join f (functor_join g h) ==
functor_join g (functor_join f h)
o trijoin_twist A B C
Proof.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
trijoin_twist A' B' C'
o functor_join f (functor_join g h) ==
functor_join g (functor_join f h)
o trijoin_twist A B C
  intro x.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
trijoin_twist A' B' C'
  (functor_join f (functor_join g h) x) =
functor_join g (functor_join f h)
  (trijoin_twist A B C x)
  lhs nrefine (ap _ (functor_trijoin_as_functor_join f g h x)).A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
trijoin_twist A' B' C' (functor_trijoin f g h x) =
functor_join g (functor_join f h)
  (trijoin_twist A B C x)
  rhs nrapply functor_trijoin_as_functor_join.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
trijoin_twist A' B' C' (functor_trijoin f g h x) =
functor_trijoin g f h (trijoin_twist A B C x)
  apply trijoin_twist_nat'.
Defined.

(** ** Naturality of [trijoin_id_sym] *)

(** Naturality of [trijoin_id_sym], using [functor_join].  In this case, it's easier to do this version first. *)
Definition trijoin_id_sym_nat {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
  : trijoin_id_sym A' B' C' o functor_join f (functor_join g h)
    == functor_join f (functor_join h g) o trijoin_id_sym A B C.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
trijoin_id_sym A' B' C'
o functor_join f (functor_join g h) ==
functor_join f (functor_join h g)
o trijoin_id_sym A B C
Proof.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
trijoin_id_sym A' B' C'
o functor_join f (functor_join g h) ==
functor_join f (functor_join h g)
o trijoin_id_sym A B C
  intro x; simpl.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
functor_join idmap (join_sym B' C')
  (functor_join f (functor_join g h) x) =
functor_join f (functor_join h g)
  (functor_join idmap (join_sym B C) x)
  lhs_V nrapply functor_join_compose.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
functor_join (fun x : A => f x)
  (fun x : Join B C =>
   join_sym B' C' (functor_join g h x)) x =
functor_join f (functor_join h g)
  (functor_join idmap (join_sym B C) x)
  rhs_V nrapply functor_join_compose.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
functor_join (fun x : A => f x)
  (fun x : Join B C =>
   join_sym B' C' (functor_join g h x)) x =
functor_join (fun x : A => f x)
  (fun x : Join B C =>
   functor_join h g (join_sym B C x)) x
  apply functor2_join.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
(fun x : A => f x) == (fun x : A => f x)
A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
(fun x : Join B C =>
 join_sym B' C' (functor_join g h x)) ==
(fun x : Join B C => functor_join h g (join_sym B C x))
  -A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
(fun x : A => f x) == (fun x : A => f x) reflexivity.
  -A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
(fun x : Join B C =>
 join_sym B' C' (functor_join g h x)) ==
(fun x : Join B C => functor_join h g (join_sym B C x)) apply join_sym_nat.
Defined.

(** Naturality of [trijoin_id_sym], using [functor_trijoin]. *)
Definition trijoin_id_sym_nat' {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
  : trijoin_id_sym A' B' C' o functor_trijoin f g h
    == functor_trijoin f h g o trijoin_id_sym A B C.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
trijoin_id_sym A' B' C' o functor_trijoin f g h ==
functor_trijoin f h g o trijoin_id_sym A B C
Proof.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
trijoin_id_sym A' B' C' o functor_trijoin f g h ==
functor_trijoin f h g o trijoin_id_sym A B C
  intro x.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: TriJoin A B C
trijoin_id_sym A' B' C' (functor_trijoin f g h x) =
functor_trijoin f h g (trijoin_id_sym A B C x)
  lhs_V nrefine (ap _ (functor_trijoin_as_functor_join f g h x)).A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: TriJoin A B C
trijoin_id_sym A' B' C'
  (functor_join f (functor_join g h) x) =
functor_trijoin f h g (trijoin_id_sym A B C x)
  rhs_V nrapply functor_trijoin_as_functor_join.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: TriJoin A B C
trijoin_id_sym A' B' C'
  (functor_join f (functor_join g h) x) =
functor_join f (functor_join h g)
  (trijoin_id_sym A B C x)
  apply trijoin_id_sym_nat.
Defined.

(** ** Naturality of [join_assoc] *)

(** Since [join_assoc] is a composite of [join_sym], [trijoin_twist] and [trijoin_id_sym], we just use their naturality. *)
Definition join_assoc_nat {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C')
  : join_assoc A' B' C' o functor_join f (functor_join g h)
    == functor_join (functor_join f g) h o join_assoc A B C.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
join_assoc A' B' C'
o functor_join f (functor_join g h) ==
functor_join (functor_join f g) h o join_assoc A B C
Proof.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
join_assoc A' B' C'
o functor_join f (functor_join g h) ==
functor_join (functor_join f g) h o join_assoc A B C
  (* We'll work from right to left, as it is easier to work near the head of a term. *)
  intro x.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
join_assoc A' B' C'
  (functor_join f (functor_join g h) x) =
functor_join (functor_join f g) h (join_assoc A B C x)
  unfold join_assoc; cbn.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
join_sym C' (Join A' B')
  (trijoin_twist A' C' B'
     (trijoin_id_sym A' B' C'
        (functor_join f (functor_join g h) x))) =
functor_join (functor_join f g) h
  (join_sym C (Join A B)
     (trijoin_twist A C B (trijoin_id_sym A B C x)))
  (* First we pass the [functor_joins]s through the outer [join_sym]. *)
  rhs_V nrapply join_sym_nat.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
join_sym C' (Join A' B')
  (trijoin_twist A' C' B'
     (trijoin_id_sym A' B' C'
        (functor_join f (functor_join g h) x))) =
join_sym C' (Join A' B')
  (functor_join h (functor_join f g)
     (trijoin_twist A C B (trijoin_id_sym A B C x)))
  (* Strip off the outer [join_sym]. *)
  apply (ap _).A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
trijoin_twist A' C' B'
  (trijoin_id_sym A' B' C'
     (functor_join f (functor_join g h) x)) =
functor_join h (functor_join f g)
  (trijoin_twist A C B (trijoin_id_sym A B C x))
  (* Next we pass the [functor_join]s through [trijoin_twist]. *)
  rhs_V nrapply trijoin_twist_nat.A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
trijoin_twist A' C' B'
  (trijoin_id_sym A' B' C'
     (functor_join f (functor_join g h) x)) =
trijoin_twist A' C' B'
  (functor_join f (functor_join h g)
     (trijoin_id_sym A B C x))
  (* Strip off the [trijoin_twist]. *)
  apply (ap _).A, B, C, A', B', C': Type
f: A -> A'
g: B -> B'
h: C -> C'
x: Join A (Join B C)
trijoin_id_sym A' B' C'
  (functor_join f (functor_join g h) x) =
functor_join f (functor_join h g)
  (trijoin_id_sym A B C x)
  (* Finally, we pass the [functor_join]s through [trijoin_id_sym]. *)
  apply trijoin_id_sym_nat.
Defined.

Global Instance join_associator : Associator Join.Associator Join
Proof.Associator Join
  snrapply Build_Associator; simpl.forall a b c : Type,
Join a (Join b c) $<~> Join (Join a b) c
Is1Natural
  (fun pat : Type * Type * Type =>
   Join (fst (fst pat))
     (Join (snd (fst pat)) (snd pat)))
  (fun pat : Type * Type * Type =>
   Join (Join (fst (fst pat)) (snd (fst pat)))
     (snd pat))
  (fun pat : Type * Type * Type =>
   ?Goal (fst (fst pat)) (snd (fst pat)) (snd pat))
  -forall a b c : Type,
Join a (Join b c) $<~> Join (Join a b) c exact join_assoc.
  -Is1Natural
  (fun pat : Type * Type * Type =>
   Join (fst (fst pat))
     (Join (snd (fst pat)) (snd pat)))
  (fun pat : Type * Type * Type =>
   Join (Join (fst (fst pat)) (snd (fst pat)))
     (snd pat))
  (fun pat : Type * Type * Type =>
   join_assoc (fst (fst pat)) (snd (fst pat))
     (snd pat)) intros [[A B] C] [[A' B'] C'] [[f g] h]; cbn.A, B, C, A', B', C': Type
f: fst (fst (A, B, C)) $-> fst (fst (A', B', C'))
g: snd (fst (A, B, C)) $-> snd (fst (A', B', C'))
h: snd (A, B, C) $-> snd (A', B', C')
(fun x : Join A (Join B C) =>
 join_assoc A' B' C'
   (functor_join f (functor_join g h) x)) ==
(fun x : Join A (Join B C) =>
 functor_join (functor_join f g) h
   (join_assoc A B C x))
    apply join_assoc_nat.
Defined.

(** ** The Triangle Law *)

(** The unitors were defined in Join/Core.v, since they do not require associativity. *)

(** Here's a version of the triangle law expressed using [trijoin_twist] instead of [join_assoc], and only using the right unitor. Since the left unitor is defined using [join_sym], the usual triangle law follows. *)
Definition join_trianglelaw' A B
  : join_sym B A o functor_join idmap (equiv_join_empty_right A) o trijoin_twist A B Empty
    == functor_join idmap (equiv_join_empty_right B).A, B: Type
join_sym B A
o functor_join idmap (equiv_join_empty_right A)
o trijoin_twist A B Empty ==
functor_join idmap (equiv_join_empty_right B)
Proof.A, B: Type
join_sym B A
o functor_join idmap (equiv_join_empty_right A)
o trijoin_twist A B Empty ==
functor_join idmap (equiv_join_empty_right B)
  (* A direct proof with [Join_ind] three times is not hard, but the path algebra is slightly simpler if we manipulate things ahead of time using [functor_join_join_rec] and [trijoin_rec_trijoin_twist]. *)
  intro x.A, B: Type
x: TriJoin A B Empty
join_sym B A
  (functor_join idmap (equiv_join_empty_right A)
     (trijoin_twist A B Empty x)) =
functor_join idmap (equiv_join_empty_right B) x
  rapply moveR_equiv_M.A, B: Type
x: TriJoin A B Empty
functor_join idmap (equiv_join_empty_right A)
  (trijoin_twist A B Empty x) =
(join_sym B A)^-1
  (functor_join idmap (equiv_join_empty_right B) x)
  unfold equiv_join_empty_right at 1; cbn.A, B: Type
x: TriJoin A B Empty
functor_join idmap
  (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
     |}) (trijoin_twist A B Empty x) =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B) x)
  lhs nrapply functor_join_join_rec; cbn.A, B: Type
x: TriJoin A B Empty
trijoin_rec
  {|
    j1 := fun x : B => joinl x;
    j2 := fun x : A => joinr x;
    j3 :=
      fun x : Empty =>
      joinr (Empty_rect (fun _ : Empty => A) x);
    j12 := fun (a : B) (b : A) => jglue a b;
    j13 :=
      fun (a : B) (c : Empty) =>
      jglue a (Empty_rect (fun _ : Empty => A) c);
    j23 :=
      fun (b : A) (c : Empty) =>
      ap joinr
        (Empty_rect
           (fun b0 : Empty =>
            b = Empty_rect (fun _ : Empty => A) b0) c);
    j123 :=
      fun (a : B) (b : A) (c : Empty) =>
      triangle_v a
        (Empty_rect
           (fun b0 : Empty =>
            b = Empty_rect (fun _ : Empty => A) b0) c)
  |} (trijoin_twist A B Empty x) =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B) x)
  lhs nrapply trijoin_rec_trijoin_twist.A, B: Type
x: TriJoin A B Empty
trijoin_rec
  (trijoinrecdata_twist B A Empty (Join B A)
     {|
       j1 := fun x : B => joinl x;
       j2 := fun x : A => joinr x;
       j3 :=
         fun x : Empty =>
         joinr (Empty_rect (fun _ : Empty => A) x);
       j12 := fun (a : B) (b : A) => jglue a b;
       j13 :=
         fun (a : B) (c : Empty) =>
         jglue a (Empty_rect (fun _ : Empty => A) c);
       j23 :=
         fun (b : A) (c : Empty) =>
         ap joinr
           (Empty_rect
              (fun b0 : Empty =>
               b = Empty_rect (fun _ : Empty => A) b0)
              c);
       j123 :=
         fun (a : B) (b : A) (c : Empty) =>
         triangle_v a
           (Empty_rect
              (fun b0 : Empty =>
               b = Empty_rect (fun _ : Empty => A) b0)
              c)
     |}) x =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B) x)
  revert x.A, B: Type
forall x : TriJoin A B Empty,
trijoin_rec
  (trijoinrecdata_twist B A Empty (Join B A)
     {|
       j1 := fun x0 : B => joinl x0;
       j2 := fun x0 : A => joinr x0;
       j3 :=
         fun x0 : Empty =>
         joinr (Empty_rect (fun _ : Empty => A) x0);
       j12 := fun (a : B) (b : A) => jglue a b;
       j13 :=
         fun (a : B) (c : Empty) =>
         jglue a (Empty_rect (fun _ : Empty => A) c);
       j23 :=
         fun (b : A) (c : Empty) =>
         ap joinr
           (Empty_rect
              (fun b0 : Empty =>
               b = Empty_rect (fun _ : Empty => A) b0)
              c);
       j123 :=
         fun (a : B) (b : A) (c : Empty) =>
         triangle_v a
           (Empty_rect
              (fun b0 : Empty =>
               b = Empty_rect (fun _ : Empty => A) b0)
              c)
     |}) x =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B) x)
  apply moveR_trijoin_rec.A, B: Type
trijoinrecdata_twist B A Empty (Join B A)
  {|
    j1 := fun x : B => joinl x;
    j2 := fun x : A => joinr x;
    j3 :=
      fun x : Empty =>
      joinr (Empty_rect (fun _ : Empty => A) x);
    j12 := fun (a : B) (b : A) => jglue a b;
    j13 :=
      fun (a : B) (c : Empty) =>
      jglue a (Empty_rect (fun _ : Empty => A) c);
    j23 :=
      fun (b : A) (c : Empty) =>
      ap joinr
        (Empty_rect
           (fun b0 : Empty =>
            b = Empty_rect (fun _ : Empty => A) b0) c);
    j123 :=
      fun (a : B) (b : A) (c : Empty) =>
      triangle_v a
        (Empty_rect
           (fun b0 : Empty =>
            b = Empty_rect (fun _ : Empty => A) b0) c)
  |} $==
trijoin_rec_inv
  (fun x : TriJoin A B Empty =>
   join_sym A B
     (functor_join idmap (equiv_join_empty_right B) x))
  snrapply Build_TriJoinRecPath; intros; cbn.A, B: Type
a: A
joinr a =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B)
     (join1 a))
A, B: Type
b: B
joinl b =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B)
     (join2 b))
A, B: Type
c: Empty
joinr (Empty_rect (fun _ : Empty => A) c) =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B)
     (join3 c))
A, B: Type
a: A
b: B
(jglue b a)^ @ ?Goal0 =
?Goal @
ap
  (fun x : TriJoin A B Empty =>
   join_sym A B
     (functor_join idmap (equiv_join_empty_right B) x))
  (join12 a b)
A, B: Type
a: A
c: Empty
ap joinr
  (Empty_rect
     (fun b : Empty =>
      a = Empty_rect (fun _ : Empty => A) b) c) @
?Goal1 =
?Goal @
ap
  (fun x : TriJoin A B Empty =>
   join_sym A B
     (functor_join idmap (equiv_join_empty_right B) x))
  (join13 a c)
A, B: Type
b: B
c: Empty
jglue b (Empty_rect (fun _ : Empty => A) c) @ ?Goal1 =
?Goal0 @
ap
  (fun x : TriJoin A B Empty =>
   join_sym A B
     (functor_join idmap (equiv_join_empty_right B) x))
  (join23 b c)
A, B: Type
a: A
b: B
c: Empty
prism
  (moveR_Vp
     (jglue b (Empty_rect (fun _ : Empty => A) c))
     (ap joinr
        (Empty_rect
           (fun b : Empty =>
            a = Empty_rect (fun _ : Empty => A) b) c))
     (jglue b a)
     (triangle_v b
        (Empty_rect
           (fun b : Empty =>
            a = Empty_rect (fun _ : Empty => A) b) c))^)
  (ap_triangle
     (fun x : TriJoin A B Empty =>
      join_sym A B
        (functor_join idmap (equiv_join_empty_right B)
           x)) (join123 a b c)) ?Goal2 ?Goal3 ?Goal4
  3, 5, 6, 7: by destruct c.A, B: Type
a: A
joinr a =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B)
     (join1 a))
A, B: Type
b: B
joinl b =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B)
     (join2 b))
A, B: Type
a: A
b: B
(jglue b a)^ @ ?Goal0 =
?Goal @
ap
  (fun x : TriJoin A B Empty =>
   join_sym A B
     (functor_join idmap (equiv_join_empty_right B) x))
  (join12 a b)
  -A, B: Type
a: A
joinr a =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B)
     (join1 a)) reflexivity.
  -A, B: Type
b: B
joinl b =
join_sym A B
  (functor_join idmap (equiv_join_empty_right B)
     (join2 b)) reflexivity.
  -A, B: Type
a: A
b: B
(jglue b a)^ @ 1 =
1 @
ap
  (fun x : TriJoin A B Empty =>
   join_sym A B
     (functor_join idmap (equiv_join_empty_right B) x))
  (join12 a b) apply equiv_p1_1q.A, B: Type
a: A
b: B
(jglue b a)^ =
ap
  (fun x : TriJoin A B Empty =>
   join_sym A B
     (functor_join idmap (equiv_join_empty_right B) x))
  (join12 a b)
    symmetry.A, B: Type
a: A
b: B
ap
  (fun x : TriJoin A B Empty =>
   join_sym A B
     (functor_join idmap (equiv_join_empty_right B) x))
  (join12 a b) = (jglue b a)^
    lhs nrapply (ap_compose (functor_join idmap _) _ (join12 a b)).A, B: Type
a: A
b: B
ap (join_sym A B)
  (ap (functor_join idmap (equiv_join_empty_right B))
     (join12 a b)) = (jglue b a)^
    lhs nrapply ap.A, B: Type
a: A
b: B
ap (functor_join idmap (equiv_join_empty_right B))
  (join12 a b) = ?Goal
A, B: Type
a: A
b: B
ap (join_sym A B) ?Goal = (jglue b a)^
    1: apply functor_join_beta_jglue.A, B: Type
a: A
b: B
ap (join_sym A B)
  (jglue (idmap a)
     (equiv_join_empty_right B (joinl b))) =
(jglue b a)^
    apply join_sym_beta_jglue.
Defined.

Definition join_trianglelaw : TriangleIdentity Join Empty.TriangleIdentity Join Empty
Proof.TriangleIdentity Join Empty
  intros A B x; cbn.A, B: Type
x: Join A (Join Empty B)
functor_join idmap
  (fun x : Join Empty B =>
   equiv_join_empty_right B (join_sym Empty B x)) x =
functor_join (equiv_join_empty_right A) idmap
  (join_assoc A Empty B x) 
  lhs nrapply (functor_join_compose idmap _ idmap _).A, B: Type
x: Join A (Join Empty B)
functor_join idmap (equiv_join_empty_right B)
  (functor_join idmap (join_sym Empty B) x) =
functor_join (equiv_join_empty_right A) idmap
  (join_assoc A Empty B x)
  lhs_V nrapply join_trianglelaw'.A, B: Type
x: Join A (Join Empty B)
join_sym B A
  (functor_join idmap (equiv_join_empty_right A)
     (trijoin_twist A B Empty
        (functor_join idmap (join_sym Empty B) x))) =
functor_join (equiv_join_empty_right A) idmap
  (join_assoc A Empty B x)
  unfold join_assoc; cbn.A, B: Type
x: Join A (Join Empty B)
join_sym B A
  (functor_join idmap (equiv_join_empty_right A)
     (trijoin_twist A B Empty
        (functor_join idmap (join_sym Empty B) x))) =
functor_join (equiv_join_empty_right A) idmap
  (join_sym B (Join A Empty)
     (trijoin_twist A B Empty
        (trijoin_id_sym A Empty B x)))
  apply join_sym_nat.
Defined.

(** ** The hexagon axiom *)

(** For the hexagon, we'll need to know how to compose [trijoin_id_sym] with something of the form [trijoin_rec f]. For some reason, the proof is harder than it was for [trijoin_twist]. *)

(** This describes the transformation on [TriJoinRecData] corresponding to precomposition with [trijoin_id_sym], as in the next result. *)
Definition trijoinrecdata_id_sym {A B C P} (f : TriJoinRecData A B C P)
  : TriJoinRecData A C B P.A, B, C, P: Type
f: TriJoinRecData A B C P
TriJoinRecData A C B P
Proof.A, B, C, P: Type
f: TriJoinRecData A B C P
TriJoinRecData A C B P
  snrapply (Build_TriJoinRecData (j1 f) (j3 f) (j2 f)); intros.A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: C
j1 f a = j3 f b
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
c: B
j1 f a = j2 f c
A, B, C, P: Type
f: TriJoinRecData A B C P
b: C
c: B
j3 f b = j2 f c
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: C
c: B
(fun (a : A) (b : C) => ?Goal) a b @
(fun (b : C) (c : B) => ?Goal1) b c =
(fun (a : A) (c : B) => ?Goal0) a c
  -A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: C
j1 f a = j3 f b apply (j13 f).
  -A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
c: B
j1 f a = j2 f c apply (j12 f).
  -A, B, C, P: Type
f: TriJoinRecData A B C P
b: C
c: B
j3 f b = j2 f c symmetry; apply (j23 f).
  -A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: C
c: B
(fun (a : A) (b : C) => j13 f a b) a b @
(fun (b : C) (c : B) => (j23 f c b)^) b c =
(fun (a : A) (c : B) => j12 f a c) a c cbn beta.A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: C
c: B
j13 f a b @ (j23 f c b)^ = j12 f a c  apply moveR_pV; symmetry.A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: C
c: B
j12 f a c @ j23 f c b = j13 f a b
    apply (j123 f).
Defined.

(** This is analogous to [trijoin_rec_trijoin_twist] above, with [trijoin_twist] replaced by [trijoin_id_sym]. *)
Definition trijoin_rec_id_sym {A B C P} (f : TriJoinRecData A C B P)
  : trijoin_rec f o trijoin_id_sym A B C == trijoin_rec (trijoinrecdata_id_sym f).A, B, C, P: Type
f: TriJoinRecData A C B P
trijoin_rec f o trijoin_id_sym A B C ==
trijoin_rec (trijoinrecdata_id_sym f)
Proof.A, B, C, P: Type
f: TriJoinRecData A C B P
trijoin_rec f o trijoin_id_sym A B C ==
trijoin_rec (trijoinrecdata_id_sym f)
  (* First we use [functor_join_join_rec] on the LHS. *)
  etransitivity.A, B, C, P: Type
f: TriJoinRecData A C B P
trijoin_rec f o trijoin_id_sym A B C == ?Goal
A, B, C, P: Type
f: TriJoinRecData A C B P
?Goal == trijoin_rec (trijoinrecdata_id_sym f)
  {A, B, C, P: Type
f: TriJoinRecData A C B P
trijoin_rec f o trijoin_id_sym A B C == ?Goal refine (cat_postwhisker (A:=Type) (trijoin_rec f) _).A, B, C, P: Type
f: TriJoinRecData A C B P
trijoin_id_sym A B C $== ?Goal0
    apply functor_join_join_rec. }A, B, C, P: Type
f: TriJoinRecData A C B P
trijoin_rec f $o
trijoin_rec
  {|
    j1 := fun x : A => joinl (1%equiv x);
    j2 :=
      fun x : B => joinr (jl (join_sym_recdata B C) x);
    j3 :=
      fun x : C => joinr (jr (join_sym_recdata B C) x);
    j12 :=
      fun (a : A) (b : B) =>
      jglue (1%equiv a) (jl (join_sym_recdata B C) b);
    j13 :=
      fun (a : A) (c : C) =>
      jglue (1%equiv a) (jr (join_sym_recdata B C) c);
    j23 :=
      fun (b : B) (c : C) =>
      ap joinr (jg (join_sym_recdata B C) b c);
    j123 :=
      fun (a : A) (b : B) (c : C) =>
      triangle_v (1%equiv a)
        (jg (join_sym_recdata B C) b c)
  |} == trijoin_rec (trijoinrecdata_id_sym f)
  unfold join_sym_recdata, jl, jr, jg.A, B, C, P: Type
f: TriJoinRecData A C B P
trijoin_rec f $o
trijoin_rec
  {|
    j1 := fun x : A => joinl (1%equiv x);
    j2 := fun x : B => joinr (joinr x);
    j3 := fun x : C => joinr (joinl x);
    j12 :=
      fun (a : A) (b : B) =>
      jglue (1%equiv a) (joinr b);
    j13 :=
      fun (a : A) (c : C) =>
      jglue (1%equiv a) (joinl c);
    j23 :=
      fun (b : B) (c : C) => ap joinr (jglue c b)^;
    j123 :=
      fun (a : A) (b : B) (c : C) =>
      triangle_v (1%equiv a) (jglue c b)^
  |} == trijoin_rec (trijoinrecdata_id_sym f)
  (* And now we use naturality of the second [trijoin_rec] on the LHS. *)
  refine ((trijoin_rec_nat A B C (trijoin_rec f) _)^$ $@ _).A, B, C, P: Type
f: TriJoinRecData A C B P
trijoin_rec
  (trijoinrecdata_fun (trijoin_rec f)
     {|
       j1 := fun x : A => joinl (1%equiv x);
       j2 := fun x : B => joinr (joinr x);
       j3 := fun x : C => joinr (joinl x);
       j12 :=
         fun (a : A) (b : B) =>
         jglue (1%equiv a) (joinr b);
       j13 :=
         fun (a : A) (c : C) =>
         jglue (1%equiv a) (joinl c);
       j23 :=
         fun (b : B) (c : C) => ap joinr (jglue c b)^;
       j123 :=
         fun (a : A) (b : B) (c : C) =>
         triangle_v (1%equiv a) (jglue c b)^
     |}) $== trijoin_rec (trijoinrecdata_id_sym f)
  refine (fmap trijoin_rec _).A, B, C, P: Type
f: TriJoinRecData A C B P
trijoinrecdata_fun (trijoin_rec f)
  {|
    j1 := fun x : A => joinl (1%equiv x);
    j2 := fun x : B => joinr (joinr x);
    j3 := fun x : C => joinr (joinl x);
    j12 :=
      fun (a : A) (b : B) =>
      jglue (1%equiv a) (joinr b);
    j13 :=
      fun (a : A) (c : C) =>
      jglue (1%equiv a) (joinl c);
    j23 :=
      fun (b : B) (c : C) => ap joinr (jglue c b)^;
    j123 :=
      fun (a : A) (b : B) (c : C) =>
      triangle_v (1%equiv a) (jglue c b)^
  |} $-> trijoinrecdata_id_sym f
  (* Finally, we provide the needed [TriJoinRecPath]. *)
  bundle_trijoinrecpath; intros; cbn.A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
b: B
ap (trijoin_rec f) (jglue a (joinr b)) = j13 f a b
A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
c: C
ap (trijoin_rec f) (jglue a (joinl c)) = j12 f a c
A, B, C, P: Type
f: TriJoinRecData A C B P
b: B
c: C
ap (trijoin_rec f) (ap joinr (jglue c b)^) =
(j23 f c b)^
A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
b: B
c: C
prism'
  (ap_triangle (trijoin_rec f)
     (triangle_v a (jglue c b)^))
  (moveR_pV (j23 f c b) (j12 f a c) (j13 f a b)
     (j123 f a c b)^) ?Goal ?Goal0 ?Goal1
  -A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
b: B
ap (trijoin_rec f) (jglue a (joinr b)) = j13 f a b apply trijoin_rec_beta_join13.
  -A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
c: C
ap (trijoin_rec f) (jglue a (joinl c)) = j12 f a c apply trijoin_rec_beta_join12.
  -A, B, C, P: Type
f: TriJoinRecData A C B P
b: B
c: C
ap (trijoin_rec f) (ap joinr (jglue c b)^) =
(j23 f c b)^ lhs refine (ap _ (ap_V _ _)).A, B, C, P: Type
f: TriJoinRecData A C B P
b: B
c: C
ap (trijoin_rec f) (ap joinr (jglue c b))^ =
(j23 f c b)^
    lhs refine (ap_V (trijoin_rec f) _).A, B, C, P: Type
f: TriJoinRecData A C B P
b: B
c: C
(ap (trijoin_rec f) (ap joinr (jglue c b)))^ =
(j23 f c b)^
    apply (ap inverse).A, B, C, P: Type
f: TriJoinRecData A C B P
b: B
c: C
ap (trijoin_rec f) (ap joinr (jglue c b)) = j23 f c b
    apply trijoin_rec_beta_join23.
  -A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
b: B
c: C
prism'
  (ap_triangle (trijoin_rec f)
     (triangle_v a (jglue c b)^))
  (moveR_pV (j23 f c b) (j12 f a c) (j13 f a b)
     (j123 f a c b)^) (trijoin_rec_beta_join13 f a b)
  (trijoin_rec_beta_join12 f a c)
  (ap (ap (trijoin_rec f)) (ap_V joinr (jglue c b)) @
   (ap_V (trijoin_rec f) (ap joinr (jglue c b)) @
    ap inverse (trijoin_rec_beta_join23 f c b))) unfold prism'.A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
b: B
c: C
ap_triangle (trijoin_rec f)
  (triangle_v a (jglue c b)^) @
trijoin_rec_beta_join12 f a c =
(trijoin_rec_beta_join13 f a b @@
 (ap (ap (trijoin_rec f)) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f) (ap joinr (jglue c b)) @
   ap inverse (trijoin_rec_beta_join23 f c b)))) @
moveR_pV (j23 f c b) (j12 f a c) (j13 f a b)
  (j123 f a c b)^
    rewrite ap_trijoin_V.A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
b: B
c: C
((1 @@
  (ap (ap (trijoin_rec f)) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f) (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f) (join23 c b))
   (ap (trijoin_rec f) (join12 a c))
   (ap (trijoin_rec f) (join13 a b))
   (ap_trijoin (trijoin_rec f) a c b)^) @
trijoin_rec_beta_join12 f a c =
(trijoin_rec_beta_join13 f a b @@
 (ap (ap (trijoin_rec f)) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f) (ap joinr (jglue c b)) @
   ap inverse (trijoin_rec_beta_join23 f c b)))) @
moveR_pV (j23 f c b) (j12 f a c) (j13 f a b)
  (j123 f a c b)^
    rewrite trijoin_rec_beta_join123.A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
b: B
c: C
((1 @@
  (ap (ap (trijoin_rec f)) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f) (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f) (join23 c b))
   (ap (trijoin_rec f) (join12 a c))
   (ap (trijoin_rec f) (join13 a b))
   (((trijoin_rec_beta_join12 f a c @@
      trijoin_rec_beta_join23 f c b) @ j123 f a c b) @
    (trijoin_rec_beta_join13 f a b)^)^) @
trijoin_rec_beta_join12 f a c =
(trijoin_rec_beta_join13 f a b @@
 (ap (ap (trijoin_rec f)) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f) (ap joinr (jglue c b)) @
   ap inverse (trijoin_rec_beta_join23 f c b)))) @
moveR_pV (j23 f c b) (j12 f a c) (j13 f a b)
  (j123 f a c b)^
    set (f' := f).A, B, C, P: Type
f: TriJoinRecData A C B P
a: A
b: B
c: C
f':= f: TriJoinRecData A C B P
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((trijoin_rec_beta_join12 f' a c @@
      trijoin_rec_beta_join23 f' c b) @ j123 f' a c b) @
    (trijoin_rec_beta_join13 f' a b)^)^) @
trijoin_rec_beta_join12 f' a c =
(trijoin_rec_beta_join13 f' a b @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse (trijoin_rec_beta_join23 f' c b)))) @
moveR_pV (j23 f' c b) (j12 f' a c) (j13 f' a b)
  (j123 f' a c b)^
    destruct f as [f1 f2 f3 f12 f13 f23 f123]; cbn.A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((trijoin_rec_beta_join12 f' a c @@
      trijoin_rec_beta_join23 f' c b) @ f123 a c b) @
    (trijoin_rec_beta_join13 f' a b)^)^) @
trijoin_rec_beta_join12 f' a c =
(trijoin_rec_beta_join13 f' a b @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse (trijoin_rec_beta_join23 f' c b)))) @
moveR_pV (f23 c b) (f12 a c) (f13 a b) (f123 a c b)^
    generalize (f123 a c b).A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
forall p : f12 a c @ f23 c b = f13 a b,
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((trijoin_rec_beta_join12 f' a c @@
      trijoin_rec_beta_join23 f' c b) @ p) @
    (trijoin_rec_beta_join13 f' a b)^)^) @
trijoin_rec_beta_join12 f' a c =
(trijoin_rec_beta_join13 f' a b @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse (trijoin_rec_beta_join23 f' c b)))) @
moveR_pV (f23 c b) (f12 a c) (f13 a b) p^
    generalize (trijoin_rec_beta_join23 f' c b); cbn.A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
forall
(p : ap (trijoin_rec f') (join23 c b) = f23 c b)
(p0 : f12 a c @ f23 c b = f13 a b),
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((trijoin_rec_beta_join12 f' a c @@ p) @ p0) @
    (trijoin_rec_beta_join13 f' a b)^)^) @
trijoin_rec_beta_join12 f' a c =
(trijoin_rec_beta_join13 f' a b @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse p))) @
moveR_pV (f23 c b) (f12 a c) (f13 a b) p0^
    generalize (f23 c b).A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
forall (p : f2 c = f3 b)
(p0 : ap (trijoin_rec f') (join23 c b) = p)
(p1 : f12 a c @ p = f13 a b),
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((trijoin_rec_beta_join12 f' a c @@ p0) @ p1) @
    (trijoin_rec_beta_join13 f' a b)^)^) @
trijoin_rec_beta_join12 f' a c =
(trijoin_rec_beta_join13 f' a b @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse p0))) @
moveR_pV p (f12 a c) (f13 a b) p1^
    generalize (trijoin_rec_beta_join13 f' a b); cbn.A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
forall
(p : ap (trijoin_rec f') (join13 a b) = f13 a b)
(p0 : f2 c = f3 b)
(p1 : ap (trijoin_rec f') (join23 c b) = p0)
(p2 : f12 a c @ p0 = f13 a b),
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((trijoin_rec_beta_join12 f' a c @@ p1) @ p2) @ p^)^) @
trijoin_rec_beta_join12 f' a c =
(p @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse p1))) @
moveR_pV p0 (f12 a c) (f13 a b) p2^
    generalize (f13 a b).A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
forall (p : f1 a = f3 b)
(p0 : ap (trijoin_rec f') (join13 a b) = p)
(p1 : f2 c = f3 b)
(p2 : ap (trijoin_rec f') (join23 c b) = p1)
(p3 : f12 a c @ p1 = p),
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((trijoin_rec_beta_join12 f' a c @@ p2) @ p3) @
    p0^)^) @ trijoin_rec_beta_join12 f' a c =
(p0 @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse p2))) @ moveR_pV p1 (f12 a c) p p3^
    generalize (trijoin_rec_beta_join12 f' a c); cbn.A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
forall
(p : ap (trijoin_rec f') (join12 a c) = f12 a c)
(p0 : f1 a = f3 b)
(p1 : ap (trijoin_rec f') (join13 a b) = p0)
(p2 : f2 c = f3 b)
(p3 : ap (trijoin_rec f') (join23 c b) = p2)
(p4 : f12 a c @ p2 = p0),
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((p @@ p3) @ p4) @ p1^)^) @ p =
(p1 @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse p3))) @ moveR_pV p2 (f12 a c) p0 p4^
    generalize (f12 a c); cbn.A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
forall (p : f1 a = f2 c)
(p0 : ap (trijoin_rec f') (join12 a c) = p)
(p1 : f1 a = f3 b)
(p2 : ap (trijoin_rec f') (join13 a b) = p1)
(p3 : f2 c = f3 b)
(p4 : ap (trijoin_rec f') (join23 c b) = p3)
(p5 : p @ p3 = p1),
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((p0 @@ p4) @ p5) @ p2^)^) @ p0 =
(p2 @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse p4))) @ moveR_pV p3 p p1 p5^
    intros p12 beta12 p13 beta13 p23 beta23 p123.A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
p12: f1 a = f2 c
beta12: ap (trijoin_rec f') (join12 a c) = p12
p13: f1 a = f3 b
beta13: ap (trijoin_rec f') (join13 a b) = p13
p23: f2 c = f3 b
beta23: ap (trijoin_rec f') (join23 c b) = p23
p123: p12 @ p23 = p13
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   (((beta12 @@ beta23) @ p123) @ beta13^)^) @ beta12 =
(beta13 @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @
   ap inverse beta23))) @ 
moveR_pV p23 p12 p13 p123^
    induction beta12, beta13, beta23; cbn.A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
p123: ap (trijoin_rec f') (join12 a c) @
ap (trijoin_rec f') (join23 c b) =
ap (trijoin_rec f') (join13 a b)
((1 @@
  (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
   ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
 moveR_pV (ap (trijoin_rec f') (join23 c b))
   (ap (trijoin_rec f') (join12 a c))
   (ap (trijoin_rec f') (join13 a b))
   ((1 @ p123) @ 1)^) @ 1 =
(1 @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  (ap_V (trijoin_rec f') (ap joinr (jglue c b)) @ 1))) @
moveR_pV (ap (trijoin_rec f') (join23 c b))
  (ap (trijoin_rec f') (join12 a c))
  (ap (trijoin_rec f') (join13 a b)) p123^
    rewrite 3 concat_p1, concat_1p.A, B, C, P: Type
f1: A -> P
f2: C -> P
f3: B -> P
f12: forall (a : A) (b : C), f1 a = f2 b
f13: forall (a : A) (c : B), f1 a = f3 c
f23: forall (b : C) (c : B), f2 b = f3 c
f123: forall (a : A) (b : C) (c : B),
f12 a b @ f23 b c = f13 a c
a: A
b: B
c: C
f':= {|
  j1 := f1;
  j2 := f2;
  j3 := f3;
  j12 := f12;
  j13 := f13;
  j23 := f23;
  j123 := f123
|}: TriJoinRecData A C B P
p123: ap (trijoin_rec f') (join12 a c) @
ap (trijoin_rec f') (join23 c b) =
ap (trijoin_rec f') (join13 a b)
(1 @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
moveR_pV (ap (trijoin_rec f') (join23 c b))
  (ap (trijoin_rec f') (join12 a c))
  (ap (trijoin_rec f') (join13 a b)) p123^ =
(1 @@
 (ap (ap (trijoin_rec f')) (ap_V joinr (jglue c b)) @
  ap_V (trijoin_rec f') (ap joinr (jglue c b)))) @
moveR_pV (ap (trijoin_rec f') (join23 c b))
  (ap (trijoin_rec f') (join12 a c))
  (ap (trijoin_rec f') (join13 a b)) p123^
    reflexivity.
Defined.

(** Here is our first hexagon law.  This is not the usual hexagon axiom, but we will see that it is equivalent, and is itself useful.  This law states that the following diagram commutes, where we write [*] for [Join]:
<<
    A * (B * C) -> A * (C * B) -> C * (A * B)
        |                            |
        v                            v
    B * (A * C) -> B * (C * A) -> C * (B * A)
>>
Here every arrow is either [trijoin_twist _ _ _] or [trijoin_id_sym _ _ _], and they alternate as you go around.  These correspond to the permutations (1,2) and (2,3) in the symmetric group on three letters.  We already know that they are their own inverses, i.e., they have order two.  The above says that the composite (1,2)(2,3) has order three.  These are the only relations in this presentation of [S_3].  Note also that every object in this diagram is parenthesized in the same way.  That will be important in our proof. *)
Definition hexagon_join_twist_sym A B C
  : trijoin_id_sym C A B o trijoin_twist A C B o trijoin_id_sym A B C
    == trijoin_twist B C A o trijoin_id_sym B A C o trijoin_twist A B C.A, B, C: Type
trijoin_id_sym C A B o trijoin_twist A C B
o trijoin_id_sym A B C ==
trijoin_twist B C A o trijoin_id_sym B A C
o trijoin_twist A B C
Proof.A, B, C: Type
trijoin_id_sym C A B o trijoin_twist A C B
o trijoin_id_sym A B C ==
trijoin_twist B C A o trijoin_id_sym B A C
o trijoin_twist A B C
  (* It's enough to show that both sides induces the same natural transformation under the covariant Yoneda embedding, i.e., after postcomposing with a general function [f]. *)
  rapply (opyon_faithful_0gpd (A:=Type)).A, B, C: Type
forall (c : Type) (h : TriJoin C B A $-> c),
h $o
(fun x : TriJoin A B C =>
 trijoin_id_sym C A B
   (trijoin_twist A C B (trijoin_id_sym A B C x))) $==
h $o
(fun x : TriJoin A B C =>
 trijoin_twist B C A
   (trijoin_id_sym B A C (trijoin_twist A B C x)))
  intros P f.A, B, C, P: Type
f: TriJoin C B A $-> P
f $o
(fun x : TriJoin A B C =>
 trijoin_id_sym C A B
   (trijoin_twist A C B (trijoin_id_sym A B C x))) $==
f $o
(fun x : TriJoin A B C =>
 trijoin_twist B C A
   (trijoin_id_sym B A C (trijoin_twist A B C x)))
  (* We replace [f] by [trijoin_rec t] for generic [t].  This will allow induction later. *)
  pose proof (p := issect_trijoin_rec_inv f).A, B, C, P: Type
f: TriJoin C B A $-> P
p: trijoin_rec (trijoin_rec_inv f) $== f
f $o
(fun x : TriJoin A B C =>
 trijoin_id_sym C A B
   (trijoin_twist A C B (trijoin_id_sym A B C x))) $==
f $o
(fun x : TriJoin A B C =>
 trijoin_twist B C A
   (trijoin_id_sym B A C (trijoin_twist A B C x)))
  intro x; refine ((p _)^ @ _ @ p _); clear p.A, B, C, P: Type
f: TriJoin C B A $-> P
x: TriJoin A B C
trijoin_rec (trijoin_rec_inv f)
  (trijoin_id_sym C A B
     (trijoin_twist A C B (trijoin_id_sym A B C x))) =
trijoin_rec (trijoin_rec_inv f)
  (trijoin_twist B C A
     (trijoin_id_sym B A C (trijoin_twist A B C x)))
  generalize (trijoin_rec_inv f) as t.A, B, C, P: Type
f: TriJoin C B A $-> P
x: TriJoin A B C
forall t : TriJoinRecData C B A P,
trijoin_rec t
  (trijoin_id_sym C A B
     (trijoin_twist A C B (trijoin_id_sym A B C x))) =
trijoin_rec t
  (trijoin_twist B C A
     (trijoin_id_sym B A C (trijoin_twist A B C x)))
  intro t; clear f.A, B, C, P: Type
x: TriJoin A B C
t: TriJoinRecData C B A P
trijoin_rec t
  (trijoin_id_sym C A B
     (trijoin_twist A C B (trijoin_id_sym A B C x))) =
trijoin_rec t
  (trijoin_twist B C A
     (trijoin_id_sym B A C (trijoin_twist A B C x)))
  (* Now we use how these various maps postcompose with [trijoin_rec foo]. *)
  lhs rapply trijoin_rec_id_sym.A, B, C, P: Type
x: TriJoin A B C
t: TriJoinRecData C B A P
trijoin_rec (trijoinrecdata_id_sym t)
  (trijoin_twist A C B (trijoin_id_sym A B C x)) =
trijoin_rec t
  (trijoin_twist B C A
     (trijoin_id_sym B A C (trijoin_twist A B C x)))
  lhs rapply trijoin_rec_trijoin_twist.A, B, C, P: Type
x: TriJoin A B C
t: TriJoinRecData C B A P
trijoin_rec
  (trijoinrecdata_twist C A B P
     (trijoinrecdata_id_sym t))
  (trijoin_id_sym A B C x) =
trijoin_rec t
  (trijoin_twist B C A
     (trijoin_id_sym B A C (trijoin_twist A B C x)))
  lhs rapply trijoin_rec_id_sym.A, B, C, P: Type
x: TriJoin A B C
t: TriJoinRecData C B A P
trijoin_rec
  (trijoinrecdata_id_sym
     (trijoinrecdata_twist C A B P
        (trijoinrecdata_id_sym t))) x =
trijoin_rec t
  (trijoin_twist B C A
     (trijoin_id_sym B A C (trijoin_twist A B C x)))
  rhs rapply trijoin_rec_trijoin_twist.A, B, C, P: Type
x: TriJoin A B C
t: TriJoinRecData C B A P
trijoin_rec
  (trijoinrecdata_id_sym
     (trijoinrecdata_twist C A B P
        (trijoinrecdata_id_sym t))) x =
trijoin_rec (trijoinrecdata_twist C B A P t)
  (trijoin_id_sym B A C (trijoin_twist A B C x))
  rhs rapply trijoin_rec_id_sym.A, B, C, P: Type
x: TriJoin A B C
t: TriJoinRecData C B A P
trijoin_rec
  (trijoinrecdata_id_sym
     (trijoinrecdata_twist C A B P
        (trijoinrecdata_id_sym t))) x =
trijoin_rec
  (trijoinrecdata_id_sym
     (trijoinrecdata_twist C B A P t))
  (trijoin_twist A B C x)
  rhs rapply trijoin_rec_trijoin_twist.A, B, C, P: Type
x: TriJoin A B C
t: TriJoinRecData C B A P
trijoin_rec
  (trijoinrecdata_id_sym
     (trijoinrecdata_twist C A B P
        (trijoinrecdata_id_sym t))) x =
trijoin_rec
  (trijoinrecdata_twist B A C P
     (trijoinrecdata_id_sym
        (trijoinrecdata_twist C B A P t))) x
  revert x; refine (fmap trijoin_rec _).A, B, C, P: Type
t: TriJoinRecData C B A P
trijoinrecdata_id_sym
  (trijoinrecdata_twist C A B P
     (trijoinrecdata_id_sym t)) $->
trijoinrecdata_twist B A C P
  (trijoinrecdata_id_sym
     (trijoinrecdata_twist C B A P t))
  bundle_trijoinrecpath; intros; cbn.A, B, C, P: Type
t: TriJoinRecData C B A P
a: A
b: B
(j23 t b a)^ = (j23 t b a)^
A, B, C, P: Type
t: TriJoinRecData C B A P
a: A
c: C
(j13 t c a)^ = (j13 t c a)^
A, B, C, P: Type
t: TriJoinRecData C B A P
b: B
c: C
(j12 t c b)^ = (j12 t c b)^
A, B, C, P: Type
t: TriJoinRecData C B A P
a: A
b: B
c: C
prism'
  (moveR_pV (j12 t c b) (j13 t c a)^ (j23 t b a)^
     (moveR_Vp (j12 t c b) (j23 t b a)^ (j13 t c a)
        (moveR_pV (j23 t b a) (j12 t c b) (j13 t c a)
           (j123 t c b a)^)^)^)
  (moveR_Vp (j12 t c b)^ (j13 t c a)^ (j23 t b a)
     (moveR_pV (j13 t c a) (j12 t c b)^ (j23 t b a)
        (moveR_Vp (j13 t c a) (j23 t b a) (j12 t c b)
           (j123 t c b a)^)^)^) ?Goal ?Goal0 ?Goal1
  1, 2, 3: reflexivity.A, B, C, P: Type
t: TriJoinRecData C B A P
a: A
b: B
c: C
prism'
  (moveR_pV (j12 t c b) (j13 t c a)^ (j23 t b a)^
     (moveR_Vp (j12 t c b) (j23 t b a)^ (j13 t c a)
        (moveR_pV (j23 t b a) (j12 t c b) (j13 t c a)
           (j123 t c b a)^)^)^)
  (moveR_Vp (j12 t c b)^ (j13 t c a)^ (j23 t b a)
     (moveR_pV (j13 t c a) (j12 t c b)^ (j23 t b a)
        (moveR_Vp (j13 t c a) (j23 t b a) (j12 t c b)
           (j123 t c b a)^)^)^) 1 1 1
  by triangle_ind t c b a.
Defined.

(** Next we paste on a naturality square for [join_sym] on the right of the diagram:
<<
    A * (B * C) -> A * (C * B) -> C * (A * B) -> (A * B) * C
        |                            |                |
        v                            v                v
    B * (A * C) -> B * (C * A) -> C * (B * A) -> (B * A) * C
>>
The new horizontal maps are [join_sym _ _] and the new vertical map is [functor_join (join_sym A B) idmap]. This makes both horizontal composites definitionally equal to [join_assoc _ _ _], so the statement is about a square. *)
Definition square_join_sym_assoc_twist A B C
  : functor_join (join_sym A B) idmap o join_assoc A B C
    == join_assoc B A C o trijoin_twist A B C.A, B, C: Type
functor_join (join_sym A B) idmap o join_assoc A B C ==
join_assoc B A C o trijoin_twist A B C
Proof.A, B, C: Type
functor_join (join_sym A B) idmap o join_assoc A B C ==
join_assoc B A C o trijoin_twist A B C
  unfold join_assoc; cbn.A, B, C: Type
(fun x : Join A (Join B C) =>
 functor_join (join_sym A B) idmap
   (join_sym C (Join A B)
      (trijoin_twist A C B (trijoin_id_sym A B C x)))) ==
(fun x : TriJoin A B C =>
 join_sym C (Join B A)
   (trijoin_twist B C A
      (trijoin_id_sym B A C (trijoin_twist A B C x))))
  intro x; lhs_V rapply join_sym_nat.A, B, C: Type
x: Join A (Join B C)
join_sym C (Join B A)
  (functor_join idmap (join_sym A B)
     (trijoin_twist A C B (trijoin_id_sym A B C x))) =
join_sym C (Join B A)
  (trijoin_twist B C A
     (trijoin_id_sym B A C (trijoin_twist A B C x)))
  apply ap.A, B, C: Type
x: Join A (Join B C)
functor_join idmap (join_sym A B)
  (trijoin_twist A C B (trijoin_id_sym A B C x)) =
trijoin_twist B C A
  (trijoin_id_sym B A C (trijoin_twist A B C x))
  apply hexagon_join_twist_sym.
Defined.

(** Finally, we paste on the defining square for [join_assoc] on the left to get the hexagon axiom for the symmetric monoidal structure:
<<
    A * (C * B) -> A * (B * C) -> (A * B) * C
         |              |              |
         v              v              v
    (A * C) * B -> B * (A * C) -> (B * A) * C
>>
The right-hand square is a horizontally-compressed version of the rectangle from the previous result, whose horizontal arrows are associativity. In the left-hand square, the new vertical map is [join_assoc A C B] and the horizontal maps are [trijoin_id_sym A C B] and [join_sym (Join A C) B]. *)
Definition hexagon_join_assoc_sym A B C
  : functor_join (join_sym A B) idmap o join_assoc A B C o trijoin_id_sym A C B
    == join_assoc B A C o join_sym (Join A C) B o join_assoc A C B.A, B, C: Type
functor_join (join_sym A B) idmap o join_assoc A B C
o trijoin_id_sym A C B ==
join_assoc B A C o join_sym (Join A C) B
o join_assoc A C B
Proof.A, B, C: Type
functor_join (join_sym A B) idmap o join_assoc A B C
o trijoin_id_sym A C B ==
join_assoc B A C o join_sym (Join A C) B
o join_assoc A C B
  intro x.A, B, C: Type
x: TriJoin A C B
functor_join (join_sym A B) idmap
  (join_assoc A B C (trijoin_id_sym A C B x)) =
join_assoc B A C
  (join_sym (Join A C) B (join_assoc A C B x))
  refine (square_join_sym_assoc_twist A B C _ @ _).A, B, C: Type
x: TriJoin A C B
join_assoc B A C
  (trijoin_twist A B C (trijoin_id_sym A C B x)) =
join_assoc B A C
  (join_sym (Join A C) B (join_assoc A C B x))
  apply ap.A, B, C: Type
x: TriJoin A C B
trijoin_twist A B C (trijoin_id_sym A C B x) =
join_sym (Join A C) B (join_assoc A C B x)
  simpl.A, B, C: Type
x: TriJoin A C B
trijoin_twist A B C
  (functor_join idmap (join_sym C B) x) =
join_sym (Join A C) B
  (join_sym B (Join A C)
     (trijoin_twist A B C
        (functor_join idmap (join_sym C B) x)))
  symmetry.A, B, C: Type
x: TriJoin A C B
join_sym (Join A C) B
  (join_sym B (Join A C)
     (trijoin_twist A B C
        (functor_join idmap (join_sym C B) x))) =
trijoin_twist A B C
  (functor_join idmap (join_sym C B) x)
  exact (eissect (equiv_join_sym B (Join A C)) _).
Defined.