universe

(in category theory/type theory/computer science)

of all homotopy types

type of types, object classifier,

codomain fibration

of homotopy n-types

of 0-truncated types/h-sets

of (-1)-truncated types/h-propositions