Università degli Studi dell'Insubria Insubria Space

InsubriaSPACE - Thesis PhD Repository >
Insubria Thesis Repository >
01 - Tesi di dottorato >

Please use this identifier to cite or link to this item: http://hdl.handle.net/10277/885

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
Issue Date: 2019
Language: eng
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:

File Description SizeFormatVisibility
PhD_Thesis_BonacinaRoberta_completa.pdftesto completo tesi966,36 kBAdobe PDFView/Open

This item is licensed under a Creative Commons License
Creative Commons

Items in InsubriaSPACE are protected by copyright, with all rights reserved, unless otherwise indicated.

Share this record




Stumble it!



  ICT Support, development & maintenance are provided by the AePIC team @ CILEA. Powered on DSpace Software.  Feedback