Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-10 00:12 96d748eb

View on Github →

refactor(category_theory): rename functor.on_iso to functor.map_iso (#893)

  • feat(category_theory): functor.map_nat_iso
  • define functor.map_nat_iso, and relate to whiskering
  • rename functor.on_iso to functor.map_iso
  • add some missing lemmas about whiskering
  • some more missing whiskering lemmas, while we're at it
  • removing map_nat_iso

Estimated changes