Simone Tonelli: Investigations into a model of type theory based on the concept of basic pair

The principal aim of this thesis is to explain a possible model of Per Martin-Löf's type theory based on the concept of Giovanni Sambin’s basic pair. This means to extend the concept of “set” in the easiest and most natural way: transforming it in a couple of sets and an arbitrary relations set between them, i.e. a basic pair. This reasoning will be applied to all the judgment forms and will give us an interpretation of Martin-Löf's type theory. Our purpose will be to find a model which satisfies this interpretation, and we will look for it following two different approaches. The first one is meant to remain inside the standard type theory constructing an internal model; the second one, arisen from some impasses reached in the development of the first attempt, is aimed at adding new type constructors at the standard theory, extending it and allowing us to create an external model. These new types, that we have denoted here with a star, have to be seen like an arbitrary relations set between two set of the same type without star. This extended theory will give us all the results needed in a natural way, and might be useful in different interpretations for further research.