In Lifting Grothendieck universes Hofmann and Streicher construct a universe in the category of presheaves over a small category given a Grothendieck universe in $\mathbf{Set}$.

Suppose now I have two small categories $\mathbb{C}$ and $\mathbb{D}$, a functor $\mathfrak{f} : \mathbf{Set}^{\mathbb{C}} \to \mathbf{Set}^{\mathbb{D}}$ and a universe $u : E \to V$ in $\mathbf{Set}^{\mathbb{C}}$ that is closed under the formation of dependent products, sums and W-types.

What conditions on $\mathfrak{f}$ are sufficient to ensure that $\mathfrak{f}(u) : \mathfrak{f}(E) \to \mathfrak{f}(V)$ is a universe in $\mathbf{Set}^{\mathbb{D}}$ that is closed under the same constructions?

I am mostly interested in the case where $\mathbb{C}$ and $\mathbb{D}$ are posets, if this makes anything easier.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.