Menu:
My research is in category theory, particularly categorical logic, and constructive mathematics. My main current project is investigating the connections between higher-dimensional category theory and Martin-Löf intensional type theory.
Publications & preprints
- 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. Prepublication version, Dec 2011: pdf
- On the Bourbaki-Witt Principle in Toposes, with Andrej Bauer. A miscellany of constructive proofs and countermodels, on the theme of the Bourbaki-Witt fixed-point theorem. Submitted, Jan 2012. pdf · arXiv
- 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. pdf · LMCS · arXiv · 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). Preprint (Oct 2008): pdf · arXiv
- 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, June 2008. pdf · TAC · arXiv
Talks
- 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.