2014/11/20 by Cesare Gallozzi, Gallozzi, Cesare
Computer Science · Mathematics · #Advanced Topology and Set Theory #Algebraic Topology (math.AT) #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1411.5591
openalex publication_date 2014/11/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.