proposition: Lemma O_hfiber_O_fact {A B : Type} {f : A -> B} (fact : Factorization (@IsConnMap O) (@MapIn O) f) (b : B) : O (hfiber (factor2 fact o factor1 fact) b) <~> hfiber (factor2 fact) b.
proof: Proof. refine (_ oE (equiv_O_functor O (hfiber_compose (factor1 fact) (factor2 fact) b))). nrefine (equiv_sigma_contr (fun w => O (hfiber (factor1 fact) w.1)) oE _). - intros w; exact (inclass1 fact w.1). - nrefine ((equiv_sigma_inO_O (fun w => hfiber (factor1 fact) w.1))^-1)%equiv. exact (inclass2 fact b). Defined.
imports: HoTT.Basics HoTT.Types HFiber Extensions Factorization Limits.Pullback ReflectiveSubuniverse