{A B : Type} {P : B -> Type} (f : A -> B) `{!IsEquiv f} (h : forall a, P (f a)) : forall a, functor_forall_equiv_pb f h (f a) = h a. Proof. intro a; srapply (_ @ apD h (eissect f a)); srapply (_ @ (transport_compose _ _ _ _)^). srapply ap10; apply ap; apply eisadj. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids