Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-11 19:10 953c612e

View on Github →

fix(category_theory): simplifying universes (#1122)

Estimated changes

Modified src/category_theory/adjunction/basic.lean

Modified src/category_theory/adjunction/limits.lean

Modified src/category_theory/category.lean

modified theorem category_theory.category.assoc_symm

modified def category_theory.large_category

modified def category_theory.small_category

Modified src/category_theory/comma.lean

modified structure category_theory.comma

Modified src/category_theory/concrete_category.lean

modified structure category_theory.bundled

modified def category_theory.forget

modified def category_theory.mk_ob

Modified src/category_theory/const.lean

Modified src/category_theory/core.lean

modified def category_theory.core

Modified src/category_theory/discrete_category.lean

Modified src/category_theory/epi_mono.lean

Modified src/category_theory/eq_to_hom.lean

Modified src/category_theory/equivalence.lean

modified structure category_theory.equivalence

Modified src/category_theory/full_subcategory.lean

modified def category_theory.induced_category

Modified src/category_theory/fully_faithful.lean

Modified src/category_theory/functor.lean

modified structure category_theory.functor

Modified src/category_theory/functor_category.lean

Modified src/category_theory/groupoid.lean

modified def category_theory.large_groupoid

modified def category_theory.small_groupoid

Modified src/category_theory/isomorphism.lean

modified structure category_theory.iso

Modified src/category_theory/limits/cones.lean

Modified src/category_theory/limits/functor_category.lean

Modified src/category_theory/limits/limits.lean

modified theorem category_theory.limits.colimit.map_post

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.pre_post

Modified src/category_theory/limits/opposites.lean

Modified src/category_theory/limits/over.lean

Modified src/category_theory/limits/preserves.lean

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

modified def category_theory.limits.pair_function

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

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

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

Modified src/category_theory/monoidal/category.lean

modified def category_theory.tensor_iso

Modified src/category_theory/monoidal/category_aux.lean

Modified src/category_theory/monoidal/functor.lean

Modified src/category_theory/natural_isomorphism.lean

modified def category_theory.iso.app

Modified src/category_theory/natural_transformation.lean

modified structure category_theory.nat_trans

Modified src/category_theory/opposites.lean

Modified src/category_theory/pempty.lean

Modified src/category_theory/products/default.lean

Modified src/category_theory/punit.lean

Modified src/category_theory/sparse.lean

Modified src/category_theory/types.lean

Modified src/category_theory/whiskering.lean

Modified src/category_theory/yoneda.lean