Peter LeFanu Lumsdaine: Comparing algebraic structures for semantics of type theory

In 1986, John Cartmell introduced *contextual categories* as an algebraic tool for working with models of type theories.  In the thirty years since, many variations on these have been introduced: categories with families, categories with attributes, type-categories, comprehension categories, c-systems, …   To add to the fun, some of these names have been given slightly different definitions by different authors.

They are all closely related, and some but not all are precisely equivalent.  I will survey the relationships between them, and their implications for modelling type theory.  This is in part a report on work in progress with Benedikt Ahrens and Vladimir Voevodsky, in which we formalise some of the comparisons in question.