REFLECTIVE SEMANTICS OF CONSTRUCTIVE TYPE THEORY

It is well-known that the proof theory of many sufficiently powerful logics may be represented internally by Godelization. Here we show that for Constructive Type Theory, it is furthermore possible to define a semantics of the types in the type theory itself, and that this procedure results in new reasoning principles for type theory. Paradoxes are avoided by stratifying the definition in layers.