{A B C A' B' C' P} (k : TriJoinRecData A B C P) {f f' : A' -> A} {g g' : B' -> B} {h h' : C' -> C} (p : f == f') (q : g == g') (r : h == h') : trijoinrecdata_tricomp k f g h $== trijoinrecdata_tricomp k f' g' h'. Proof. snrapply Build_TriJoinRecPath; intros; cbn. - apply ap, p. - apply ap, q. - apply ap, r. - induction (p a), (q b); by apply equiv_p1_1q. - induction (p a), (r c); by apply equiv_p1_1q. - induction (q b), (r c); by apply equiv_p1_1q. - induction (p a), (q b), (r c); apply prism_id. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.