Update Mathlib/CategoryTheory/ObjectProperty/Basic.lean

Co-authored-by: Markus Himmel <[email protected]>
leanprover-community · Feb 25, 2025 · 55fd3b6 · 55fd3b6
1 parent b147e9c
commit 55fd3b6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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