{A B} (f : A -> B) `{IsEquiv _ _ f} : IsEquiv (fmap F f). Proof. refine (equiv_induction (fun A' e => IsEquiv (fmap F e)) _ _ (Build_Equiv _ _ f _)). refine (transport _ (fmap_idmap F)^ _); try apply isequiv_idmap. Defined.
Require Import HoTT.Basics Types.Universe.