Peter LeFanu Lumsdaine: The 2-category of comprehension categories

Abstract: Comprehension categories, introduced by Bart Jacobs, are a generalisation of categories with attributes, contextual categories, and so on — so, yet another categorical structure for the semantics of type theory.

Their unique selling point is that they are flexible and general enough to capture both the strict substitutivity properties enjoyed by syntax, and the weaker pullback-stability properties typically found in models.  They thus form a good setting for defining and comparing such stability properties.

I will discuss how a 2-categorical viewpoint can be fruitful in the study of comprehension categories.