Menu:
My research lies broadly in category theory, logic, and constructive mathematics. Most of my recent work is within or related to the Homotopy Type Theory/Univalent Foundations programme: developing dependent type theory as a foundation for mathematics, drawing on ideas from homotopy theory and higher category theory.
I am also interested in quantum programming languages (I worked on the early stages of Quipper) and mathematical computing.
Publications & preprints
- The homotopy theory of type theories, with Chris Kapulkin, preprint (2016). pdf · arXiv
- The HoTT Library: A formalization of homotopy type theory in Coq, with Bauer, Gross, Shulman, Sozeau, and Spitters, submitted (2016). pdf · arXiv
- Constructive reflection principles for regular theories, with Henrik Forssell, submitted (2016). pdf · arXiv
- A mechanization of the Blakers–Massey connectivity theorem in homotopy type theory, with Kuen-Bang Hou, Eric Finster, and Dan Licata, Logic in Computer Science (LICS 2016), to appear.
- The local universes model: an overlooked coherence construction for dependent type theories, with Michael A. Warren, ACM Trans. Computational Logic 16, no. 3, pp.23.1–23.31 (2014). pdf · arXiv · journal
- Homotopy limits in type theory, with Jeremy Avigad and Chris Kapulkin, Mathematical Structures in Computer Science, 25(05), pp.1040–1070 (2014). pdf · arXiv · journal
- The simplicial model of Univalent Foundations, with Chris Kapulkin and Vladimir Voevodsky, preprint (2014). arXiv Shorter version (simplicial aspects only): Univalence in Simplicial Sets (2012). arXiv
- Homotopy Type Theory: Univalent Foundations of Mathematics, “The HoTT book”, collaborative book by the Univalent Foundations Group (2013). website
- Quipper: A Scalable Quantum Programming Language, with Alexander Green, Julien Ross, Peter Selinger, and Benoît Valiron, ACM SIGPLAN Notices 48(6):333-342 (2013). arXiv
- An introduction to Quantum Programming in Quipper, with Alexander Green, Julien Ross, Peter Selinger, and Benoît Valiron, for RC2013, Lecture Notes in Computer Science 7948:110-124, Springer (2013). arXiv
- Model Structures from Higher Inductive Types. Proves that any type theory with HIT’s (sepcifically, mapping cylinder types) admits most of the structure of a model category. Unpublished note (2011). pdf
- On the Bourbaki-Witt Principle in Toposes, with Andrej Bauer, Mathematical Proceedings of the Cambridge Philosophical Society, Vol. 155, No. 1 (2012). A miscellany of constructive proofs and countermodels, on the theme of the Bourbaki-Witt fixed-point theorem. pdf · arXiv · journal
- A Small Observation on Co-categories, Theory and Applications of Categories, Vol. 25, No. 9, pp.247–250 (2011). “Every co-category in a coherent category is a co-equivalence relation.” Short note, four pages (2008). pdf · arXiv · journal
- PhD thesis: Higher Categories from Type Theories, Carnegie Mellon University (2010). pdf
- Weak ω-Categories from Intensional Type Theory. Originally presented at TLCA 2009, Brasília; journal version in Logical Methods in Computer Science, Vol. 6, issue 23, paper 24 (2010). pdf · arXiv · journal · proceedings
- Lawvere-Tierney Sheaves in Algebraic Set Theory, with Steve Awodey, Nicola Gambino and Michael A. Warren, Journal of Symbolic Logic, Vol. 74, Issue 3, pp.861–890 (2009). pdf · arXiv
Talks
- Formalising the semantics of DTT, in DTT, DMV 2015, Hamburg, September 2015. Slides: pdf
- Higher Categories from Dependent Type Theories, CT2011, Vancouver, July 2011. An overview of part of my thesis work. (Taught me an important lesson in proofreading: start at the title slide, not the beginning of the text. Thanks to those who pointed this out after my talk, having decided that Higer was the squirrel at the end.) Slides: pdf
- Homotopy Type Theory: a very short introduction, OPLSS, Eugene, June 2011. Does what it says on the tin. Slides: pdf
- Higher Inductive Types: the circle and friends, axiomatically, FMCS 2011, Kananaskis, Alberta. An overview of homotopy type theory, and an introduction to higher inductive types, with pictures. Slides: pdf
- Conservativity principles: a homotopy-theoretic approach, Octoberfest 2010, Halifax. An elementary demonstration of how techniques from Homotopy Theory can be profitably applied in Type Theory. This was for a semi-special-session, so is a little lighter on DTT background than it might have been otherwise. Slides: pdf
- Topology and Algebra: an introduction to duality, CMU Grad Seminar, April 2009. Expository talk, for a general mathematical audience: presenting Gel’fand Duality, as a jumping-off point to illustrate the ideas of non-commutative geometry/topology and the language of category theory. Slides: pdf
-
Weak ω-categories and intensional type theory, October 2008. Handwritten notes from talks in CMU logic seminar. Not at first intended for public comsumption; quality improves as they go on. Talks 1–3 are entirely expository, 1 on type theory, 2 and 3 and the start of 4 on Tom Leinster's definition of weak ω-categories.
Talk 1 (Extremely scrappy notes.) A quick introduction to Intensional ML Type Theory.
Talk 2 Strict higher categories, and operads, in preparation for weak higher categories.
Talk 3 Globular operads, in preparation for weak higher categories.
Talk 4 Finally: weak higher categories! and a construction of the "fundamental weak ω-category" of a type.