chore(category/equivalence): cleanup (#3164)
Previously some "shorthands" like
```
@[simp] def unit (e : C ≌ D) : 𝟭 C ⟶ e.functor ⋙ e.inverse := e.unit_iso.hom
```
had been added in `equivalence.lean`.
These were a bit annoying, as even though they were marked as `simp` sometimes the syntactic difference between `e.unit` and `e.unit_iso.hom` would get in the way of tactics working.
This PR turns these into abbreviations.
This comes at a slight cost: apparently expressions like `{ X := X }.Y` won't reduce when `.Y` is an abbreviation for `.X.Z`, so we add some `@[simp]` lemmas back in to achieve this.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
