Commit 2020-06-18 21:08 e060c93d

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.