{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). Proof. intros [c q]. nrefine (isconnected_equiv' O _ (hfiber_functor_hfiber p b c q)^-1 _). apply OO_isconnected_hfiber. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Extensions Limits.Pullback. Require Import Modality Accessible Modalities.Localization.