Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-17 09:15 cf260cab

View on Github →

feat(category_theory/*): some lemmas about universes

Estimated changes

Modified category_theory/category.lean

Modified category_theory/functor.lean

added def category_theory.functor.ulift_down

added def category_theory.functor.ulift_up

Modified category_theory/natural_isomorphism.lean

added def category_theory.functor.ulift_down_up

added def category_theory.functor.ulift_up_down