trijoin_id_sym_nat' {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C') : trijoin_id_sym A' B' C' o functor_trijoin f g h == functor_trijoin f h g o trijoin_id_sym A B C. Proof. intro x. lhs_V nrefine (ap _ (functor_trijoin_as_functor_join f g h x)). rhs_V nrapply functor_trijoin_as_functor_join. apply trijoin_id_sym_nat. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.