{A B C A' B' C' P} (k : TriJoinRecData A B C P) (f : A' -> A) (g : B' -> B) (h : C' -> C) : TriJoinRecData A' B' C' P := {| j1 := j1 k o f; j2 := j2 k o g; j3 := j3 k o h; j12 := fun a b => j12 k (f a) (g b); j13 := fun a c => j13 k (f a) (h c); j23 := fun b c => j23 k (g b) (h c); j123 := fun a b c => j123 k (f a) (g b) (h c); |}.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.