Talks

• Primitive Recursive Dependent Type Theory at LICS 2024, 24-07-09, [slides]
• Primitive Recursive (Homotopy) Type Theory at HoTT/UF, 2024-04-02, [slides] [arxiv]
• Displayed Univalent Reflexive Graphs in Cubical Type Theory, at Agda Implementors’ Meeting XXXIII, 2020-10-05