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 for the interpretation of Martin-L\"of type theory in a presheaf category . It turns out that can be described as the \emph{categorical nerve} of the classifier \dot{\Set}^{\mathsf{op}} \to \op{\Set} for discrete fibrations in , 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 . 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