(A B C : Type) : trijoin_twist A B C == equiv_trijoin_twist' A B C. Proof. symmetry. rapply (fmap trijoin_rec). bundle_trijoinrecpath; intros; cbn. 1: refine (ap inverse _). 1, 2, 3: apply ap_idmap. generalize (join123 b a c). generalize (join23 (A:=B) a c). generalize (join13 (B:=A) b c). generalize (join12 (C:=C) b a). generalize (join3 (A:=B) (B:=A) c). generalize (join2 (A:=B) (C:=C) a). generalize (join1 (B:=A) (C:=C) b). intros k1 k2 k3 k12 k13 k23 k123. induction k12, k23, k123. reflexivity. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.