{A} {P Q : A -> Type} (g : forall a, P a -> Q a) `{forall a, O_inverts (g a)} : O_inverts (functor_sigma idmap g). Proof. apply O_inverts_from_extendable; intros Z Z_inO. apply ooextendable_functor_sigma_id; intros a. nrapply ooextendable_O_inverts; exact _. 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.