{A B : Type} (f : A -> B) : Factorization (@IsConnMap O) (@MapIn O) f. Proof. pose mapinO_pr1. refine (Build_Factorization {b : B & O (hfiber f b)} (fun a => (f a ; to O _ (a;1))) pr1 (fun a => 1) _ _). pose conn_map_functor_sigma. exact (conn_map_compose O (equiv_fibration_replacement f) (functor_sigma idmap (fun b => to O (hfiber f b)))). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Factorization Limits.Pullback.