Talks

1. Higher Inductive Types, talk at HoTT/UF 2016, Porto.
2. Programming with Higher Inductive Types, talk at EUTYPES meeting, Ljubljana.
3. The Three-HITs Theorem, talk at FPFM workshop, Nantes.
4. Higher Inductive Types in Programming, talk at Agda Implementors Meeting XXVII, Gothenburg.
5. Finite Sets in HoTT, talk at EUTYPES meeting in Nijmegen.
6. 1-Types vs Groupoids, talk at TYPES2018, Braga.
7. Bicategories in Homotopy Type Theory, talk at EUTYPES meeting in Aarhus.
8. Category Theory in UniMath, talk at UniMath School II 2019, Birmingham.
9. Bicategories in Univalent Foundations, talk at TYPES2019, Oslo.
10. Bicategories in Univalent Foundations, talk at FSCD2019, Dortmund.
11. The Construction of Set-Truncated Higher Inductive Types, talk at MFPS. London.
12. Constructing 1-truncated finitary higher inductive types as groupoid quotients, talk at HoTTEST2020 (video).
13. Constructing Higher Inductive Types as Groupoid Quotients, talk at LICS2020 (video, Q&A).
14. Semantics for two-dimensional type theory, talk at Syntax and Semantics of Type Theories, Stockholm.
15. Semantics for two-dimensional type theory, talk at TYPES2022, Nantes (video).
16. Category Theory in UniMath, talk at UniMath School III 2022, Cortona, Italy.
17. Enriched Categories in Univalent Foundations, talk at HoTT/UF 2023, Vienna, Austria.
18. Enriched Categories in Univalent Foundations, talk at TYPES 2023, Valencia, Spain (video).
19. The Formal Theory of Monads, Univalently, talk at FSCD 2023, Rome, Italy.
20. Displayed Monoidal Categories for the Semantics of Linear Logic, talk at CPP 2024, London, UK (video).
21. Displayed Monoidal Categories for the Semantics of Linear Logic, talk at SWS seminar.
22. Certifying higher-order polynomial interpretations, talk at rewriting/logic seminar.
23. The Internal Language of Univalent Categories, talk at the Programming Languages Seminar in Delft.
24. Formalizing Double Categories in UniMath, talk at the CoREACT Seminar.
25. The Interval Domain in Homotopy Type Theory, talk at Geuversfest.
26. The Internal Language of Univalent Categories, talk at TYPES2024, Copenhagen.
27. The Univalence Maxim and Univalent Double Categories, talk at TYPES2024, Copenhagen.
28. Univalent Enriched Categories and the Enriched Rezk Completion, talk at FSCD2024, Tallinn.
29. The internal languages of univalent categories, talk at HoTTEST2024 (video).
30. The internal languages of univalent categories, talk at CT seminar in Utrecht.
31. How to give a talk, Logic Mentoring Workshop 2025, Amsterdam.
32. Insights From Univalent Foundations: A Case Study Using Double Categories, talk at CSL2025, Amsterdam.
33. The Univalence Maxim and Univalent Double Categories, talk at CT seminar in Utrecht.
34. Impredicative Encodings of Inductive and Coinductive Types, talk at DutchCATs.
35. Impredicative Encodings of Inductive and Coinductive Types, talk at TYPES2025, Glasgow (video).
36. The internal languages of univalent categories, talk at LICS2025, Singapore.
37. Impredicative Encodings of Inductive and Coinductive Types, talk at FSCD2025, Birmingham.
38. The UniMath Rocq Library, talk at EuroProofNet Workshop on Proof Libraries, Orsay.
39. Inductive Types, lecture for the course Logical Verification, Amsterdam.
40. Impredicativity in Linear Dependent Type Theory, talk at LIX seminar, Paris.
41. A realisability model of linear dependent type theory, talk at Formath Seminar, Paris.
42. A General Construction of Strict Models in HoTT, talk at TYPES2026, Gothenburg.
43. A Realisability Model for Impredicative Linear Dependent Type Theory, talk at CT seminar in Utrecht.