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
Subject MIUR : MAT/01 LOGICA MATEMATICA
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
Del.icio.us

Citeulike

Connotea

Facebook

Stumble it!

reddit


 

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