Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-24 11:03 ed579163

View on Github →

feat(category_theory): functions to convert is_lawful_functor and is_… (#1258)

  • feat(category_theory): functions to convert is_lawful_functor and is_lawful_monad to their corresponding category_theory concepts
  • Fix typo
  • feat(category): add mjoin_map_pure, mjoin_pure to the simpset (and use <$> notation)

Estimated changes

added theorem mjoin_map_map
added theorem mjoin_map_mjoin
added theorem mjoin_map_pure
added theorem mjoin_pure