English

On Hofmann-Streicher universes

Category Theory 2023-07-12 v3 Logic

Abstract

We have another look at the construction by Hofmann and Streicher of a universe (U,El)(U,{\mathsf{E}l}) for the interpretation of Martin-L\"of type theory in a presheaf category \psh\C\psh{\C}. It turns out that (U,El)(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\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 \CP\int_\C P. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.

Keywords

Cite

@article{arxiv.2205.10917,
  title  = {On Hofmann-Streicher universes},
  author = {Steve Awodey},
  journal= {arXiv preprint arXiv:2205.10917},
  year   = {2023}
}

Comments

21 pages; added change of base and fibrations

R2 v1 2026-06-24T11:24:56.545Z