 We admit sorts of object indexed by the natural numbers (this is purely a typographical convenience; no actual reference to natural numbers is involved). Type 0 is inhabited by “individuals” with no specified structure. Type 1 is inhabited by sets of type 0 objects, and in general type \(n + 1\) is inhabited by sets of type \(n\) objects.