{A B C P : Type} (f : TriJoinRecData A B C P) : TriJoin A B C $-> P. Proof. snrapply Join_rec. - exact (j1 f). - snrapply Join_rec. + exact (j2 f). + exact (j3 f). + exact (j23 f). - intro a. snrapply Join_ind; cbn beta. + exact (j12 f a). + exact (j13 f a). + intros b c. lhs nrapply transport_paths_Fr. exact (1 @@ Join_rec_beta_jglue _ _ _ _ _ @ j123 f a b c). Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.