Abstract
In the early 2010s, when homotopy type theory was young, Martín and I had many discussions on Hedberg’s Theorem and propositional truncation. These discussions shaped my PhD. At the workshop, I will talk about results that we found together, how they inspired me to study Shulman’s Reedy fibrant inverse diagrams and Makkai’s FOLDS, and eventually convinced me of the need for a second type-theoretic layer on top of homotopy type theory.
Talk Details
Speaker: Nicolai Kraus (University of Nottingham, UK)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Thursday 18 December 2025
Time: 16:00
Key Topics
- Hedberg’s theorem
- Propositional truncation
- Homotopy type theory
- Truncation elimination
- Two-level type theory
- Reedy fibrant inverse diagrams
- FOLDS (First-Order Logic with Dependent Sorts)
Personal Connection
This talk reflects the deep collaborative relationship between Kraus and Escardó during the early development of homotopy type theory, highlighting how their discussions on fundamental concepts like Hedberg’s theorem and propositional truncation shaped Kraus’s doctoral research and subsequent work on two-level type theory.
Related Work
- Shulman’s Reedy fibrant inverse diagrams
- Makkai’s FOLDS
- Two-level type theory development