Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-08 01:59 0a490302

View on Github →

fix(category_theory): turn has_limits classes into structures (#896)

fix(category_theory): turn has_limits classes into structures
fixing all the other pi-type typclasses
oops

Estimated changes

Modified src/category_theory/adjunction.lean

Modified src/category_theory/instances/topological_spaces.lean

Modified src/category_theory/limits/functor_category.lean

Modified src/category_theory/limits/limits.lean

deleted def category_theory.limits.has_colimits

deleted def category_theory.limits.has_colimits_of_shape

deleted def category_theory.limits.has_limits

deleted def category_theory.limits.has_limits_of_shape

Modified src/category_theory/limits/over.lean

Modified src/category_theory/limits/preserves.lean

deleted def category_theory.limits.preserves_colimits

deleted def category_theory.limits.preserves_colimits_of_shape

deleted def category_theory.limits.preserves_limits

deleted def category_theory.limits.preserves_limits_of_shape

deleted def category_theory.limits.reflects_colimits

deleted def category_theory.limits.reflects_colimits_of_shape

deleted def category_theory.limits.reflects_limits

deleted def category_theory.limits.reflects_limits_of_shape

Modified src/category_theory/limits/types.lean