Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 13 of 13
there is this new master thesis:
which discusses aspects of weak Tarskian homotopy type universes following the indications that Mike Shulman has been making, for instance at universe (homotopytypetheory). I just got permission to share this and I have now included pointers to the thesis to that entry, to type of types, etc.
Thanks for sharing this. I am a bit surprised about the discussion at the end. The thesis seems to contain a variation (weak universes) on the Aczel interpretation, but does not appear to fit very well with the ideas behind HoTT. E.g. is it clear that all the constructed sets are hSets?
I only interacted with Cesare at an early stage of this thesis, when I highlighted the issue of weak Tarskian universes in models of homotopy type theory to him. That was shortly after I had asked Mike to write the entry model of type theory in an (infinity,1)-topos (homotopytypetheory) (which he very kindly did!) in order for there to be at least some minimum of public written account of the statement that every $\infty$-topos models HoTT if one allows weak Tarskian type universes (maybe even with strict ones, but while this is open, it is important to record the statement for the weak Tarskian ones). At some point I thought that would be what Cesare was going to investigate in his thesis, but I was not involved anymore beyond that, and the plans have clearly been different, and I suppose also time constraints played a role.
So I have seen that last section on models of constructive set theory with weak Tarskian universes just the other day for the first time, too. I am also a wondering what the relation of that section 6 to the standard hSets would be. I don’t know. You’d be a canonical expert to say more about this! :-)
Notice that the third paragraph of the conclusions has a comment, ever so brief, on the relation with the discussion in the HoTT book.
In any case, what I am really looking forward to is that somebody will publish the proof of the statement that HoTT with weak Tarskian univalent universes has interpretation in any $\infty$-stack $\infty$-topos. Mike said this is too easy a consequence of his previous publications to make for a publication, and I suppose he is too busy anyway, but what is easy for Mike is a mystery to other HoTT researchers and just for the record it would be immensely useful to have this statement formally published. When you next run into a Master student looking for a HoTT thesis topic, give him this and make him or here write this out and publish it!
I guess one can carry out the construction in hSets (they are closed under W-types) and end up with an hSet. However, one would still end up with a setoid V, not a type. An important advantage of HoTT is precisely that we do not need setoids anymore.
Thanks for that comment.
I think I was too optimistic/generous. $V := (W x : U)El(x)$. perhaps we can have the collection of codes as an hSet, but El maps into the universe type, certainly not an hSet. So, the closed-under-W-types argument does not apply. The construction seems correct, but it is unclear to me how it is relevant to HoTT.
@Urs #3 just one correction, it’s not a consequence of my work, but of the (still unpublished) coherence theorem for models of type theory of Lumsdaine-Warren, together with the proof by Cisinski and Gepner-Kock that every locally cartesian closed locally presentable $(\infty,1)$-category can be presented by a right proper Cisinski model category.
FWIW, I don’t think it’s likely that any model constructed out of hsets (= 0-truncated types) can be shown to satisfy collection without some additional assumption on the type theory, such as an AST-like collection axiom that every surjection onto a small type is factored through by a surjection with small domain.
Re #9. We have some remarks along these lines in sec 3.5 of our paper:
The 0-truncated types in the cubical set model are precisely the setoids. Considering the cubical model inside an extensional type theory with a propositions- as-types interpretation, every set has a projective cover [45]. The same holds if we have the axiom of choice in the meta-theory. Both the collection axiom [21, 5.2] and AMC follow from this axiom [32]. On the other hand [37, Prop. 11.2], the 0-truncation of a model topos of simplicial sheaves on a site is the topos of sheaves on that site. Hence, if we start with a topos without countable choice, we cannot have projective covers in the cubical sets model. This suggests investigating homotopy type theory with and without this axiom. It is argued in [11] that we need AMC to obtain a model theory for predicative toposes with good closure properties, e.g. closure under sheaf models. Concretely, AMC is used to show that W-types are small in sheaf models, but also to show that every inter- nal site is presentable. It would be interesting to reconsider the latter of these issues in the presence of higher inductive types and the univalence axiom.
AMC is the same as WISC, in nLab parlance.
the rough idea of the thesis is that weak Tarski universes can be motivated in some way (for example from the models), but they need some kind of justification from the point of view of constructive mathematics.
For what it’s worth, I would have thought, conversely, that propositional equality has better motivation from the point of view of constructive mathematics than judgemental equality (since it requires to construct witnesses of equality) and that therefore the weak version of Tarski type universes would be better motivated, constructively, while from the constructive point of view one would have to argue why the strict version is even justified.
(Which is essentially what happens in the models in infinity-toposes: they are constructive and hence much strictification work is necessary, if it works at all, to turn these propositional equalities into judgemental equalities in these models.)
But probably that’s a different kind of “motivation” than you mean?
1 to 13 of 13