Title: Talk About Types

Abstract: Many metaphysical theories of identity, existence, and so on, are formulated using higher-order languages like the simply typed lambda calculus. But as I argue, for the purposes of metaphysical theorizing, a different language would be better: the calculus of constructions. Since this language—like many pure type systems—allows for quantification over types, it is preferable to the languages currently being used in the philosophical literature. For the purposes of metaphysical theorizing, in other words, the calculus of constructions is the better language.