{A B C P : Type} (f : TriJoin A B C -> P) (a : A) (b : B) (c : C) : ap f (join12 a b) @ ap f (join23 b c) = ap f (join13 a c). Proof. nrapply ap_trijoin_general. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.