fact: Definition equiv_total_iff_equiv_fiberwise {A} (P Q : A -> Type) (g : forall a, P a -> Q a) : IsEquiv (functor_sigma idmap g) <-> forall a, IsEquiv (g a).
imports: HoTT.Basics Types.Sigma Types.Forall Types.Arrow Types.Paths