fact: Definition trijoinrecdata_tricomp2 {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'.
imports: Basics Types.Paths WildCat Join.Core HoTT.Tactics