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.