equiv_trijoin_twist' (A B C : Type) : TriJoin A B C <~> TriJoin B A C. Proof. rapply (opyon_equiv_0gpd (A:=Type)). apply trijoinrecdata_fun_twist. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.