Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-11 09:58 c68f23df

View on Github →

chore(category_theory/types): add documentation, remove bad simp lemmas and instances, add notation for functions as morphisms (#2383)

Add module doc and doc strings for src/category_theory/types.lean.
Remove some bad simp lemmas and instances in that file and src/category_theory/category/default.lean.
Add a notation ↾f which enables Lean to see a function f : α → β as a morphism α ⟶ β in the category of types.

Estimated changes

Modified src/algebra/category/Group/adjunctions.lean

Modified src/category_theory/category/default.lean

added theorem category_theory.epi_comp

added theorem category_theory.mono_comp

Modified src/category_theory/limits/shapes/images.lean

Modified src/category_theory/types.lean

added def category_theory.as_hom

deleted theorem category_theory.functor_to_types.map_comp

added theorem category_theory.functor_to_types.map_comp_apply

deleted theorem category_theory.functor_to_types.map_id

added theorem category_theory.functor_to_types.map_id_apply

modified theorem category_theory.types_comp

added theorem category_theory.types_comp_apply

modified theorem category_theory.types_hom

modified theorem category_theory.types_id

added theorem category_theory.types_id_apply

Modified src/category_theory/yoneda.lean

Modified src/topology/metric_space/lipschitz.lean