{A B : Type} `{Q : B -> Type} (f0 : A -> B) `{!IsEquiv f0} : (forall a:A, Q (f0 a)) -> (forall b:B, Q b) := functor_forall_equiv f0 (fun _ => idmap).
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids