{A B C A' B' C'} (f : A <~> A') (g : B <~> B') (h : C <~> C') : TriJoin A B C <~> TriJoin A' B' C' := Build_Equiv _ _ (functor_trijoin f g h) _. Local Lemma ap_triangle_functor_join {A BC A' P} (f : A -> A') (g : BC -> P) (a : A) {b c : BC} (bc : b = c) (bc' : g b = g c) (beta_jg : ap g bc = bc') : ap_triangle (functor_join f g) (triangle_v a bc) @ functor_join_beta_jglue f g a c = (functor_join_beta_jglue f g a b @@ ((ap_compose joinr (functor_join f g) bc)^ @ (ap_compose g joinr bc @ ap (ap joinr) beta_jg))) @ triangle_v (f a) bc'. Proof. induction bc, beta_jg; simpl. transitivity (concat_p1 _ @ functor_join_beta_jglue f g a b). - refine (_ @@ 1). unfold ap_triangle. apply moveR_Vp; symmetry. exact (ap_pp_concat_p1 (functor_join f g) (jglue a b)). - apply moveR_Mp; symmetry. exact (concat_p_pp _ _ _ @ whiskerR_p1 _). Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.