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. Proof. unfold join_assoc; cbn. intro x; lhs_V rapply join_sym_nat. apply ap. apply hexagon_join_twist_sym. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.