Paige Randall North

About me

Paige Randall North

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

Group

Funding

  • 2026–2031: NWO Vidi project Enriched type theory.
  • 2021–2024: AFOSR project HoTTDiTop.

Current members

Past members

Research projects

Coalgebraic control of inductive datatypes

with Maximilien Péroux, Lukas Mulder

  • Measuring data types (2026), to appear in the postproceedings of CATMI 2023 (Category Theory at Work in Computational Mathematics and Theoretical Informatics). [arXiv]
  • Functoriality of Enriched Data Types, published in MFPS 2025. [doi] [arXiv]
  • Coinductive control of inductive data types, published in CALCO 2023. [doi] [arXiv]
  • Slides from related talks: TYPES, CATMI, IRIF, CHoCoLa, FICS, CMCS, CT, CSCS, Utrecht, HoTTEST
  • Videos from related talks: HoTTEST

Categorical structures as type theories

with Benedikt Ahrens, Niyousha Najmaei, Niels van der Weide

  • From Semantics to Syntax: A Type Theory for Comprehension Categories, published in POPL 2026. [doi] [arXiv]
  • 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

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, published in CSL 2025. [doi] [arXiv]
  • Univalent Double Categories, published in CPP 2024. [doi] [arXiv]
  • Slides from related talks: Informal Formalization

Structure of the semantics of dependent types

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

  • Algebraic presentations of dependent type theories (2025), published in Logical Methods in Computer Science. [doi] [arXiv]
  • Comparing semantic frameworks for dependently-sorted algebraic theories, published in APLAS 2024. (Best paper award) [doi] [arXiv]
  • B-systems and C-systems are equivalent (2023), published in Journal of Symbolic Logic. [doi]

The univalence principle

with Benedikt Ahrens, Michael Shulman, Dimitris Tsementzis

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

Directed type theory

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. [arXiv] [tac]
  • Univalent foundations and the equivalence principle (2019), joint with B. Ahrens, published in Reflections on the Foundations of Mathematics, Synthese. [doi] [pdf]

Teaching

Regular courses

  • Spring 2027: Type theory (Mastermath) (planned)
  • Spring 2027: Software testing and verification (Utrecht) (planned)
  • Spring 2026: Software testing and verification (Utrecht)
  • Spring 2026: Homotopy type theory (Mastermath)
  • Spring 2025: Seminar on logic and foundations of computing (Utrecht)
  • Spring 2025: Homotopy type theory (Mastermath)
  • Fall 2024: Logica voor informatica (Utrecht)
  • Spring 2024: Advanced functional programming (Utrecht)
  • Spring 2024: Homotopy type theory (Mastermath)
  • Spring 2023: Softwareproject informatica (Utrecht)
  • Spring 2023: Advanced mathematics (University College Utrecht)
  • Fall 2021: Calculus III – linear algebra (Penn)
  • Spring 2021: Calculus IV – applied partial differential equations (Penn)
  • Spring 2020: Foundations of higher mathematics (OSU) (videos)
  • Fall 2018: Linear algebra (OSU)
  • Spring 2018: Introduction to discrete mathematics (OSU)
  • Fall 2017: Linear algebra (OSU)
  • Lent 2015: Number fields (Cambridge)
  • Michaelmas 2014: Galois theory (Cambridge)
  • Michaelmas 2012: Number theory (Cambridge)

Summer schools

Activities