{A B C P Q : Type} (g : P -> Q) (f : TriJoinRecData A B C P) : TriJoinRecData A B C Q. Proof. snrapply Build_TriJoinRecData. - exact (g o j1 f). - exact (g o j2 f). - exact (g o j3 f). - exact (fun a b => ap g (j12 f a b)). - exact (fun a c => ap g (j13 f a c)). - exact (fun b c => ap g (j23 f b c)). - intros a b c; cbn beta. exact (ap_triangle g (j123 f a b c)). Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.