Propositional functions and families of types (Q908912): Difference between revisions

When specifying the task of a computer program, it is often natural to use recursion on a data type. In Martin-Löf's type theory, a universe must be used when defining a propositional function by recursion. There are disadvantages to using a universe and the author introduces an extension of type theory in which the use of a universe can often be avoided. The extension put forward here is that the elimination rules for the various set forming operations should be generalized so that the conclusion of such a rule is not restricted to be of the form ``c is an element in the set C'', but will be of the form ``c is an object of type \(\gamma\) ''. This means that it will be possible to define type valued functions by recursion on a set and, in particular, to define propositional functions by recursion without using a universe. The paper is arranged as following: First the author briefly describes how sets in Martin-Löf's type theory can be viewed as specifications, and then why a universe sometimes must be used when expressing propositions. A presentation of the separation of sets and types is given before the extension is formulated. Finally, the author gives an interpretation of the extended type theory in type theory with one universe.