FactorizationSystem. Proof. refine (Build_FactorizationSystem (@IsConnMap O) _ _ _ (@MapIn O) _ _ _ (@image) _). intros A B f fact fact'. simple refine (Build_PathFactorization fact fact' _ _ _ _). - refine (_ oE equiv_fibration_replacement (factor2 fact)). refine ((equiv_fibration_replacement (factor2 fact'))^-1 oE _). apply equiv_functor_sigma_id; intros b; simpl. apply equiv_O_factor_hfibers. - intros a; exact (pr1_path (equiv_O_factor_hfibers_beta f fact fact' a)). - intros x. exact ((equiv_O_factor_hfibers f fact fact' (factor2 fact x) (x ; 1)).2 ^). - intros a. apply moveR_pM. refine ((inv_V _)^ @ _ @ inv_V _); apply inverse2. refine (_ @ pr2_path (equiv_O_factor_hfibers_beta f fact fact' a)). refine (_ @ (transport_paths_Fl _ _)^). exact (inv_pp _ _ @ (1 @@ inv_V _)). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.