(A B C : Type) : NatEquiv (opyon_0gpd (TriJoin A B C)) (opyon_0gpd (TriJoin B A C)) := natequiv_compose (trijoin_rec_natequiv B A C) (natequiv_compose (trijoinrecdata_twist_natequiv A B C) (trijoin_rec_inv_natequiv A B C)).
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.