{A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P} (f : TriJoinRecData' j1' j2' j3') : TriJoinRecData A B C P := Build_TriJoinRecData j1' j2' j3' (j12' f) (j13' f) (j23' f) (j123' f).
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.