On Hofmann-Streicher universes

Abstract

We have another look at the construction by Hofmann and Streicher of a universe $(U,\mathsf{E}l)$ for the interpretation of Martin-Löf type theory in a presheaf category $\psh{\C}$. It turns out that $(U,\mathsf{E}l)$ can be described as the \emph{categorical nerve} of the classifier $\dot{\Set}^{\mathsf{op}} \to \op{\Set}$ for discrete fibrations in $\Cat$, where the nerve functor is right adjoint to the so-called ``Grothendieck construction'' taking a presheaf $P : \op{\C}\to\Set$ to its category of elements $\int_\C P$. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.

21 pages; added change of base and fibrations

Cited by in corpus (1)

• A denotationally-based program logic for higher-order store