CLASP
The Centre for Linguistic Theory and Studies in Probability

Universes in MTT-semantics

In type theory, a universe is a type of types. Universes play important roles when modern type theories (MTTs) are employed as foundational languages for linguistic semantics. In this talk, I’ll report work on two kinds of universes in the study of MTT-semantics. The first kind may be called linguistic universes which include CN, the universe of common nouns, and LType, the universe employed in the study of coordination. It is shown how they are introduced and used in semantic studies and, in particular, their usefulness is reflected in how they facilitate \Pi-polymorphism in various semantic formalisations.

I shall then study logical universes. In order to formulate MTT-semantics adequately, proof irrelevance needs to be enforced in the underlying type theory. For example, in type theory UTT, this is possible because there is the universe Prop of all logical propositions. However, in Martin-Löf’s type theory, this is impossible because types and propositions are identified in MLTT. I propose that the extension of MLTT with h-logic, as developed in the HoTT project, can be used adequately as a foundational language for MTT-semantics, since there is a built-in notion of proof irrelevance in h-logic.