mathlib

e060c93d - feat(category_theory/discrete): build equivalence from equiv (#3099)

feat(category_theory/discrete): build equivalence from equiv (#3099) * renames all the construction building functors/transformations out of discrete categories as `discrete.functor`, `discrete.nat_trans`, `discrete.nat_iso`, rather than names using `of_function`. * adds `def discrete.equivalence {I J : Type u₁} (e : I ≃ J) : discrete I ≌ discrete J`, * removes some redundant definitions * breaks some long lines, * and adds doc-strings. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>