Théo Winterhalter, Formalisation and Meta-Theory of Type Theory, Nantes (2020) [pdf, github]
Talks
Théo Winterhalter, A conservative and constructive translation from extensional type theory to weak type theory, Strength of Weak Type Theory, DutchCATS, 11 May 2023. (slides)