Skip to main content
Logo UniTrento
  • Italiano
MyUnitn
Cerca
 cerca nel Magazine
CALENDAR
Doctoral School in Mathematics
Seminar

Proof theoretical issues in Martin-Löf Type Theory and Homotopy Type Theory

Cycle 34th Oral Defence of the Phd Thesis
29 June 2022
Start time 
2:00 pm
PovoZero - Via Sommarive 14, Povo (Trento)

Vai alla mappa

Seminar Room "-1"
share
Facebook LinkedIn Twitter 
Versione stampabile
Organizer: 
Doctoral School in Mathematics
Target audience: 
University community
Attendance: 
Online – Registration required
Registration email: 
phd.maths@unitn.it
Contact person: 
Zunino Roberto - Marco Benini

Venue: The event will take in presence and online through the ZOOM platform. To get the access codes please contact the secretary office (phd.maths [at] unitn.it)
Time: 14:00

Marco Girardi - PhD in Mathematics, University of Trento

Abstract:
Homotopy Type Theory (HoTT) is a quite recent branch of research in mathematical logic, which provides interesting connections among various areas of mathematics. It was first introduced by Vladimir Voevodsky as a means to develop synthetic homotopy theory, and further advancements suggested that it can be used as a formal foundation to mathematics. Among its notable features, inductive and higher inductive types are of great interest, e.g. allowing for the study of geometric entities (such as spheres) in the setting of HoTT.
However, so far in most of the literature higher inductive types are treated in an ad-hoc way; there is no easy general schema stating what an higher inductive type is, thus hindering the study of the related proof theory. Moreover, although Martin-Löf Type Theory has been deeply and widely studied, many proof theoretic results about its specific variant used in HoTT are folklore, and the proofs are missing.
In this final talk, we provide an overview on some results we obtained, aiming to address these problems. In the first part of the talk, we will discuss a normalization theorem for the type theory underlying HoTT. In the second part of the talk we will propose a general syntax schema to encapsulate a relevant class of higher inductive types, potentially allowing for future study of the proof theory of HoTT enriched with such types.

Supervisor: Roberto Zunino
Co-Supervisor: Marco Benini

Download 
PDF icon Poster Oral Defence of the Phd Thesis Cycle 34th_Marco Girardi_June 29, 2022 (PDF | 438 KB)
EVENTSsee all