(A B C : Type) : TriJoin A B C <~> TriJoin B A C := equiv_homotopic_inverse (' A B C) (trijoin_twist_homotopic A B C) (trijoin_twist_homotopic B A C).
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.