Smallness of a property of objects

In this file, given P : ObjectProperty C, we define ObjectProperty.Small.{w} P as an abbreviation for Small.{w} (Subtype P).

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.Small {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) : Prop

A property of objects is small relative to a universe w if the corresponding subtype is.

Equations

• CategoryTheory.ObjectProperty.Small.{?u.22, ?u.21, ?u.20} P = Small.{?u.22, ?u.20} (Subtype P)

instance CategoryTheory.ObjectProperty.instSmallFullSubcategoryOfSmall {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.Small.{w, v, u} P] : Small.{w, u} P.FullSubcategory

theorem CategoryTheory.ObjectProperty.Small.of_le {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} [ObjectProperty.Small.{w, v, u} Q] (h : P ≤ Q) : ObjectProperty.Small.{w, v, u} P

instance CategoryTheory.ObjectProperty.instSmallOppositeOp {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [ObjectProperty.Small.{w, v, u} P] : ObjectProperty.Small.{w, v, u} P.op

instance CategoryTheory.ObjectProperty.instSmallUnopOfOpposite {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) [ObjectProperty.Small.{w, v, u} P] : ObjectProperty.Small.{w, v, u} P.unop

instance CategoryTheory.ObjectProperty.instSmallOfObjOfSmall {C : Type u} [Category.{v, u} C] {ι : Type u_1} (X : ι → C) [Small.{w, u_1} ι] : ObjectProperty.Small.{w, v, u} (ofObj X)

instance CategoryTheory.ObjectProperty.instSmallPair {C : Type u} [Category.{v, u} C] (X Y : C) : ObjectProperty.Small.{w, v, u} (pair X Y)