{A B C A' B' C' P} {k l : TriJoinRecData A B C P} (p : k $== l) (f : A' -> A) (g : B' -> B) (h : C' -> C) : trijoinrecdata_tricomp k f g h $== trijoinrecdata_tricomp l f g h. Proof. unfold trijoinrecdata_tricomp; destruct p. snrapply Build_TriJoinRecPath; intros; cbn; apply_hyp. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.