Abstract
As a constructive foundation of mathematics, we expect type theory to be able to reason about its own syntax and semantics. However to precisely and conveniently represent type theory inside itself has turned out to be a longstanding open problem, with notable contributions by Dybjer, Danielsson and Chapman. A breakthrough was achieved by Altenkirch and Kaposi, who realised that quotient inductive-inductive types are well suited to represent the syntax of type theory up to definitional equality. Nowadays, the proof assistant Agda has support for quotient inductive-inductive types in its cubical mode, but unfortunately Altenkirch and Kaposi’s construction is not accepted as-is by cubical Agda, due to equality transports confusing the strict positivity checker. I will present an alternative construction of the syntax of type theory, which is accepted in cubical Agda, this time as an quotient inductive-inductive-recursive definition. The addition of a recursive component is inspired by Awodey’s notion of a natural model of type theory. This is joint work with Liang-Ting Chen and Tzu-Chun Tsai.
Talk Details
Speaker: Fredrik Nordvall Forsberg (University of Strathclyde, UK)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Wednesday 17 December 2025
Time: 11:50
Slides: Available
Key Topics
- Type theory reflection
- Quotient inductive-inductive types
- Cubical Agda
- Natural models
- Strict positivity
- Definitional equality
- Syntax representation
Collaborators
- Liang-Ting Chen
- Tzu-Chun Tsai
Related Work
- Altenkirch and Kaposi’s construction
- Awodey’s natural models
- Dybjer, Danielsson and Chapman’s contributions