\tableofcontents
\section{Idea}
In intensional type theory?, there are typically two ways to construct a “type of small types”. One way is by Russell universes, where a term? of a universe type? is literally a type . The alternative is by Tarski universes, where terms are not literally types, but rather the universe type comes with the additional structure of a type family , such that the dependent type represents the actual type.
Usually universes are defined using derivations? and rules?, such as the type reflection rule
for Tarski universes. However, one could also study Tarski universes mathematically as mathematical structure?: as a type with a type family indexed by , in the same way that one studies univalent categories? as a type with a set-valued binary type family indexed by pairs and so forth. In this manner, Tarski universes become internal models of dependent type theory inside of an intensional type theory?. Furthermore, the type formers could be defined by the categorical universal properties? as homotopy limits? or homotopy colimits? defined suitably, rather than directly through the formation rules?, introduction rules?, elimination rules?, computation rules?, and uniqueness rules? in the external syntax of the type theory.
This article treats Tarski universes as actual mathematical objects, rather than as something in the foundations of mathematics? to do mathematics in.
\section{Definition}
We work inside of a dependent type theory with type judgments and term judgments and a notion of identity types, dependent sum types?, and dependent product types?.
A Tarski universe is a type with a type family whose dependent types are indexed by terms .
The terms represent the internal types of the universe, or equivalently, the -small types. An internal type family or a locally -small type family in indexed by a internal type is represented by a function ; for each term the term is a dependent type, and the term is a dependent term or section.
\section{Properties}
Already, we could define certain external properties a Tarski universe could have.
There are two notions of equivalence in a Tarski universe , equality and equivalence . There is a canonical transport dependent function
A Tarski universe is externally univalent if for all terms and the function is an equivalence of types
Similarly, a Tarski universe satisfies the external axiom K? if for all terms the type is an h-set?
It is possible for a Tarski universe to be both externally univalent and satisfy the external axiom K: the resulting Tarski universe is an h-groupoid?, since the type of equivalences between any two h-sets? and is an h-set? itself.
There are other versions of axiom K, one for each h-level? : for all terms the type is at h-level?
If is also externally univalent, then has h-level? .
A Tarski universe satisfies the external axiom of choice? if for all -small types , locally -small type families , and dependent functions such that
there is a witness
where the type is the propositional truncation? of the type .
Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. (web, pdf)
Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (pdf) (478 pages)