Commit 2020-06-25 07:40 266d3163

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.