(x : A) : ap p (lift_factsys_tri1 x)^ @ lift_factsys_tri2 (i x) = h x. Proof. unfold lift_factsys_tri1, lift_factsys_tri2. Open Scope long_path_scope. pose (r := path_fact_factors (path_factor factsys (p o f) fact fact') x : q2 (f1 x) @ ap g2 (q1 x) @ (gf (i x) @ (h x)^) = ap p (ff x)). rewrite concat_p_pp in r. apply moveL_pM, moveR_Vp in r. refine (_ @ r); clear r. repeat rewrite inv_pp; repeat rewrite ap_pp; rewrite ap_V. repeat rewrite concat_pp_p; apply whiskerL. repeat rewrite concat_p_pp; apply whiskerR. rewrite (ap_compose q^-1 f2), <- ap_pp, <- inv_pp. unfold lift_factsys. rewrite <- ap_pp. rewrite <- ap_V, <- ap_compose. rewrite (concat_Ap q2). rewrite concat_pp_p; apply whiskerL. rewrite ap_compose. rewrite <- ap_pp. apply ap. rewrite inv_pp, ap_pp, ap_V. rewrite <- eisadj. rewrite concat_pp_p; apply moveR_Vp. rewrite <- ap_V, inv_V, <- ap_compose. exact (concat_A1p (eisretr q) (q1 x)). Close Scope long_path_scope. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.