Paige Randall North

About me

Paige Randall North

I am an assistant professor at Utrecht University, in the Department of Mathematics and the Department of Information and Computing Sciences. I study the mathematical foundations of type theory using category theory and homotopy theory: directed and enriched type theories, the semantics of dependent types, and the formalisation of mathematics in proof assistants. Before Utrecht I was a postdoc at the University of Pennsylvania and at Ohio State University, and I did my PhD at Cambridge with Martin Hyland.

Research

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: HoTTEST, Utrecht, CSCS, CT, CMCS, FICS, CHoCoLa, IRIF, CATMI, TYPES
  • 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, Shreya Arya, Greta Coraglia, Juli O’Connor, Ana Luiza Tenório

Directed type theory and directed homotopy theory

with Fernando Chu Rivera, Sanjeevi Krishnan

Category theory in univalent foundations

with Nima Rasekh, Niels van der Weide, Benedikt Ahrens, Dennis Hilhorst

  • Insights From Univalent Foundations: A Case Study Using Double Categories, published in CSL 2025. [doi] [arXiv]
  • Formalizing the algebraic small object argument in UniMath, published in ITP 2024. [doi]
  • Univalent Double Categories, published in CPP 2024. [doi] [arXiv]
  • Slides from related talks: Informal Formalization, ITP

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]
  • 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: Leeds, JMM

The univalence principle

with Benedikt Ahrens, Michael Shulman, Dimitris Tsementzis

Group

Funding

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

Current members

Past members

Teaching

Regular courses

  • Spring 2027: Type theory (Mastermath)
  • Spring 2026–7: Software testing and verification (Utrecht)
  • Spring 2024–6: Homotopy type theory (Mastermath)
  • Spring 2025: Seminar on logic and foundations of computing (Utrecht)
  • Fall 2024: Logica voor informatica (Utrecht)
  • Spring 2024: Advanced functional programming (Utrecht)
  • 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 2017–8: Linear algebra (OSU)
  • Spring 2018: Introduction to discrete mathematics (OSU)
  • Lent 2015: Number fields (Cambridge)
  • Michaelmas 2014: Galois theory (Cambridge)
  • Michaelmas 2012: Number theory (Cambridge)

Summer schools

Service