I am an assistant professor at Utrecht University with a dual appointment in the Department of Mathematics and the Department of Information and Computing Sciences. I am also an Honorary Research Fellow in the School of Computer Science at the University of Birmingham and a Guest Researcher at the Delft University of Technology. Previously, I was a postdoc in the Departments of Mathematics and Electrical and Systems Engineering at the University of Pennsylvania, working with Rob Ghrist, and in the Mathematics Department at the Ohio State University, working with Sanjeevi Krishnan. Before that, I did my PhD in mathematics at the University of Cambridge under the supervision of Martin Hyland and my BS in mathematics at the University of Chicago.

In my research, I apply tools of topology and category theory to problems in computer science. I am most focused on the connections between functional programming/type theory and homotopy theory/higher category theory.

News

• June/July 2025: I’m looking forward to returning to the Oregon Programming Languages Summer School to give a lecture series on Category Theory.
• December 2024: I will be speaking at the HoTTEST seminar.
• October 2024: Our paper Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories won the best paper award at APLAS 2024!
• October 2024: Our paper Insights From Univalent Foundations: A Case Study Using Double Categories has been accepted at CSL 2025.

Group

We currently have no PhD or postdoc vacancies.

Current members

• Pim Otte, PhD candidate, 2024-
• Fernando Chu Rivera, PhD candidate, 2024-
• Léonard Guetta, postdoc, 2023-

Past members

• Alkis Ioannidis, master’s student, 2023-4
  • Currently a CS PhD student at Tallinn University of Technology
  • Thesis: The quasicategory of frames from a Type Theoretic Model Topos is an Elementary Infinity Topos
• Lukas Mulder, master’s student, 2023-4
  • Currently a CS PhD student at Radboud Universiteit
  • Thesis: The Functorial Nature of Enriched Data Types
• Éléonore Mangel, research intern, 2023-4
  • Currently a CS PhD student at Institut de recherche en informatique fondamental
• Dennis Hilhorst, master’s student, 2023
  • Currently a software engineer at High Voltage Engineering
  • Thesis: A Formalization of the Algebraic Small Object Argument in UniMath
• Erin McCloskey, master’s student, 2020-2
  • Thesis: Relative Weak Factorization Systems

Funding

• From 2021-4, we were funded by the AFOSR.

Research projects

Formalization of double categories in HoTT/UF

with Nima Rasekh, Niels van der Weide, Benedikt Ahrens

• Insights From Univalent Foundations: A Case Study Using Double Categories, to appear in CSL 2025. [arXiv]
• Univalent Double Categories, published in CPP 2024. [doi] [arXiv]
• Slides from related talks: Informal Formalization

Formalization of model category theory in HoTT/UF

with Dennis Hilhorst

• Formalizing the algebraic small object argument in UniMath, published in ITP 2024. [doi]
• Slides from related talks: ITP

Coalgebraic control of inductive datatypes

with Maximilien Péroux, Lukas Mulder

• Measuring data types (preprint, 2024). [arXiv]
• Coinductive control of inductive data types, published in CALCO 2023. [doi] [arXiv]
• Slides from related talks: TYPES, CATMI, CHoCoLa, IRIF, FICS, CMCS, CT, CSCS, Utrecht

Bicategorical type theory

with Benedikt Ahrens, Niels van der Weide

• Bicategorical type theory: semantics and syntax (2023), published in Mathematical Structures in Computer Science. [doi][arXiv]
• Semantics for two-dimensional type theory, published in LICS 2022. [doi]

Categorical dynamics

with Rob Ghrist, Miguel Lopez, Hans Riess

• Slides from related talks: Socio-Math, IRIF, Topos Institute, USD
• Videos from related talks: Topos Institute

Structure of the semantics of dependent types

with Benedikt Ahrens, Jacopo Emmenegger, Peter Lefanu Lumsdaine, Egbert Rijke

• Comparing semantic frameworks of dependently-sorted algebraic theories, published in APLAS 2024. [doi]
• Algebraic presentations of dependent type theories (preprint, 2022). [arXiv]
• B-systems and C-systems are equivalent (2023), published in the Journal of Symbolic Logic. [doi]

The univalence principle

with Benedikt Ahrens, Michael Shulman, Dimitris Tsementzis

• The univalence principle (2021), to appear in Memoirs of the AMS. [arXiv]
• A higher structure identity principle (2020), published in LICS 2020. [doi][arXiv]
• Slides from related talks: HoTT, HoTTEST, LICS, Penn Pizza, Algebra | Coalgebra, Penn Logic and Computation Part 1, Part 2, Part 3, MPI, ASL North American Annual Meeting, Utrecht Math, Cornell Topology Festival, (∞,n)-Categories and their applications, Utrecht Philosophy
• Videos from related talks: HoTTEST, LICS

Directed type theory

• Towards a directed homotopy type theory, published in MFPS 2019, [doi] [arXiv]
• Slides from related talks: AMS Spring 2018 Central Sectional Meeting, Birmingham, TYPES, HoTT/UF & HDRA, CT, CAS HoTT/UF, MFPS, HoTT-UF, Stockholm, Aarhus, Midwest HoTT, UPenn Applied Topology, Foundations and Applications of Univalent Mathematics, Florida State, Edinburgh, Minisymposium on Physically Grounded Semantics for Programming Hybrid Dynamical Systems, DutchCATS Workshop on AWFSs, GETCO 2022, Paris XIII, Nantes, GETCO 2023, MPI
• Videos from related talks: Spring School on Theoretical Computer Science (EPIT) – Homotopy Type Theory, Edinburgh, Minisymposium on Physically Grounded Semantics for Programming Hybrid Dynamical Systems, DutchCATS Workshop on AWFSs, GETCO 2022

PhD thesis: Type theoretic weak factorization systems

• Identity types and weak factorization systems in Cauchy complete categories, (2019), published in Mathematical Structures in Computer Science. [doi] [arXiv]
• Type theoretic weak factorization systems, PhD thesis, 2017, University of Cambridge [doi]
• Slides from related talks: JMM, Leeds

Other papers

• A Hurewicz model structure for directed topology (2021), joint with S. Krishnan, published in Theory and Applications of Categories. [tac] [arXiv]
• Univalent foundations and the equivalence principle (2019), joint with with B. Ahrens, published in Reflections on the Foundations of Mathematics, Synthese. [doi] [pdf]

Teaching

Regular courses

• Spring 2025: Seminar on Logic and Foundations of Computing (Utrecht)
• Spring 2025: Homotopy type theory (Mastermath)
• Winter 2024: Logica voor informatica (Utrecht)
• Spring 2024: Advanced functional programming (Utrecht)
• Spring 2024: Homotopy type theory (Mastermath)
• Spring 2023: Advanced Mathematics (University College Utrecht)
• Autumn 2021: Calculus III – linear algebra (Penn)
• Spring 2021: Calculus IV – applied partial differential equations (Penn)
• Spring 2020: Foundations of Higher Mathematics (OSU) (videos)
• Autumn 2018: Linear Algebra (OSU)
• Spring 2018: Introduction to Discrete Mathematics (OSU)
• Autumn 2017: Linear Algebra (OSU)
• Lent 2015: Number Fields (Cambridge)
• Michaelmas 2014: Galois Theory (Cambridge)
• Michaelmas 2012: Number Theory (Cambridge)

Summer schools

• Summer 2025: Oregon Programming Languages Summer School
• Summer 2024: UniMath School
• Fall 2023: Interactions of Proof Assistants and Mathematics (materials)
• Summer 2023: Oregon Programming Languages Summer School (materials)
• Summer 2022: Applied Category Theory Adjoint School
• Summer 2022: HoTTEST Summer School
• Summer 2022: UniMath School
• Spring 2021: Spring School on Theoretical Computer Science (EPIT) (video)
• Summer 2020: Applied Category Theory Adjoint School
• Summer 2019: Ross Program (course page)

Activities

Current

• Steering committee chair of TYPES
• Organizer of DutchCATS

Past

• PC Member of ACT 2022, 2023, 2024
• PC Member of STACS 2024
• PC Member of CPP 2024
• PC Member of SYCO 11, 12
• Organizer of WG6 2023 Meeting
• PC Member of MFPS 2023
• PC Member of HoTT/UF 2017, 2020, 2021, 2022, 2023
• Scientific organizer of HoTT/UF 2022
• Organizer of Midwest HoTT Seminar 2020 (cancelled)