Amélia Liao: Displayed Categories as Building Blocks

Displayed categories are a type-theoretic abstraction for conveniently working with the data of what is, essentially, a functor. Consequently, displayed categories are widely applicable, and can be used to formalise, in a reusable way, many “folklore results” about building complex categories in terms of simpler ones.

Many categories of “sets with structures” can be phrased, using the language of displayed categories, literally as structures over the category of sets, rather than defining an ad-hoc “forgetful functor” afterwards. Furthermore, properties of the induced forgetful functor arise naturally as fibrational properties of the displayed category.