## 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.

## Publications

- Homotopy Type Theory: Univalent Foundations of Mathematics
- Collaborative Book 2013 link

- Eilenberg-MacLane Spaces in Homotopy Type Theory
- A Mechanization of the Blakers-Massey Theorem in Homotopy Type Theory
- A Type Theoretic Definition of Weak ω-Categories
- Goodwillie’s Calculus of Functors and Higher Topos Theory
- A Generalized Blakers-Massey Theorem
- Types are Internal oo-Groupoids

## Notes, Preprints and Work in Progress

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

## Videos

- Cohomology in Homotopy Type Theory ias
- The Calculus of Opetopes ias
- A Survey of Univalent Foundations youtube
- A Type Theoretic View of Goodwillie Calculus part one/part two
- Weak Structures from Strict Ones youtube
- Higher Algebra in Computer Science youtube

## Code

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

## My Thesis

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