{A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C') : trijoin_id_sym A' B' C' o functor_join f (functor_join g h) == functor_join f (functor_join h g) o trijoin_id_sym A B C. Proof. intro x; simpl. lhs_V nrapply functor_join_compose. rhs_V nrapply functor_join_compose. apply functor2_join. - reflexivity. - apply join_sym_nat. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.