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. Proof. rapply (opyon_faithful_0gpd (A:=Type)). intros P f. pose proof (p := issect_trijoin_rec_inv f). intro x; refine ((p _)^ @ _ @ p _); clear p. generalize (trijoin_rec_inv f) as t. intro t; clear f. lhs rapply trijoin_rec_id_sym. lhs rapply trijoin_rec_trijoin_twist. lhs rapply trijoin_rec_id_sym. rhs rapply trijoin_rec_trijoin_twist. rhs rapply trijoin_rec_id_sym. rhs rapply trijoin_rec_trijoin_twist. revert x; refine (fmap trijoin_rec _). bundle_trijoinrecpath; intros; cbn. 1, 2, 3: reflexivity. by triangle_ind t c b a. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.