trijoin_twist_nat' {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C') : trijoin_twist A' B' C' o functor_trijoin f g h == functor_trijoin g f h o trijoin_twist A B C. Proof. intro x. rhs nrapply trijoin_rec_trijoin_twist. nrapply trijoin_rec_functor_trijoin. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.