{A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P} {f g : TriJoinRecData' j1' j2' j3'} (h : TriJoinRecPath' f g) : TriJoinRecPath (bundle_trijoinrecdata f) (bundle_trijoinrecdata g). Proof. snrapply Build_TriJoinRecPath. 1, 2, 3: reflexivity. 1, 2, 3: intros; apply equiv_p1_1q. - apply (h12' h). - apply (h13' h). - apply (h23' h). - cbn beta zeta. intros a b c. apply bundle_prism, (h123' h). Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.