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