My area of concentration is category theory, particularly categorical logic. My main current project is investigating the connections between higher-dimensional category theory and Martin-Löf intensional type theory.
- Weak ω-Categories from Intensional Type Theory, TLCA 2009, Brasília. Preprint of journal version: (pdf) (arXiv)
- Lawvere-Tierney Sheaves in Algebraic Set Theory, with Steve Awodey, Nicola Gambino and Michael A. Warren, Journal of Symbolic Logic, Vo. 74, Issue 3, pp.861–890 (2009). Preprint (Oct 2008): (pdf) (arXiv)
- A Small Observation on Co-categories, June 2008. “Every co-category in a coherent category is a co-equivalence relation.” Short note, four pages. (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.