(A B C P : Type) : trijoinrecdata_twist B A C P $o trijoinrecdata_twist A B C P $== Id _. Proof. intro f; simpl. bundle_trijoinrecpath. all: intros; cbn. - apply inv_V. - reflexivity. - reflexivity. - by triangle_ind f a b c. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.