added pointer to:

- Ralf Krömer, §6.4.5 in:
*Tool and object: A history and philosophy of category theory*, Science Networks. Historical Studies**32**(2007) [doi:10.1007/978-3-7643-7524-9]

added what I guess is the original reference:

- Per Martin-Löf (notes by Giovanni Sambin): p. 48 in:
*Intuitionistic type theory*, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) [pdf, MartinLofIntuitionisticTypeTheory.pdf:file]

and expanded out this bibitem:

- Martin Hofmann,
*Syntax and semantics of dependent types*, Chapter 2 in:*Extensional concepts in intensional type theory*, Ph.D. thesis, University of Edinburgh (1995), Distinguished Dissertations, Springer (1997) [ECS-LFCS-95-327, HofmannExtensionalIntensionalTypeTheory.pdf:file, doi:10.1007/978-1-4471-0963-1]

The entry used to point the reader to section 2.1.6 in there. But at least the above pdf version has no such section, instead the section titled “Universes” is 2.3.5. So I changed this, but let me know if I am missing something.

]]>added a section regarding closure of universes under all propositions.

Anonymous

]]>added paragraph about definitional univalence for Tarski universes

Anonymous

]]>added a definition of Tarski universe which does not involve a type family. This parallels the case in set theory where a family of sets is the fibers of a function rather than being a primitive concept.

Anonymous

]]>added section on hierarchies of Tarski universes

Anonymous

]]>expanded article significantly and renamed article to Tarski universe; the whole reason why one would want such an object is to build up various notions of Tarski universes in type theory, which may or may not be strictly or weakly closed under various type formers in the type theory

Anonymous

]]>Renamed due to parallels with other univalent objects like univalent category and univalent universe

Anonymous

]]>Tarski universes are supposed to refer to the entire structure consisting of a type $U$ and the type family $El$, not just the type $U$. So the corresponding name should be “univalent type with a type family” rather than “univalent index type of a type family”.

]]>Page created, but author did not leave any comments.

Anonymous

]]>