Thursday 14 November 2019, 14:00, LSV library: Dependent type theories as "cellular" Lawvere theories (joint work with P. LeFanu Lumsdaine), Chaitanya Leena Subramaniam (PhD student, IRIF).

Certain kinds of algebraic structures (monoids, groups, rings, modules, etc.) admit a definition via an algebraic presentation of their theory using generators and equations, known commonly as a (multisorted) "Lawvere" theory. We extend this to dependent type theories, by viewing multisorted Lawvere theories as dependent type theories without any type (or sort) dependency. For an inverse category C, we show how suitable “C-sorted type theories” may be viewed (1) as monoids in a category of collections, and (2) as generalised Lawvere theories in the sense of Berger–Melliès–Weber. Moreover, essentially every dependent type theory arises in this way. Examples of algebraic structures that can be defined via dependent type theories (and that cannot be defined via multisorted Lawvere theories) are categories, groupoids, weak and strict \omega-categories, semi-simplicial sets, globular sets, opetopic sets etc. Inverse categories are known from homotopy theory, where they (or their opposite categories) provide a good notion of a category of "cells". Examples are the category of semi-simplices, the category of globes, the category of opetopes, etc.