# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeOct 17th 2014
• (edited Oct 23rd 2014)

there is this new master thesis:

• Cesare Gallozzi, Constructive Set Theory from a Weak Tarski Universe, MSc thesis (2014)

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.

• CommentRowNumber2.
• CommentAuthorspitters
• CommentTimeOct 17th 2014

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?

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeOct 18th 2014
• (edited Oct 18th 2014)

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!

• CommentRowNumber4.
• CommentAuthorspitters
• CommentTimeOct 18th 2014

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.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeOct 19th 2014

Thanks for that comment.

• CommentRowNumber6.
• CommentAuthorspitters
• CommentTimeOct 19th 2014

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.

1. Thank you for sharing my thesis Urs!

Regarding the questions, 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.
Aczel used the type-theoretical interpretation of CZF to provide justification for his set theory and motivate new axioms, after many years we are used to CZF and we think we understand it, so we can use it now to motivate variants of Martin-Löf type theory.

I still would like to see a construction of a model of CZF by means of 0-truncated types (is hSets another name for them?).

If you have other comments or questions about my thesis I would be glad to answer.
• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeOct 22nd 2014

@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.

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeOct 22nd 2014

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.

• CommentRowNumber10.
• CommentAuthorspitters
• CommentTimeOct 22nd 2014

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.

• CommentRowNumber11.
• CommentAuthorDavidRoberts
• CommentTimeOct 22nd 2014

AMC is the same as WISC, in nLab parlance.

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeOct 22nd 2014
• (edited Oct 22nd 2014)

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?

2. Actually, I think that judgemental equalities are justified in a constructivist framework: they provide a notion of equality at the level of judgements and are derived using a finitary sistem of rules from other judgements, and the computational rules for the type constructors are the type theoretic analogous to the conversion rules in natural deduction given by Prawitz.