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`.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
