From d285129507bacea9a80e98a887ea710ac00e7f2f Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 4 Jul 2023 05:50:36 +0000 Subject: [PATCH] chore: correct name in Category/ULift docs (#5701) Co-authored-by: Scott Morrison --- Mathlib/CategoryTheory/Category/ULift.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Category/ULift.lean b/Mathlib/CategoryTheory/Category/ULift.lean index 814124a683c26..229363b2691d3 100644 --- a/Mathlib/CategoryTheory/Category/ULift.lean +++ b/Mathlib/CategoryTheory/Category/ULift.lean @@ -19,8 +19,8 @@ import Mathlib.Data.ULift This file contains a very basic API for working with the categorical instance on `ULift C` where `C` is a type with a category instance. -1. `CategoryTheory.ULift.up` is the functorial version of the usual `ULift.up`. -2. `CategoryTheory.ULift.down` is the functorial version of the usual `ULift.down`. +1. `CategoryTheory.ULift.upFunctor` is the functorial version of the usual `ULift.up`. +2. `CategoryTheory.ULift.downFunctor` is the functorial version of the usual `ULift.down`. 3. `CategoryTheory.ULift.equivalence` is the categorical equivalence between `C` and `ULift C`.