Constructive Set Theory from a Weak Tarski Universe

TL;DR

This thesis introduces a new weak Tarski universe concept in homotopy type theory, connecting constructive set theory with simplicial sets and their homotopy models, and extends the interpretation to homotopy type theory.

Contribution

It presents the first formal definition of a weak Tarski universe in type theory, motivated by categorical models like simplicial sets, and generalizes constructive set theory interpretation to homotopy type theory.

Findings

Defined a weak Tarski universe in type theory.

Showed the interpretation extends to homotopy type theory.

Connected constructive set theory with simplicial set models.

Abstract

The aim of this thesis is to give a concise introduction to homotopy type theory, to Aczel's constructive set theory and to simplicial sets and their homotopy theory in particular referring to their standard model structure, showing some of their interactions. The original part of this thesis consists in the final chapter where we introduce in the type theoretic context a definition of weak Tarski universe motivated by categorical models like the one given by simplicial sets. The weakening of this notion, although present in some imprecise form in mathematical folklore was not published before, at the best of our knowledge. Moreover, we show using the axiom of function extensionality that the type theoretic interpretation of constructive set theory generalises to homotopy type theory with a weak Tarski universe.