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.