{A B C P : Type} (f : TriJoin A B C -> P) (a : A) (b : B) (c : C) : ap_trijoin f a b c = (1 @@ ap_compose _ f _)^ @ (transport_paths_Fr _ _)^ @ apD (fun x => ap f (jglue a x)) (jglue b c). Proof. nrapply ap_trijoin_general_transport. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.