An increasing amount of twenty-first century metaphysics is couched in explicitly hyperintensional terms. A prerequisite of hyperintensional metaphysics is that reality itself be hyperintensional: at the metaphysical level, propositions, properties, operators, and other elements of the type hierarchy, must be more fine-grained than functions from possible worlds to extensions. In this paper I develop, in the setting of type theory, a general framework for reasoning about the granularity of propositions and properties. The theory takes as primitive the notion of a (...) substitution on a proposition (property, etc.) and, among other things, uses this idea to elucidate a number of theoretically important distinctions. A class of structures are identified which can be used to model a wide range of positions about the granularity of reality; certain of these structures are seen to receive a natural treatment in the category of M-sets. (shrink)