8
$\begingroup$

Let $\mathcal C$ be a small category, and consider the topos $Psh(\mathcal C)$ of $Set$-valued presheaves on $\mathcal C$. For simplicity, assume that there exists a proper class of inaccessible cardinals. If $\kappa$ is an inaccessible exceeding the size of $\mathcal C$, a universe of size $\kappa$ in $Psh(\mathcal C)$ is supposed to roughly be an object $U_\kappa \in Psh(\mathcal C)$ such that morphisms $X \to U_\kappa$ correspond to maps $Y \to X$ with $\kappa$-small fibers.

There is some subtlety here having to do with ensuring that the the universe is a (strict!) functor $\mathcal C^{op} \to Set$. But Hofmann and Streicher observed (in an unpublished note (that's a direct link to a 4-page pdf)) that there is a very natural way to construct such a universe. Namely, let $U_\kappa(I) = Psh_\kappa(\mathcal C/I)$, where $Psh_\kappa = Fun( (-)^{op}, Set_\kappa)$ is the category of presheaves with values in $V_\kappa$, and $\mathcal C/I$ is the slice category.

But for some reason, even after Hofmann and Streicher's note, some authors have continued to use universe constructions which are more elaborate and less canonical. See, for example Kapulkin and Lumsdaine, or Cisinski, involving well-orderings, or choices of actions of simplicial operators. My question is: why?

Question 1: Is there any reason to prefer more elaborate universe constructions to Hofmann-Streicher universes?

Question 2: If I'm reading something like Cisinski's book above, is it safe for me to replace all occurrences of his more elaborate universes with Hofmann-Streicher universes?

To be clear -- after constructing a Hofmann-Streicher universe, you generally want to cut down to some subuniverse to study things like left/right or co/cartesian fibrations, so this is not the end of the story. That's part of why I ask -- it's conceivable that one of these later steps will depend in an essential way on the initial choice of generic universes.

Improve this question
$\endgroup$
9
  • 4
    $\begingroup$ The construction of the universe I usually use is the one of Hofmann-Streicher. This construction goes way back before their work though. You may find variations on it in Giraud's book "Cohomologie non abélienne" (published in 1971) but the idea can be traced back to Grothendieck's SGA1 where the Grothendieck construction is introduced and various ways to rectify 2-functors are explained out of the induced biequivalence and a 2-categpriical version of the Yoneda LemmA (SGA1 is also published in 1971 but the seminar took place in 1961, and copies of the seminar notes circulated since then). $\endgroup$ Commented Apr 1, 2023 at 21:26
  • 5
    $\begingroup$ The general construction is as follows. Say you work with sheaves on a small site $C$. Then $x\mapsto Sh(C/x)$ is a stack i.e. a sheaf with values in the $(\infty,1)$-category of categories. We can replace this stack up to equivalence by a stack $F$ so that it is also an ordinary sheaf with values in the 1-category of categories. We can then define the universe $U=Ob(F)$. The choice of $F$ is irrelevant as long as it is obtained as above. All constructions of universes in practice are explicit choices of such $F$ of which we take subsheaves. $\endgroup$ Commented Apr 1, 2023 at 21:38
  • 1
    $\begingroup$ Yes I mean that the version I use in my book is isomorphic. And no, I do not claim that the universe of Hofmann-Streicher is equivalent to the stack; this does not make sense because they define a sheaf of sets as opposed to a stack. What I claim is that, the only thing that matters is to choose a sheaf F with values in the 1-category of 1-categories that is equivalent to 𝑥↦𝑆ℎ(𝐶/𝑥) (as 2-functors) and to define $U$ to the be the sheaf of sets obtained as 𝑥↦Ob(F(𝑥)). I claim that any such $U$ is OK. (...) $\endgroup$ Commented Apr 3, 2023 at 15:36
  • 2
    $\begingroup$ In addition to @D.-C.Cisinski's point above that all three of these maps are generic for the same class of maps, all 3 behave similarly wrt what strict/1-categorical structure we can equip them with. In fact, all 3 satisfy the "realignment lemma" so they function in much the same way; we are able to obtain excellent and very strict equalities on particular codes in these universes which we need to show eg, fibrancy. (For instance, Streicher has a note redoing the VV proof of fibrancy for the HS universe). $\endgroup$ Commented Apr 4, 2023 at 12:55
  • 3
    $\begingroup$ There are a few situations in type theory where one must replace the HS universe, but these are typically due to somewhat perverse constraints. For instance, satisfying some degree of the realignment lemma constructively (the HS universe relativizes), getting certain codes to be injective, etc. But these are all sort of non-invariant properties of the particular universe and typically invisible. See, for instance Lemma 5.9 of this pdf or this note $\endgroup$ Commented Apr 4, 2023 at 12:57

1 Answer 1

Reset to default
8
$\begingroup$

(Stumbling upon this old question I missed at the time.) At least for the Kapulkin–Lumsdaine paper on the simplicial model, our motivation for the choice was just following Voevodsky; and his motivation, I believe, was having a construction that would also work in a univalent foundation. Specifically, in a univalent setting, the presheaf of types needs to be a geniune presheaf, i.e. valued in sets (0-types). If the universe of sets you start from is univalent, then it’s a 1-type, and so the Hofmann–Streicher universe on it will be valued in 1-types. To adapt it to be set-valued, you need to start from a suitable universe of sets which is itself a set; and (assuming AC) taking a universe of well-ordered sets is the simplest way I know to achieve that (the rigidity of well-orderings cuts down the dimension). So I think Vladimir wouldn’t have been satisfied with the H–S construction applied to an arbitrary universe of sets, since in a univalent setting that’s not set-valued; I guess he would have been happy with a well-ordered version of the H–S universe, but the “isomorphism classes of well-ordered sets” version we use in the paper is the version he happened to come up with. Today we know that another way to obtain a set-universe of sets is to follow the classical set-theoretic approach and use an initial segment of the cumulative hierarchy; but that wasn’t available until Gylterud 2016, and (compared to the well-orderings approach) depends more heavily on the post-HoTT understanding of identity types.

(I’m somewhat extrapolatng Vladimir’s motivations here. I don’t remember ever hearing him compare the well-ordered universe with other alternatives — but on various other topics, he was clear that he preferred constructions that still work in a univalent foundation, even when he wasn’t explicitly working univalently.)

Improve this answer
$\endgroup$
10
  • 1
    $\begingroup$ I'm confused by your bolded statement a little bit. If we interpret the HS universe definition very literally (i.e., in terms of something like Aczel's definition of the cumulative hierarchy as a quotient of an inductive type), won't it be set-valued even if your starting category of 0-types is univalent since $V_\kappa$ is always rigid? I guess strictly speaking this needs to assume that the category of 0-types is equivalent to the category of pure sets, but you're talking about assuming AC anyway. $\endgroup$ Commented Jun 6, 2025 at 18:38
  • $\begingroup$ @JamesEHanson: Absolutely — but I think that very literal reading of the HS-definition isn’t the most obvious way to it adapt it to a type-theoretic setting, and certainly wasn’t back when Vladimir was working out the simplicial model (as the only type-theoretic treatment of the cumulative hierarchy then was Aczel’s original setoid-based one). For most things involving Grothendieck universes or similar, “a suitably-closed, possibly-univalent universe of sets” is a very good type-theoretic reading; really wanting “a segment of the cumulative hierarchy” is the exception not the rule. $\endgroup$ Commented Jun 9, 2025 at 14:09
  • $\begingroup$ Okay but your comment still isn't accurate then because the 'standard HS universe' is the one defined in terms of $V_\kappa$. The whole point of the definition is that $V_\kappa$ gives you a good canonical small representation of a universe. $\endgroup$ Commented Jun 9, 2025 at 14:20
  • $\begingroup$ @JamesEHanson: Interesting you see it as “the whole point”; I’ve always viewed the choice of $V_\kappa$ there as a detail specific to the material-set-theoretic presentation, and understood that Hofmann and Streicher also viewed it that way (see the 2nd and 3rd paras of their note). Most of the time, when you adapt a material-set-theoretic treatment to type theory, the right reading is to abstract away the set-theoretic representations — you certainly don’t want to read “ordered pairs” as the Kuratowski representation, etc. [cont’d] $\endgroup$ Commented Jun 9, 2025 at 14:59
  • 2
    $\begingroup$ @JamesEHanson: I largely agree — certainly in thinking that a lot of type-theoretic treatment of universes is not very principled or well-organised. Overlooking the cumulative hierarchy view in the answer was mainly because I was trying to recover motivations from 15+ years ago, when the type-theoretic treatment of the cumulative hierarchy was substantially less well understood, and so I don’t think it played much part in those motivations. $\endgroup$ Commented Jun 9, 2025 at 21:52

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.