I do unfortunately have a lot of stuff in my queue to be committed to paper at the moment. Maybe some of it will happen this summer.

The blog discussion with Cisinski is here.

]]>Urs, re 11.

Amazing that it is such a trouble for the community to bring such a simple idea to paper.

It really should be in a paper by Mike and Cisinski on the interpretation of type theory in higher toposes. I always have a bit of trouble blaming Mike not to be productive enough …

]]>never mind

]]>I had removed the pointers to Gallozzi after his advisor complained that he doesn’t want to see the thesis in public.

Amazing that it is such a trouble for the community to bring such a simple idea to paper.

]]>Cleaned up the references a bit more. Gallozi only does weak Tarski universes, Luo only strong. Is the definition of weak Tarski universe due to you Mike, or was it Gepner-Kock?

I cannot currently find the Shulman-Cisinski discussion on the n-cafe where this was worked out.

]]>(Also, it’s not a propositional equality, but rather an equivalence. We could make it into a propositional equality if both sides lived in some univalent universe… but that’s precisely the point at issue.)

]]>I’ve moved the citation of Luo to universe (homotopytypetheory), where the notions of Tarski universe are discussed.

]]>The references are for Tarski universes. Making them “weak” instead of “strong” is just in replacing a judgemental equality by a propositional one, isn’t it.

But if the references seem suboptimal you are more than welcome to finally, finally add decent references for weak Tarskian universes.

]]>There is more scattered discussion at type of types. This quotes Hofmann, but the treatment there is for strong Tarski universes. For completeness, Benno will speak on this topic in Hamburg

]]>model of type theory in an (infinity,1)-topos (homotopytypetheory) refers to Luo12 for weak Tarski universes. However, I cannot find it there. Also the references at universe (homotopytypetheory) do not seem optimal. I seem to recall the concept was first introduced by Hofmann. Does anyone know a precise reference?

I’ll add it myself when I find it.

]]>In addition to this, both agda and lean do without cumulativity of universes. This should probably simplify the relation between Tarski and Russell universes too.

]]>I find it curious that he asserts without justification that

The basic subtyping relations … should be propagated through the type constructors.

That’s not how Coq behaves for inductive types.

]]>Thanks for the link to Luo 12! This is the kind of reference that I was looking for before, without much luck. Did we have it on the $n$Lab and I missed it somehow? I have added it now to the relevant entries.

Regarding the notation: I suppose it’s the natural notation from the point of view of term introduction rules, as first we have a term $X \colon U$ of the Tarski universe, then *then* we get an actual type from this, so it needs a name that depends on the previous name.

What’s the current thinking about the benefits of each, and the relationship between them? I’ve taken a look at Zhaohui Luo’s notes.

The Tarski-style universes are semantically more fundamental but the Russell-style universes are easier to use in practice.

…

… it is argued that the essence of the Russell-style universes can be obtained by means of the Tarski-style universes together with coercive subtyping in taking the explicit lifting operators between universes as coercions (plus some notational conventions). In this way, one may obtain both the theoretical adequacy and the easy-to-use benefit.

For some reason, the Tarskian approach of types and codes for types in the universe seems easier to grasp. Is there a reason for denoting the ’code’ with the simpler syntax, $A$, and the type itself as the more complicated $El(A)$?

Mind you, I guess I have been suggesting something similar with my $P$ and ’Fact that $P$’ distinction here.

]]>