About Me

I am a lecturer in computer science at the University of Birmingham. I grew up in Los Angeles, studied in Charlottesville, and presently live in Paris.

Research Interests

My main interests are higher category theory and homotopy theory, and applications of these subjects to computer science, particularly formal methods in software development and computer-assisted mathematics.

My formal training in mathematics was in homotopy theory, and I have worked extensively on the connection between this area of topology the theory of types, a discipline which goes by the name Homotopy Type Theory.

I’m also the author of a site all about the opetopes.

PhD Opportunities at Birmingham

We are inviting applications for PhD studentships in the Theory Group at the University of Birmingham to work on Homotopy Type Theory and related areas. The Theory Group at Birmingham has a broad interest in type theory, category theory, programming language theory and formalized mathematics, and both I and Martín Escardó are active researchers in the HoTT community.

For more information, send me at e.l.finster at bham.ac.uk.

Midlands Graduate School

I will be running a course on topos theory for the Midlands Graduate School this year.


  1. Homotopy Type Theory: Univalent Foundations of Mathematics
    • Collaborative Book 2013 link
  2. Eilenberg-MacLane Spaces in Homotopy Type Theory
  3. A Mechanization of the Blakers-Massey Theorem in Homotopy Type Theory
  4. A Type Theoretic Definition of Weak ω-Categories
  5. Goodwillie’s Calculus of Functors and Higher Topos Theory
  6. A Generalized Blakers-Massey Theorem
  7. Types are Internal oo-Groupoids

Notes, Preprints and Work in Progress

  1. A Type Theory for Strictly Unital oo-Categories arXiv
  2. A Type Theory for Strictly Associative oo-Categories arXiv
  3. Higher Sheaves and Left-Exact Localizations of oo-Topoi arXiv
  4. A Note on Left Exact Modalities in Type Theory pdf
  5. Synthetic Spectra via a Monadic and Comonadic Modality arXiv
  6. Globular Weak oo-Categories as Models of a Type Theory arXiv


  1. Cohomology in Homotopy Type Theory ias
  2. The Calculus of Opetopes ias
  3. A Survey of Univalent Foundations youtube
  4. A Type Theoretic View of Goodwillie Calculus part one/part two
  5. Weak Structures from Strict Ones youtube
  6. Higher Algebra in Computer Science youtube


  1. opetopic - A web-based opetope editor
  2. opetopic-types - A library for opetopic types and higher structures in Agda
  3. catt.io - An implementation of a type theory for weak ω-categories

My Thesis

  1. Stabilization of Homotopy Limits pdf
    • University of Virginia, 2010
    • Supervised by Dr. Gregory Arone