Talks

• Propositional Geometric Type Theory HoTT/UF 2025 [slides] [abstract]
• An Informal Introduction to HoTT via Synthetic Homotopy Theory EPFL 2025 [slides]
• Primitive Recursive Dependent Type Theory at LICS 2024 [slides]
• Primitive Recursive (Homotopy) Type Theory at HoTT/UF 2024 [slides] [arxiv]
• Displayed Univalent Reflexive Graphs in Cubical Type Theory, at Agda Implementors’ Meeting XXXIII 2020