\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]] $A:U$ of a [[universe type]] $U$ is literally a [[type]] $A \; \mathrm{type}$. The alternative is by Tarski universes, where terms $A:U$ are not literally types, but rather the universe type $U$ comes with the additional structure of a [[type family]] $T$, such that the [[dependent type]] $T(A)$ represents the actual type. Usually universes are defined using [[derivations]] and [[rules]], such as the type reflection rule $$\frac{\Gamma \vdash A:U}{\Gamma \vdash T(A) \; \mathrm{type}}$$ for Tarski universes. However, one could also study Tarski universes mathematically as [[mathematical structure]]: as a type $A$ with a type family $B(a)$ indexed by $a:A$, in the same way that one studies [[univalent categories]] as a type $A$ with a set-valued binary type family $B(a, b)$ indexed by pairs $(a, b):A \times A$ 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 $U$ with a type family $T$ whose dependent types $T(A)$ are indexed by terms $A:U$. The terms $A:U$ represent the internal types of the universe, or equivalently, the **$U$-small types**. An internal type family or a **locally $U$-small** type family $B$ in $U$ indexed by a internal type $A:U$ is represented by a function $B:T(A) \to U$; for each term $a:T(A)$ the term $B(a)$ is a dependent type, and the term $b(a):T(B(A))$ 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 $(U, T)$, equality $A =_U B$ and equivalence $T(A) \simeq T(B)$. There is a canonical [[transport]] dependent function $$\mathrm{transport}^T:\prod_{A:U} \prod{B:U} (A =_U B) \to T(A) \simeq T(B)$$ A Tarski universe is **externally [[univalent universe|univalent]]** if for all terms $A:U$ and $B:U$ the function $\mathrm{transport}^T(A, B)$ is an equivalence of types $$\prod_{a:A} \prod_{b:B} \mathrm{isEquiv}(\mathrm{transport}^T(A, B))$$ Similarly, a Tarski universe satisfies the **external [[axiom K]]** if for all terms $A:U$ the type $T(A)$ is an [[h-set]] $$\prod_{a:A} \mathrm{ishSet}(T(A))$$ It is possible for a Tarski universe to be both externally univalent and satisfy the external axiom K: the resulting Tarski universe $U$ is an [[h-groupoid]], since the type of equivalences $A \simeq B$ between any two [[h-sets]] $A$ and $B$ is an [[h-set]] itself. There are other versions of axiom K, one for each [[h-level]] $n$: for all terms $A:U$ the type $T(A)$ is at [[h-level]] $n$ $$\prod_{a:A} \mathrm{isHLevel}(n, T(A))$$ If $U$ is also externally univalent, then $U$ has [[h-level]] $n + 1$. A Tarski universe satisfies the **external [[axiom of choice]]** if for all $U$-small types $A:U$, locally $U$-small type families $B:A \to U$, and dependent functions $P:\Prod_{a:T(A)} B(a) \to U$ such that * $T(A)$ is an [[h-set]] * $T(B(a))$ is an [[h-set]] for all terms $a:T(A)$ * $P(b, a)$ is an [[h-proposition]] for all terms $a:T(a)$ and $b:T(B(a))$ there is a witness $$\mathrm{choice}(A, B, P):\left(\prod_{a:T(A)} \left[ \sum_{b:T(B(a))} P(b, a) \right] \right) \to \left[ \sum_{g:\Prod_{a:T(A)} B(a)} \prod_{a:T(A)} P(x, g(x)) \right]$$ where the type $\left[A\right]$ is the [[propositional truncation]] of the type $A$. ## Tarski universe homomorphisms ## Universe hierarchies ## Internalization of types ### Identity types ### Dependent function types ### Dependent sum types ### Internal properties ## References * *Homotopy Type Theory: Univalent Foundations of Mathematics*, The Univalent Foundations Program, Institute for Advanced Study, 2013. ([web](http://homotopytypetheory.org/book/), [pdf](http://hottheory.files.wordpress.com/2013/03/hott-online-323-g28e4374.pdf)) * Egbert Rijke, *Introduction to Homotopy Type Theory*, Cambridge Studies in Advanced Mathematics, Cambridge University Press ([pdf](https://raw.githubusercontent.com/martinescardo/HoTTEST-Summer-School/main/HoTT/hott-intro.pdf)) (478 pages) [[!redirects Tarski universe]] [[!redirects Tarski universes]] [[!redirects weakly Tarski universe]] [[!redirects weakly Tarski universes]]