fact: Definition ap_trijoin_V {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)^.
imports: Basics Types.Paths WildCat Join.Core HoTT.Tactics