{A : Type} {P Q : A -> Type} (f : forall a, P a -> Q a) `{IsConnMap O _ _ (functor_sigma idmap f)} : forall a, IsConnMap O (f a). Proof. intros a q. refine (isconnected_equiv' O (hfiber (functor_sigma idmap f) (a;q)) _ _). exact (hfiber_functor_sigma_idmap P Q f a q). 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.