Hofmann–Streicher lifting of fibred categories

Abstract

In 1997, Hofmann and Streicher introduced an explicit construction to lift a Grothendieck universe 𝓤 from 𝐒𝐞𝐭 into the category of 𝐒𝐞𝐭-valued presheaves on a 𝓤-small category B. 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 𝓤’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 functor 𝐅𝐢𝐛(A) → 𝐅𝐢𝐛(B) given by postcomposition with a fibration A → B.