{A B : Type} {f : A -> B} (fact : Factorization (@IsConnMap O) (@MapIn O) f) (a : A) (b : B) (p : factor2 fact (factor1 fact a) = b) : (O_hfiber_O_fact fact b)^-1 (factor1 fact a ; p) = to O _ (a ; p). Proof. set (g := factor1 fact); set (h := factor2 fact). apply moveR_equiv_V. unfold O_hfiber_O_fact. ev_equiv. apply moveL_equiv_M. transitivity (exist (fun (w : hfiber h b) => O (hfiber g w.1)) (g a; p) (to O (hfiber g (g a)) (a ; 1))). - apply moveR_equiv_V; reflexivity. - apply moveL_equiv_V. transitivity (to O _ (exist (fun (w : hfiber h b) => (hfiber g w.1)) (g a; p) (a ; 1))). + cbn; repeat rewrite O_rec_beta; reflexivity. + destruct p; symmetry; apply to_O_natural. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.