proposition: Proposition fmap_agrees_with_univalence {A B} (f : A -> B) `{IsEquiv _ _ f} : fmap F f = equiv_path _ _ (ap F (path_universe f)).
proof: Proof. refine (equiv_induction (fun A' e => fmap F e = equiv_path _ _ (ap F (path_universe e))) _ _ (Build_Equiv _ _ f _)). transitivity (idmap : F A -> F A). - apply fmap_idmap. - change (equiv_idmap A) with (equiv_path A A 1). rewrite (@eta_path_universe _ A A 1). exact 1. Defined.
imports: HoTT.Basics Types.Universe