InsubriaSPACE - Thesis PhD Repository >
Insubria Thesis Repository >
01 - Tesi di dottorato >
Please use this identifier to cite or link to this item:
|Authors: ||Bonacina, Roberta|
|Internal Tutor: ||BENINI, MARCO|
|Title: ||Semantics for Homotopy Type Theory|
|Abstract: ||The main aim of my PhD thesis is to define a semantics for Homotopy type theory based on elementary categorical tools. This led us to extend the study of this system in other directions: we proved a Normalisation theorem, and defined a generic syntax. All those results are obtained for a subset of the whole Homotopy type theory, which we called 1-HoTT theories.
A 1-HoTT theory is composed by Martin-Löf type theory with generic inductive types, the axioms of function extensionality and univalence, truncation and generic 1-higher inductive types, which are a subset of the higher inductive types in which the higher constructor of a type T is limited to the type =T .
For those theories we obtained some proof theoretic results; the main one is a Normalisation theorem, following Girard's reducibility candidates technique.
The semantics is sound and complete, with the completeness result following from the existence of a canonical model, which is also classifying.
Our conjecture is that our proof theory and semantics can be extended to every single higher inductive type. The dissertation shows that a very large amount of higher inductive types can be analysed inside our framework: what prevents to extend the results is the lack of a systematic treatment of the syntax of the higher inductive types, which is still an open issue in Homotopy type theory.|
|Keywords: ||Homotopy type theory, semantics, proof theory, higher inductive types|
|Subject MIUR : ||MAT/01 LOGICA MATEMATICA|
|Issue Date: ||2019|
|Doctoral course: ||Informatica e matematica del calcolo|
|Academic cycle: ||32|
|Publisher: ||Università degli Studi dell'Insubria|
|Citation: ||Bonacina, R.Semantics for Homotopy Type Theory (Doctoral Thesis, Università degli Studi dell'Insubria, 2019).|
Files in This Item:
|PhD_Thesis_BonacinaRoberta_completa.pdf||testo completo tesi||966,36 kB||Adobe PDF||View/Open
This item is licensed under a Creative Commons License
Items in InsubriaSPACE are protected by copyright, with all rights reserved, unless otherwise indicated.