fact: Definition OO_conn_map_functor_hfiber {A B C D : Type} {f : A -> B} {g : C -> D} {h : A -> C} {k : B -> D} `{IsConnMap O' _ _ h, IsConnMap O' _ _ k} (p : k o f == g o h) (b : B) : IsConnMap O (functor_hfiber p b).
imports: HoTT.Basics HoTT.Types HFiber Extensions Limits.Pullback Modality Accessible Localization