{A B C P : Type} (f : TriJoin A B C -> P) (a : A) (b : B) (c : C) : ap_triangle f (triangle_v a (jglue b c)^) = (1 @@ (ap (ap f) (ap_V joinr _) @ ap_V f _)) @ moveR_pV _ _ _ (ap_trijoin f a b c)^. Proof. nrapply ap_trijoin_general_V. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.