James Cranch, How (not) to define categories in HoTT

On 10 Nov 2014, at Homotopy Type Theory Workshop (7-10 Nov 2014, Mathematical Institute, University of Oxford) Abstract: Work of Ahrens, Kapulkin and Shulman gives a convincing definition of 1-categories inside homotopy type theory. It's certainly natural to ask for much more: a full theory of (infty,1)-categories. I'll describe a fragment of such a theory, where our categories are those which differ in a finitary way from the (infty,1)-category of types. This fragment contains some handy examples (including all 1-categories), but also fails to capture some pretty crucial examples (such as most (infty,1)-categories of structured types). I'll discuss the strengths and limitations, and hopefully describe some further aspirations