From 235b8992fd8a9c8f1615122499279ad227e72915 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 18 Jun 2019 18:06:30 -0400 Subject: [PATCH] fix(category_theory/types): rename lemma `ulift_functor.map` (#1133) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * fix(category_theory/types): avoid shadowing `ulift_functor.map` by a lemma Now we can use `ulift_functor.map` in the sense `functor.map ulift_functor`. * `ulift_functor.map_spec` → `ulift_functor_map` as suggested by @semorrison in https://github.com/leanprover-community/mathlib/pull/1133#pullrequestreview-250179914 --- src/category_theory/types.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean index 0eab43cb8a601..92e77748357bf 100644 --- a/src/category_theory/types.lean +++ b/src/category_theory/types.lean @@ -55,7 +55,7 @@ def ulift_functor : Type u ⥤ Type (max u v) := { obj := λ X, ulift.{v} X, map := λ X Y f, λ x : ulift.{v} X, ulift.up (f x.down) } -@[simp] lemma ulift_functor.map {X Y : Type u} (f : X ⟶ Y) (x : ulift.{v} X) : +@[simp] lemma ulift_functor_map {X Y : Type u} (f : X ⟶ Y) (x : ulift.{v} X) : ulift_functor.map f x = ulift.up (f x.down) := rfl instance ulift_functor_faithful : fully_faithful ulift_functor :=