Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-29 00:11 ecdb1383

View on Github →

feat(category/equiv_functor): type-level functoriality w.r.t. equiv (#2255)

  • feat(data/equiv/functor): bifunctor.map_equiv
  • start
  • sketch of equiv_functor
  • update
  • removing unimpressive inhabited example; easier later
  • omit
  • revert unnecessary change
  • fix doc-string
  • fix names
  • finish fix

Estimated changes