# Seminar

Tuesday, October 29th, 2019, 16:10, Aula C.

Roberta Bonacina (Università degli Studi dell’Insubria)

*A simpler semantics for a large fragment of Homotopy Type Theory*

*Abstract:* The standard homotopical interpretation for homotopy type theory is
deep and useful, but it sounds odd that the full power of higher-order category
theory is needed to describe what is a piece “computable’’ mathematics. We show
that those complex categorical tools are not necessary, by proposing a novel
semantics, based on 1-category theory, for a big fragment of homotopy type
theory which contains the whole Martin-Löf type theory and some higher
inductive types. We also describe some proof theoretic results for this system;
in particular, we prove a normalisation theorem, extending Girard’s
reducibility candidates technique.