# 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

## Site Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeDec 6th 2011

I have created an entry type of types. Wanted to collect some literature there, but ended up not finding too much…

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeSep 20th 2012

I found the entry type of types a bit lacking in information, when I needed to point to it (from the currently last comment of this G+ discussion). So I expanded just a little bit.

1. type universe used more commonly in the article

Anonymous

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeJun 6th 2022

Something strange happening with this page: When trying to (re-)sumit it, the parser complains about strings of the form

\ type


(i.e. backslash followed by whitespace is causing the error, but all the occurrences are followed by type)

What’s the intended syntax?

• CommentRowNumber5.
• CommentAuthorGuest
• CommentTimeJun 6th 2022

It used to be that having a backslash and a whitespace a la “\ ” used to allow the parser to parse the combination of characters into a whitespace in math mode, but that stopped working on the nLab a few days ago for some reason. “\ ” still works on my local computer’s latex editor to produce whitespaces in math mode.

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeJun 6th 2022

I see, thanks for saying. I’ll bring this to the attention of the technical team.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeJun 6th 2022

Christian Sattler has fixed it, already!

2. added section on cumulativity for universes

Anonymous

3. Added a paragraph about the relation between the three notions of Tarski universe

Anonymous

4. Added a paragraph on “mixed” Tarski universes which contain both strict definitional equalities and weak type equivalences in the definition of Tarski universe.

Anonymous

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeJan 21st 2023

added pointer to where exactly Martin-Löf 1975 speaks about universes (namely in §1.10)

added UFP 2013 as a reference item

added previously missing publication data for this item:

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeJan 21st 2023

• CommentRowNumber13.
• CommentAuthorUrs
• CommentTimeJan 21st 2023

expanded out this bibitem:

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeJan 31st 2023