From 55fd3b6cf53a7de64ecf3ccace71ccd4d2bead4d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 25 Feb 2025 21:55:02 +0100 Subject: [PATCH] Update Mathlib/CategoryTheory/ObjectProperty/Basic.lean Co-authored-by: Markus Himmel --- Mathlib/CategoryTheory/ObjectProperty/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean index 872b77087d048..297e576a31426 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean @@ -9,7 +9,7 @@ import Mathlib.CategoryTheory.Category.Basic # Properties of objects in a category Given a category `C`, we introduce an abbreviation `ObjectProperty C` -for predicated `C → Prop`. +for predicates `C → Prop`. ## TODO