English

Hofmann-Streicher lifting of fibred categories

Category Theory 2026-04-29 v5 Logic in Computer Science

Abstract

In 1997, Hofmann and Streicher introduced an explicit construction to lift a Grothendieck universe from the category of sets into the category of set-valued presheaves on a small category. More recently, Awodey presented an elegant functorial analysis of this construction in terms of the categorical nerve, the right adjoint to the functor that takes a presheaf to its category of elements; in particular, the categorical nerve's functorial action on the universal small discrete fibration gives the generic family of the universe's Hofmann-Streicher lifting. Inspired by Awodey's analysis, we define a relative version of Hofmann-Streicher lifting in terms of the right pseudo-adjoint to the 2-functor given by postcomposition with a fibration. Finally, we construct a new 2-bifibration of fibrations in which the opcartesian and cartesian lifts arise from these pseudo-adjunctions.

Keywords

Cite

@article{arxiv.2504.09520,
  title  = {Hofmann-Streicher lifting of fibred categories},
  author = {Andrew Slattery and Jonathan Sterling},
  journal= {arXiv preprint arXiv:2504.09520},
  year   = {2026}
}

Comments

Final revision of extended version, to appear in Logical Methods in Computer Science. Added ORCID links and updated lmcs.cls