Homotopy Type Theory Tarski universe > history (Rev #4)

\tableofcontents

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

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” means that Tarski universes differ 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?. 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.

Terminology

Traditionally, Tarski universes do not have a requirement that they be univalent. However, in following the tradition started in set theory? with preorder vs partial order, and continued in intensional type theory? and homotopy type theory with precategory vs univalent category?, we shall refer to Tarski universes without univalence as Tarski preuniverses, and the Tarski universes with univalence as univalent Tarski universes.

Definition

A Tarski preuniverse 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. This is already enough to build an internal model of dependent type theory inside the Tarski preuniverse:

• 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$.

Furthermore, there are two notions of equivalence in a Tarski preuniverse $(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

A Tarski preuniverse 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

Closure under type formers

The different types in Tarski universes can be defined using the univeral properties? corresponding to the categorical semantics? of the types, rather than directly in syntax.

Empty type

The empty type inside of a Tarski preuniverse is the homotopy initial type, a small type $0:U$, such that for all $U$-small types $A:U$, the type of functions with domain $T(0)$ and codomain $T(A)$ is contractible:

A Tarski universe is weakly closed under the empty type if it has an empty type $0:U$. A Tarski universe is strongly closed under the empty type if the external type theory has an empty type $0$, and $T(0)$ is definitionally equal? to $0$. $T(0) \equiv 0$.

Unit type

Let the type of pointed types? in a Tarski preuniverse be the type

$U_*$ is also a Tarski preuniverse, and in fact is a Tarski subpreuniverse of the original Tarski universe $U$.

For each pointed type $A:U_*$ and $B:U_*$, one could construct the type of point-preserving functions with domain $T(\pi_1(A))$ and codomain $T(\pi_1(B))$:

The unit type inside of a Tarski preuniverse is the homotopy initial pointed type, a small type $(1, *):U_*$, such that for all small pointed types $A:U_*$, the type of point-preserving functions with domain $T(1)$ and codomain $T(\pi_1(A))$ is contractible:

Identity types

Dependent function types

Dependent sum types

References

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