(a : A) : equiv_O_factor_hfibers (factor2 fact (factor1 fact a)) (factor1 fact a ; 1) = (factor1 fact' a ; (H a)^). Proof. unfold equiv_O_factor_hfibers. ev_equiv. apply moveR_equiv_M. do 2 rewrite O_hfiber_O_fact_inverse_beta. unfold equiv_fun, equiv_O_functor. transitivity (to O _ (equiv_hfiber_homotopic (factor2 fact o factor1 fact) (factor2 fact' o factor1 fact') H (factor2 fact (factor1 fact a)) (a;1))). - refine (to_O_natural O _ _). - apply ap. simpl. apply ap; auto with path_hints. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.