Johannes Schipp von Branitz: Primitive Recursive Dependent Type Theory
Time: Wed 2025-10-15 10.00 - 12.00
Location: Albano house 1, floor 3, Room U (Kovalevsky)
Participating: Johannes Schipp von Branitz (University of Nottingham)
Abstract
It is a theorem that in a type theory where elimination out of the natural numbers is restricted to a universe without function types, all small constructions are primitive recursive. This is compatible with larger universes containing Pi-types. We explore the proof, which uses synthetic Tait computability in a novel way, and hint at potential extensions to univalent type theories and judgemental small Gödel encodings, as well as the geometricity of function types.
Ulrik Torben Buchholtz, Johannes Schipp von Branitz, Primitive Recursive Dependent Type Theory, Proceedings of LICS '24, 2024, https://doi.org/10.1145/3661814.3662136