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. Proof. intro x. refine (square_join_sym_assoc_twist A B C _ @ _). apply ap. simpl. symmetry. exact (eissect (equiv_join_sym B (Join A C)) _). Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.