\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 $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]]