{A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C') : join_assoc A' B' C' o functor_join f (functor_join g h) == functor_join (functor_join f g) h o join_assoc A B C. Proof. intro x. unfold join_assoc; cbn. rhs_V nrapply join_sym_nat. apply (ap _). rhs_V nrapply trijoin_twist_nat. apply (ap _). apply trijoin_id_sym_nat. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.