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). Proof. intro x. rapply moveR_equiv_M. unfold equiv_join_empty_right at 1; cbn. lhs nrapply functor_join_join_rec; cbn. lhs nrapply trijoin_rec_trijoin_twist. revert x. apply moveR_trijoin_rec. snrapply Build_TriJoinRecPath; intros; cbn. 3, 5, 6, 7: by destruct c. - reflexivity. - reflexivity. - apply equiv_p1_1q. symmetry. lhs nrapply (ap_compose (functor_join idmap _) _ (join12 a b)). lhs nrapply ap. 1: apply functor_join_beta_jglue. apply join_sym_beta_jglue. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.