Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.functor.ulift_down_up

Modification history

2020-06-26 07:16
src/category_theory/natural_isomorphism.lean
chore(category/*): linting (#3178) …
Deleted category_theory.functor.ulift_down_upView on Github →
2019-09-01 11:29
src/category_theory/natural_isomorphism.lean
chore(category_theory/notation): consistently use notation for functor.id (#1378) …
Modified category_theory.functor.ulift_down_upView on Github →
2018-12-28 02:49
category_theory/natural_isomorphism.lean
refactor(category_theory): minimize the amount of universe annotations in category_theory (#552)
Modified category_theory.functor.ulift_down_upView on Github →
2018-09-17 09:15
category_theory/natural_isomorphism.lean
feat(category_theory/*): some lemmas about universes
Added category_theory.functor.ulift_down_upView on Github →