`{Funext} {A B : Type} (f : A -> B) `{IsConnMap O _ _ f} (P : B -> Type) `{forall b:B, In O (P b)} : IsEquiv (fun (g : forall b:B, P b) => g oD f). Proof. apply isequiv_contr_map; intros d. apply contr_inhabited_hprop. - nrefine (@istrunc_equiv_istrunc {g : forall b, P b & g oD f == d} _ _ _ _). { refine (equiv_functor_sigma_id _); intros g. apply equiv_path_forall. } apply hprop_allpath. intros g h. exact (allpath_extension_conn_map f P d g h). - exists (conn_map_elim f P d). apply path_forall; intros x; apply conn_map_comp. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.