Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-28 02:49 17d62630

View on Github →

refactor(category_theory): minimize the amount of universe annotations in category_theory (#552)

Estimated changes

Modified category_theory/category.lean

modified theorem category_theory.category.assoc_symm

modified def category_theory.large_category

modified def category_theory.small_category

Modified category_theory/comma.lean

Modified category_theory/const.lean

Modified category_theory/discrete_category.lean

Modified category_theory/eq_to_hom.lean

Modified category_theory/equivalence.lean

modified structure category_theory.equivalence

modified def category_theory.functor.obj_preimage

Modified category_theory/examples/topological_spaces.lean

Modified category_theory/full_subcategory.lean

Modified category_theory/fully_faithful.lean

Modified category_theory/functor.lean

modified structure category_theory.functor

Modified category_theory/functor_category.lean

Modified category_theory/groupoid.lean

modified def category_theory.large_groupoid

modified def category_theory.small_groupoid

Modified category_theory/isomorphism.lean

modified structure category_theory.iso

Modified category_theory/limits/cones.lean

Modified category_theory/limits/functor_category.lean

modified def category_theory.limits.functor_category_is_colimit_cocone

Modified category_theory/limits/limits.lean

modified theorem category_theory.limits.colimit.map_post

modified theorem category_theory.limits.colimit.pre_map'

modified theorem category_theory.limits.colimit.pre_post

modified def category_theory.limits.is_colimit.of_faithful

modified def category_theory.limits.is_limit.of_faithful

modified theorem category_theory.limits.limit.map_post

modified theorem category_theory.limits.limit.map_pre'

modified theorem category_theory.limits.limit.pre_post

Modified category_theory/limits/preserves.lean

Modified category_theory/limits/types.lean

Modified category_theory/natural_isomorphism.lean

modified def category_theory.functor.ulift_down_up

modified def category_theory.functor.ulift_up_down

Modified category_theory/natural_transformation.lean

Modified category_theory/opposites.lean

Modified category_theory/pempty.lean

Modified category_theory/products.lean

Modified category_theory/punit.lean

Modified category_theory/types.lean

Modified category_theory/whiskering.lean

Modified category_theory/yoneda.lean