fact: Definition 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) := OO_conn_map_functor_hfiber O O p b.
imports: HoTT.Basics HoTT.Types HFiber Limits.Pullback Factorization Truncations.Core Modality Accessible Localization Descent Separated