{A B C P : Type} (f : TriJoinRecData A B C P) (b : B) (c : C) : ap (trijoin_rec f) (join23 b c) = j23 f b c. Proof. unfold trijoin_rec, join23. lhs_V nrapply (ap_compose joinr); simpl. apply Join_rec_beta_jglue. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.