nLab Tarski universe

Idea

In intensional type theory and homotopy 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 type universe $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 in intensional type theory and homotopy type theory using derivations and rules?, such as the type reflection rule

$$\frac{\Gamma \vdash A:U}{\Gamma \vdash T(A) \; \mathrm{type}}$$

for Tarski universes. Furthermore, universes are usually defined as being closed under all type formers inside the type theory, regardless of the type theory.

However, this approach of defining Tarski universes means that the notion of “Tarski universe” differs from type theory to type theory. By this approach, a Tarski universe in the bare intensional Martin-Löf type theory, which has identity types, dependent product types, dependent sum types, an empty type, a unit type, a booleans type, and a natural numbers type, would not be considered a Tarski universe in homotopy type theory, since it is missing important type formers present in homotopy type theory, such as internal pushout types, a torus type?, propositional truncations, W-types, and localizations. On the other hand, one could consider an even more spartan type theory which doesn’t even have the unit type, let alone the empty type, the natural numbers type, and the booleans type, whose Tarski universes are thus consisting of only internal identity types, dependent product types, dependent sum types.

All three notions of Tarski universe described above are in fact definable in all three versions of intensional type theory mentioned above, but Tarski universes are usually described as having, apart from addiitonal internal Tarski universes, exactly the internal type formers that the external type theory has. One usually doesn’t consider Tarski universes with an internal James construction type in bare intensional Martin-Löf type theory, even though a Tarski universe closed under James constructions is definable in Martin-Löf type theory. On the other hand, in homotopy type theory the name “Tarski universe” isn’t usually used for a universe only closed under identity types, dependent product types, dependent sum types.

From a global perspective, however, all of these types should be considered Tarski universes, since they model some notion of type of small types, even though the small types in the universe do not behave as the external types in the type theory do. And that is how we approach Tarski universes in this article: Tarski universes are a very general notion encompassing all of the above notions of Tarski universe and more, and one could describe more specific versions of Tarski universes by adding additional structure and axioms to Tarski universes, in the same way one adds additional structure and axioms to an abelian group to get a ring, a commutative ring, a $R$-module, a $R$-algebra, and an $R$-commutative algebra. We could then study in general Tarski universes and their properties as we do for abelian groups and rings. This requires a shift in the point of view of what Tarski universes are: Tarski universes are actual mathematical structure in intensional type theory, rather than being something in the foundations of mathematics to merely address size? issues or do mathematics in.

Definition

With a family of types

A Tarski universe or universe à la Tarski is simply a type $U$ with a type family $T$ whose dependent types $T(A)$ are indexed by terms $A:U$. The terms $A:U$ are usually called $U$-small types, or small types for short, and $T(A)$ is the type of terms of $A$.

With a type and a function

A Tarski universe or universe à la Tarski is a type $U$ of all $U$-small types with a type $T'$ of all terms, and a function $\mathrm{typeOf}:T' \to U$ which gets the associated type for every term $a:T'$.

Equivalence of definitions

From one direction, the individual dependent types $T(A)$ could be defined as the fiber type of $\mathrm{typeOf}$ at $A$

$$T(A) \coloneqq \mathrm{fiber}_{T', U}(\mathrm{typeOf},A)$$

From the other direction, the entire type of terms $T'$ is just the dependent sum type of all the type reflections of small types

$$T' \coloneqq \sum_{A:U} T(A)$$

We shall be using the first definition throughout this article, but everything could be translated into the second definition of a Tarski universe.

Tarski universes as models of type theory

The definitions above are already enough to build an internal model of dependent type theory inside the Tarski universe:

• The type $A \; \mathrm{type}$ is represented by the small type $A:U$
• The term $a:A$ is represented by the term $a:T(A)$ for small type $A:U$.
• The type family $B$ indexed by the type $A \; \mathrm{type}$ is represented by the function $B:T(A) \to U$ for small type $A:U$
• The dependent type $a:A \vdash B \; \mathrm{type}$ is represented by the section $B(a):U$ for term $a:T(A)$ and small type $A:U$.
• The section $a:A \vdash b:B$ is represented by the term $b:T(B(a))$ for term $a:T(A)$ and small type $A:U$.

Univalence

There are two notions of equivalence in a Tarski universe $(U, T)$, equality $A =_U B$ and equivalence $T(A) \simeq T(B)$. By the properties of the identity type, 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 a univalent Tarski universe if for all terms $A:U$ and $B:U$ the function $\mathrm{transport}^T(A, B)$ is an equivalence of types

$$\prod_{A:U} \prod_{B:U} \mathrm{isEquiv}(\mathrm{transport}^T(A, B))$$

This is the extensionality principle for any Tarski universe $(U, T)$.

Equivalently, by the fundamental theorem of identity types, a Tarski universe is a univalent Tarski universe if it comes with a dependent function

$$t:\prod_{X:U} C(X, X, \mathrm{id}_X) \vdash J(t):\prod_{A:U} \prod_{B:U} \prod_{R:T(A) \simeq T(B)} C(A, B, R)$$

and a dependent function

$$t:\prod_{X:U} C(X, X, \mathrm{id}_X) \vdash \beta(t):\prod_{A:U} J(t, A, A, \mathrm{id}_A) =_{C(A, A, \mathrm{id}_A)} t(A)$$

When the Tarski universe is closed under identity types, dependent sum types, and dependent product types (see below for more on closure of Tarski universes under type formers), one is able to internalize the type of equivalences in the universe as $A \simeq_U B$. It can be proven that $T(A \simeq_U B)$ is equivalent to $T(A) \simeq T(B)$, and that the definition of univalence using transport is equivalent to the usual definition given by the internal type of equivalences and the canonical function $\mathrm{idtoequiv}$. See at Univalence axiom#For Tarski universes for more details on this.

Construction of univalent Tarski universes via a higher inductive type

Let $(U, T)$ be a Tarski universe. Then one could construct a univalent Tarski universe as the higher inductive type $(U', T')$ generated by

• a function $F:U \to U'$
• a function $G(A):T(A) \to T'(A)$ for all terms $a:U$
• a dependent function
  $$\mathrm{ua}_{U'}:\prod_{A:U} \prod_{B:U} \mathrm{isEquiv}(\mathrm{transport}^{T'}(A, B))$$

Tarski universes with all propositions

A Tarski universe $(U, T)$ has all propositions if given a type $A$ with a family of identities $x:A, y:A \vdash \tau_{-1}(x, y):x =_A y$, the universe $U$ comes with the structure of an element $A_U:U$ and an equivalence $\delta_A:T(A_U) \simeq A$.

The rules for this condition on Tarski universes is as follows:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash \tau_{-1}(x, y):x =_A y}{\Gamma \vdash A_U:U} \qquad \frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A, y:A \vdash \tau_{-1}(x, y):x =_A y}{\Gamma \vdash \delta_A:T(A_U) \simeq A}$$

Given a Tarski universe which has all propositions, the type $\sum_{A:U} \mathrm{isProp}(T(A))$ is the type of all propositions. This is a form of strong impredicativity in the type theory, as given a type $A$, the type $A \to \sum_{A:U} \mathrm{isProp}(T(A))$ is the power set on $A$.

Closure of Tarski universes under type formers

There are many ways of defining type formers internally in a universe:

• by an equivalence or definitional equality with an existing global type former for the entire type theory.

• by translating the rules for the type former into internal structure on the universe

• by using the universal properties corresponding to the categorical semantics of the types

Using a definitional equality with an existing global type former for each type former results in a strict Tarski universe, while using equivalences for each type former results in a weak Tarski universe. There are also various Tarski universes where some type formers are strictly closed, and some type formers are only weakly closed, resulting in Tarski universes which are intermediate between strict Tarski universes and weak Tarski universes.

Empty type

A Tarski universe is closed under the empty type if the universe comes with

• a term $\emptyset_U:U$
• a dependent function
  $$\mathrm{ind}_\emptyset:\prod_{C:T(\emptyset_U) \to U} \prod_{p:T(\emptyset_U)} T(C(p))$$
• a dependent function
  $$\eta_\emptyset:\prod_{C:T(\emptyset_U) \to U} \prod_{p:T(\emptyset_U)} \mathrm{isContr}(T(C(p)))$$

If the type theory has an empty type $\emptyset \; \mathrm{type}$ external to the Tarski, universe, then an equivalence $\mathrm{smallemptytype}:T(\emptyset_U) \simeq \emptyset$ could be constructed. A Tarski universe is strictly closed under the empty type if there is a definitional equality $T(\emptyset_U) \equiv \emptyset$.

Unit type

A Tarski universe is closed under the unit type if the universe comes with

• a term $\mathbb{1}_U:U$
• a term $*:T(\mathbb{1}_U)$
• a dependent function
  $$\mathrm{ind}_\mathbb{1}: \prod_{C:T(\mathbb{1}_U) \to U} \prod_{p:T(\mathbb{1}_U)} T(C(*)) \to T(C(p))$$
• a dependent function
  $$\beta_\mathbb{1}:\prod_{C:T(\mathbb{1}_U) \to U} \mathrm{isContr}(T(C(*)))$$
• a dependent function
  $$\eta_\mathbb{1}:\prod_{C:T(\mathbb{1}_U) \to U} \prod_{p:T(\mathbb{1}_U)} \mathrm{isContr}(T(C(*))) \to \mathrm{isContr}(T(C(p)))$$

If the type theory has an unit type $\mathbb{1} \; \mathrm{type}$ external to the Tarski, universe, then an equivalence $\mathrm{smallunittype}:T(\mathbb{1}_U) \simeq \mathbb{1}$ could be constructed. A Tarski universe is strictly closed under the unit type if there is a definitional equality $T(\mathbb{1}_U) \equiv \mathbb{1}$.

Booleans type

A Tarski universe is closed under the booleans type if the universe comes with

• a term $\mathbb{2}_U:U$
• a term $0:T(\mathbb{2}_U)$
• a term $1:T(\mathbb{2}_U)$
• a dependent function
  $$\mathrm{ind}_\mathbb{2}: \prod_{C:T(\mathbb{2}_U) \to U} \prod_{p:T(\mathbb{2}_U)} T(C(0)) \times T(C(1)) \to T(C(p))$$
• a dependent function
  $$\beta_\mathbb{2}^0:\prod_{C:T(\mathbb{2}_U) \to U} \mathrm{isContr}(T(C(0)))$$
• a dependent function
  $$\beta_\mathbb{2}^1:\prod_{C:T(\mathbb{2}_U) \to U} \mathrm{isContr}(T(C(1)))$$
• a dependent function
  $$\eta_\mathbb{2}:\prod_{C:T(\mathbb{2}_U) \to U} \prod_{p:T(\mathbb{2}_U)} \mathrm{isContr}(T(C(0))) \times \mathrm{isContr}(T(C(1))) \to \mathrm{isContr}(T(C(p)))$$

If the type theory has an booleans type $\mathbb{2} \; \mathrm{type}$ external to the Tarski, universe, then an equivalence $\mathrm{smallbool}:T(\mathbb{2}_U) \simeq \mathbb{2}$ could be constructed. A Tarski universe is strictly closed under the booleans type if there is a definitional equality $T(\mathbb{2}_U) \equiv \mathbb{2}$.

Natural numbers type

A Tarski universe is closed under the natural numbers type if the universe comes with

• a term $\mathbb{N}_U:U$
• a term $0:T(\mathbb{N}_U)$
• a function $s:T(\mathbb{N}_U) \to T(\mathbb{N}_U)$
• a dependent function
  $$\mathrm{ind}_\mathbb{N}: \prod_{C:T(\mathbb{N}_U) \to U} \prod_{p:T(\mathbb{N}_U)} \left(T(C(0)) \times \prod_{n:T(\mathbb{N}_U)} T(C(n)) \to T(C(s(n)) \right) \to T(C(p))$$
• a dependent function
  $$\beta_\mathbb{N}^0:\prod_{C:T(\mathbb{N}_U) \to U} \mathrm{isContr}(T(C(0)))$$
• a dependent function
  $$\beta_\mathbb{N}^s:\prod_{C:T(\mathbb{N}_U) \to U} \prod_{n:T(\mathbb{N}_U)} \mathrm{isContr}(T(C(n))) \to \mathrm{isContr}(T(C(s(n))))$$
• A dependent function
  $$\eta_\mathbb{N}: \prod_{C:T(\mathbb{N}_U) \to U} \prod_{p:T(\mathbb{N}_U)} \left(\mathrm{isContr}(T(C(0))) \times \prod_{n:T(\mathbb{N}_U)} \mathrm{isContr}(T(C(n))) \to \mathrm{isContr}(T(C(s(n)))) \right) \to \mathrm{isContr}(T(C(p)))$$

If the type theory has a natural numbers type $\mathbb{N} \; \mathrm{type}$ external to the Tarski, universe, then an equivalence $\mathrm{smallnat}:T(\mathbb{N}_U) \simeq \mathbb{N}$ could be constructed. A Tarski universe is strictly closed under the nqtural numbers type if there is a definitional equality $T(\mathbb{N}_U) \equiv \mathbb{N}$.

Identity types

Dependent function types

Dependent sum types

Tarski subuniverses

Let $(U, T_U)$ be a Tarski universe. A Tarski universe $(V, T_V)$ is a Tarski subuniverse of $(U, T_U)$ if it comes with an embedding $t:V \hookrightarrow U$ and a dependent function

$$p:\prod_{a:V} T_U(t(a)) \simeq T_V(a)$$

This is equivalent to a family of Tarski universes $(U(i), T(i))$ indexed by terms $i:\mathbb{2}$ of the interval preorder $(\mathbb{2}, \leq_\mathbb{2})$, which comes with

• a dependent function

  $$t:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} (a \leq_\mathbb{2} b) \to (U(a) \hookrightarrow U(b))$$

• a dependent function

  $$q:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \prod_{A:U(a)} T(a)(A) \simeq T(b)(t(a, b)(p)(A))$$

  indicating that lifting each small type results in a type equivalent to the original small type.

Essentially small Tarski universes

A Tarski universe $(V, T_V)$ inside of a Tarski universe $(U, T_U)$ consists of a term $V:U$ and a function $T_V:T_U(V) \to U$.

Given a Tarski universe $(U, T_U)$, a Tarski universe $(V, T_V)$ is essentially $U$-small if it comes with

• a term $V':U$

• a function $T_{V'}:T_U(V') \to U$

• an equivalence

  $$\mathrm{smallType}:V \simeq T_U(V')$$

• a dependent function

  $$\mathrm{smallFamily}:\prod_{A:V} T_V(A) \simeq T_U(T_{V'}(\mathrm{smallType}(A)))$$

Equivalently, the entire structure could be regarded as a family of Tarski universes $(U(a), T(a))$ indexed by terms $a:\mathbb{2}$ of the interval preorder $(\mathbb{2}, \leq_\mathbb{2})$, which comes with

• a dependent function

  $$U':\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \left((b \leq_\mathbb{2} a) \to \emptyset\right) \to U(b)$$

• a dependent function

  $$T':\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \left((b \leq_\mathbb{2} a) \to \emptyset\right) \to \left(T(b)(U'(a, b, p)) \to U(b)\right)$$

• an dependent function

  $$\mathrm{smallType}:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \left((b \leq_\mathbb{2} a) \to \emptyset\right) \to \left(U(a) \simeq T(b)(U'(a, b, p))\right)$$

• a dependent function

  $$\mathrm{smallFamily}:\prod_{a:\mathbb{2}} \prod_{b:\mathbb{2}} \prod_{p:a \leq_\mathbb{2} b} \left((b \leq_\mathbb{2} a) \to \emptyset\right) \to \prod_{A:U(a)} T(a)(A) \simeq T(b)(T'(a, b, p)(\mathrm{smallType}(a, b, p)(A)))$$

Hierarchy of Tarski universes

Let $P$ be a preorder. Then, a $P$-indexed hierarchy of Tarski universes is a type family $U$ such that for all indices $a:P$, there is a Tarski universe $(U(a), T(a))$, such that for all indices $a:P$ and $b:P$ and witnesses $p:a \leq_P b$, the Tarski universe $(U(a), T(a))$ is an essentially $U(b)$-small Tarski subuniverse of the Tarski universe $(U(b), T(b))$.

Expanded out, the family of Tarski universes $(U(a), T(a))$ indexed by terms $a:P$ additionally come with

• a dependent function

  $$U':\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \left((b \leq_P a) \to \emptyset\right) \to U(b)$$

• a dependent function

  $$T':\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \left((b \leq_P a) \to \emptyset\right) \to \left(T(b)(U'(a, b, p)) \to U(b)\right)$$

• an dependent function

  $$\mathrm{smallType}:\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \left((b \leq_P a) \to \emptyset\right) \to \left(U(a) \simeq T(b)(U'(a, b, p))\right)$$

• a dependent function

  $$\mathrm{smallFamily}:\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \left((b \leq_P a) \to \emptyset\right) \to \prod_{A:U(a)} T(a)(A) \simeq T(b)(T'(a, b, p)(\mathrm{smallType}(a, b, p)(A)))$$

• a dependent function

  $$t:\prod_{a:P} \prod_{b:P} (a \leq_P b) \to (U(a) \hookrightarrow U(b))$$

• a dependent function

  $$q:\prod_{a:P} \prod_{b:P} \prod_{p:a \leq_P b} \prod_{A:U(a)} T(a)(A) \simeq T(b)(t(a, b)(p)(A))$$

Usually, hierarchies of Tarski universes are indexed by the type of natural numbers. A type theory may have multiple hierarchies of type universes.

Modalities and comodalities

A modal operator on a Tarski universe $(U, T)$ is just an endofunction $L:U \to U$. Given a Tarski universe, the modal unit family is a family of functions

$$\eta:\prod_{L:U \to U}\prod_{A:U} T(A) \to T(L(A))$$

and the comodal counit family is a family of functions

$$\epsilon:\prod_{L:U \to U}\prod_{A:U} T(L(A)) \to T(A)$$

Given a modal operator $L:U \to U$, $\eta(L)$ is called the modal unit of $L$ and $\epsilon(L)$ is called the comodal counit of $L$. A small type $A:U$ is $L$-modal if the function

$$\eta(L)(A):T(A) \to T(L(A))$$

is an equivalence of types, and $L$-comodal if the function

$$\epsilon(L)(A):T(L(A)) \to T(A)$$

is an equivalence of types.

A modality is…

…and a comodality is…

Reflective and coreflective Tarski subuniverses

(Section under construction see reflective subuniverse for the Russell universe variant for the time being)

 Choice operators

A choice operator on a universe is a family of functions which, given a witness that a type is inhabited, gives an element of the type. Given a Tarski universe $(U, T)$, the $U$-local choice operator is given by the following rule:

$$\frac{\Gamma \vdash U \; \mathrm{type} \quad \Gamma, X:U \vdash T \; \mathrm{type}}{\Gamma \vdash \varepsilon_U:\prod_{A:U} \vert T[A/X] \vert \to T[A/X]}$$

$U$ having a choice operator implies that $U$ satisfies axiom K or UIP. If $U$ is also univalent, then it is an h-groupoid.

Examples

The types of propositions in a type theory are univalent Tarski universes: they model a dependent type theoretic model of propositional logic with function types, product types, disjunction higher inductive types, empty type, and unit type.

Every concrete category and every concrete dagger category? is a Tarski universe, as given a concrete category or concrete dagger category $C$ by definition for each object $A:Ob(C)$ there is an h-set $El(A)$. This includes models of Mike Shulman‘s SEAR, which is a concrete power allegory, as well as ETCS with elements, which is a concrete elementary topos.

See also

For universes as a replacement for type judgments, see

• Russell universe

Regarding the general notion of types of small types, see

• type universe

Other mathematical structures and their univalent counterparts:

• preorder, partial order
• precategory, univalent category
• dagger precategory, univalent dagger category
• locally univalent bicategory, univalent bicategory

References

Historical review of Alfred Tarski‘s original notion in set theory:

• 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]

The terminology “universe à la Tarski” — and now in the context of type universes for Martin-Löf dependent type theory — is due to:

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

Further discussion:

• Martin Hofmann, Universes, section 2.3.5 in: 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, pdf, doi:10.1007/978-1-4471-0963-1]

See also:

• Zhaohui Luo, Notes on Universes in Type Theory, 2012 (pdf)

• Cesare Gallozzi, Constructive Set Theory from a Weak Tarski Universe, MSc thesis (2014) (arXiv:1411.5591)

• Egbert Rijke, Introduction to Homotopy Type Theory, Cambridge Studies in Advanced Mathematics, Cambridge University Press (pdf) (478 pages)

• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. (web, pdf)

• Egbert Rijke, Mike Shulman, Bas Spitters, Modalities in homotopy type theory (arXiv:1706.07526)