Timeline for answer to Is there any reason not to use Hofmann-Streicher universes? by Peter LeFanu Lumsdaine
Current License: CC BY-SA 4.0
Post Revisions
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 9, 2025 at 21:52 | comment | added | Peter LeFanu Lumsdaine | @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. | |
| Jun 9, 2025 at 16:43 | comment | added | James E Hanson | Even in contexts like the type theory of Rocq where universe levels are implemented in a relative way with ad hoc polymorphism, I don't see a deep philosophical reason for enshrining that particular level of type closure in syntax. It makes it awkward to talk about classical theories that are weaker than $\mathsf{ZFC}$ with inaccessible cardinals, but it also raises the question of why you're stopping at that particular strength. One could take Mahlo universes as primitive, for instance. | |
| Jun 9, 2025 at 16:37 | comment | added | James E Hanson | And personally I think that universes are something that set theory handles in a better and more principled way than type theory does. Universes in type theory seem to always be inserted by hand in an arguably ad hoc way. In situations where there's an explicitly named sequence of universes, there is no universal property that characterizes them. You could relabel your universes in a model of type theory with any increasing sequence of natural numbers and get an equally good model. | |
| Jun 9, 2025 at 16:33 | comment | added | James E Hanson | I shouldn't have phrased it like that because I don't really know what people consider the point of the HS definition of universes to be. I just think that there's a bit of a double standard at play in these kinds of conversations. When the natural translation of an ordinarily set-theoretic concept to type theory makes it smoother, people are quick to point this out, but this is a situation in which the translation seemingly makes it more awkward and the original version of your answer seemed, to me, to be minimizing this fact. | |
| Jun 9, 2025 at 15:19 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
clarified in response to James E Hanson’s comments
|
| Jun 9, 2025 at 15:03 | comment | added | Peter LeFanu Lumsdaine | [cont’d] I’ve always understood understood the H–S construction as applying to Gr. univs in one of these abstract senses, and so as requiring an hset-universe of hsets as input; and I didn’t realise that the cumulative hierarchy gave a construction of these in type theory until Håkon Gylterud pointed it out probably around 2016 or so (and I don’t know of anyone else having been aware of that sooner). I will edit the answer to slightly clarify this point! | |
| Jun 9, 2025 at 15:00 | comment | added | Peter LeFanu Lumsdaine | [cont’d] For “set”, the right reading is almost always either “type”, “hset/0-type”, or “subtype (of some ambient type/hset)”, very rarely “element of the cumulative hierarchy”. And for “Grothendieck universe”, the right reading is often “a suitably-closed family of hsets”, or sometimes “a suitably closed hset-indexed family of hsets” (and when H–S were writing in the 90’s, the implications of the choice between these weren’t yet well-understood). [cont’d] | |
| Jun 9, 2025 at 14:59 | comment | added | Peter LeFanu Lumsdaine | @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] | |
| Jun 9, 2025 at 14:20 | comment | added | James E Hanson | 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. | |
| Jun 9, 2025 at 14:09 | comment | added | Peter LeFanu Lumsdaine | @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. | |
| Jun 6, 2025 at 18:38 | comment | added | James E Hanson | 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. | |
| Jun 6, 2025 at 16:03 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
fixed typo; plus slight style edits
|
| Jun 6, 2025 at 11:32 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |