`{P : A -> Type} `{Q : B -> Type} (f0 : A -> B) `{!IsEquiv f0} (f1 : forall a:A, P a -> Q (f0 a)) : (forall a:A, P a) -> (forall b:B, Q b). Proof. nrapply (functor_forall f0^-1). intros b u. refine ((eisretr f0 b) # _). exact (f1 _ u). Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids