Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory object of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 13th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexWhat's the current thinking about the benefits of each, and the relationship between them? I've taken a look at Zhaohui Luo's [notes](http://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf). >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](http://nforum.mathforge.org/discussion/5332/generalized-the/?Focus=51627#Comment_51627).

   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.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeApr 13th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks for the link to [Luo 12](http://ncatlab.org/nlab/show/type+of+types#Luo12)! 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.

   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.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeApr 13th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorspitters
   • CommentTimeApr 14th 2015
   • PermaLink
   Author: spitters
   Format: MarkdownItexIn addition to this, both agda and lean do without cumulativity of universes. This should probably simplify the relation between Tarski and Russell universes too.

   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.

5. • CommentRowNumber5.
   • CommentAuthorspitters
   • CommentTimeJun 23rd 2015
   • PermaLink
   Author: spitters
   Format: MarkdownItex[[homotopytypetheory:model of type theory in an (infinity,1)-topos ]] refers to Luo12 for weak Tarski universes. However, I cannot find it there. Also the references at [[homotopytypetheory:universe]] 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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorspitters
   • CommentTimeJun 23rd 2015
   • PermaLink
   Author: spitters
   Format: MarkdownItexThere 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](https://sites.google.com/site/dmv2015hott/)

   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

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeJun 23rd 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexThe 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeJun 24th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI've moved the citation of Luo to [[homotopytypetheory:universe]], where the notions of Tarski universe are discussed.

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

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJun 24th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex(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.)

   (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.)

10. • CommentRowNumber10.
    • CommentAuthorspitters
    • CommentTimeJun 24th 2015
    • PermaLink
    Author: spitters
    Format: MarkdownItexCleaned 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.

    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.

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJun 24th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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.

    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.

12. • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 24th 2015
    • (edited Jun 24th 2015)
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexnever mind

    never mind

13. • CommentRowNumber13.
    • CommentAuthorspitters
    • CommentTimeJun 29th 2015
    • PermaLink
    Author: spitters
    Format: MarkdownItexUrs, 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 ...

    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 …

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeJun 29th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI 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](https://golem.ph.utexas.edu/category/2012/05/the_mysterious_nature_of_right.html#c041306).

    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.