Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-29 18:36 4ac87ab5

View on Github →

chore(category_theory): use the new @[ext] attribute on structures (#1663)

chore(category_theory): use the new @[ext] attribute on structures
fixes
unnecessary repeated exts

Estimated changes

Modified src/algebraic_geometry/presheafed_space.lean

Modified src/category_theory/adjunction/basic.lean

Modified src/category_theory/adjunction/fully_faithful.lean

Modified src/category_theory/comma.lean

deleted theorem category_theory.comma_morphism.ext

modified structure category_theory.comma_morphism

Modified src/category_theory/limits/cones.lean

deleted theorem category_theory.limits.cocone_morphism.ext

modified structure category_theory.limits.cocone_morphism

deleted theorem category_theory.limits.cone_morphism.ext

modified structure category_theory.limits.cone_morphism

Modified src/category_theory/limits/functor_category.lean

Modified src/category_theory/monad/algebra.lean

deleted theorem category_theory.monad.algebra.hom.ext

modified structure category_theory.monad.algebra.hom

Modified src/category_theory/natural_transformation.lean

deleted theorem category_theory.nat_trans.ext

modified structure category_theory.nat_trans

Modified src/category_theory/whiskering.lean

Modified src/category_theory/yoneda.lean