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