\section{Idea}
Tarski universes are the internal models of dependent type theory inside of a dependent type theory. They are useful in that one could define inductive types? and higher inductive types directly through the universal properties? of such types, rather than through the formation, introduction, elimination, computation, and uniqueness rules of such types.
\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)