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.

### Preprints

*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)

### Talks

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