Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:42 d074b51b

View on Github →

refactor(category_theory/concrete_category): move bundled to own file

Estimated changes

Modified src/category_theory/category.lean

deleted structure category_theory.bundled

deleted theorem category_theory.bundled_hom_coe

deleted structure category_theory.concrete_category

deleted theorem category_theory.concrete_category_comp

deleted theorem category_theory.concrete_category_id

deleted def category_theory.mk_ob

Created src/category_theory/concrete_category.lean

added theorem category_theory.bundled.bundled_hom_coe

added theorem category_theory.bundled.concrete_category_comp

added theorem category_theory.bundled.concrete_category_id

added def category_theory.bundled.map

added structure category_theory.bundled

added structure category_theory.concrete_category

added def category_theory.concrete_functor

added def category_theory.forget

added def category_theory.mk_ob

Modified src/category_theory/examples/measurable_space.lean

Modified src/category_theory/examples/monoids.lean

Modified src/category_theory/examples/rings.lean

Modified src/category_theory/examples/topological_spaces.lean

Modified src/category_theory/functor.lean

deleted def category_theory.bundled.map

deleted def category_theory.concrete_functor

Modified src/category_theory/types.lean

deleted def category_theory.forget