Commit 2021-02-28 20:56 18804b20
View on Github →chore(category/equivalence): remove functor.fun_inv_id (#6450)
F.fun_inv_id was just a confusing alternative way to write F.as_equivalence.unit_iso.symm, and meant that many lemmas couldn't fire.
Deletes the definitions functor.fun_inv_id and functor.inv_hom_id, and the lemmas is_equivalence.functor_unit_comp and is_equivalence.inv_fun_id_inv_comp.