# Two introductory seminars to Homotopy Type Theory

25-26 September, 2023

Marco Benini (Università degli Studi dell’Insubria)

*1. Homotopy Type Theory: A Gentle Introduction*: Monday, September 25th, 16:00, Aula G (Ca’ Vignal 2).

**Abstract:**
Homotopy Type Theory (HoTT) is, syntactically, Martin-Löf Type Theory
(MLTT) plus the axiom called “univalence”.
Hence, it is, at the same time, an abstract functional programming
language, a logical system, and a synthetic way to describe homotopy
spaces.
The seminar introduces the type system, focusing on the homotopy
interpretation, univalence, and higher inductive types, i.e., the main
novelties of HoTT with respect to MLTT.
The seminar aims at providing the fundamental ideas of HoTT to
mathematicians and computer scientists willing to understand what is
HoTT without the burden of a formal, in-depth presentation.

*2. Homotopy Type Theory: Equality as Equality*: Tuesday, September 26th, 16:00, Aula I (Ca’ Vignal 2).

**Abstract:**
The seminar aims at discussing the logical properties of judgemental
and propositional equalities in HoTT. It shows the fundamental
reasoning techniques of HoTT, and a few small novel results.
Also, the material provides a critical view of the current stage of
development of the theory, showing to what extent a systematic
approach is needed.
This talk is intended for mathematicians and computer scientists
willing to see more of the formal and technical side of HoTT, and some
minimal
knowledge about type theories, algebraic topology, and constructive
mathematics is presumed.

The talks will be held both in presence and on Zoom. In order to get the Zoom link, please contact Giulio Fellin.