On Hofmann–Streicher universes

We take another look at the construction by Hofmann and Streicher of a universe (U,El) for the interpretation of Martin-Löf type theory in a presheaf category [Cᵒᵖ,Set] . It turns out that (U,El) can be described as the nerve of the classifier Setᵒᵖ →Setᵒᵖ for discrete fibrations in Cat , where the nerve functor is right adjoint to the so-called “Grothendieck construction” taking a presheaf P :Cᵒᵖ→Set to its category of elements ∫ C P . We also consider change of base for such universes, as well as universes of structured families, such as fibrations.