# Commit 2020-06-18 21:08 e060c93d

View on Github →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.