Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes