{A B C P} (f : TriJoinRecData B A C P) : trijoin_rec f o trijoin_twist A B C == trijoin_rec (trijoinrecdata_twist _ _ _ _ f). Proof. transitivity (trijoin_rec f o equiv_trijoin_twist' A B C). 1: exact (fun x => ap (trijoin_rec f) (trijoin_twist_homotopic A B C x)). refine ((isnat_natequiv (trijoinrecdata_fun_twist B A C) (trijoin_rec f) _)^$ $@ _). change (?L $== ?R) with (trijoin_rec (trijoinrecdata_twist B A C P (trijoin_rec_inv (trijoin_rec f))) $== R). refine (fmap trijoin_rec _). refine (fmap (trijoinrecdata_twist B A C P) _). apply trijoin_rec_beta. Defined.
Require Import Basics Types WildCat Join.Core Join.TriJoin Spaces.Nat.Core.