 A solution of the second kind, employing a different kind of higher-order type theory, is pursued in (Thomason 1980). In Thomason’s “intentional” logic, propositions are taken as a primitive category, instead of being analyzed as intensions of type sb. In turns out that a somewhat familiar higher-order type theory can be built on this basis, in which, roughly, the type of propositions plays a role analogous to the type of truth-values in extensional type theory. A property such as orator, for example, is a function of type ip (as opposed to ib), where p is the type of propositions: given an individual as input, orator will produce the proposition that that individual is an orator as output. Proper names, however, are not translated as terms of type i, for then cicero and tully would present the same input to orator, resulting in the same proposition as output: orator(cicero) = orator(tully). So there would be no believing Cicero is an orator without believing Tully is an orator. Instead, Thomason assigns proper names the type (ip)p, functions from properties to propositions. And merely the fact that Cicero and Tully are the same individual does not require us to say that cicero and tully must produce the same propositional output given the same property input. Instead, we can have cicero(orator) and tully(orator) distinct (see Muskens 2005 for further development of Thomason’s approach).