fact: Definition O_inverts_functor_sigma_id {A} {P Q : A -> Type} (g : forall a, P a -> Q a) `{forall a, O_inverts (g a)} : O_inverts (functor_sigma idmap g).
imports: HoTT.Basics HoTT.Types Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback PathAny Colimits.Pushout