Homotopy Type Theory Tarski universe > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

\tableofcontents

\section{Idea}

Tarski In universes are the internal models ofdependent type theoryintensional type theory? , inside there are typically two ways to construct a “type of small types”. One way is by Russell universes, where adependent type theoryterm? . They are useful in that one could defineinductive types?$A:U$ and of ahigher inductive typesuniverse type? directly through theuniversal properties?$U$ of is such literally types, a rather than through the formation, introduction, elimination, computation, and uniqueness rules of such types.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

A Tarski universe is externally univalent if for all terms $A:U$ and $B:U$ the function $\mathrm{transport}^T(A, B)$ is an equivalence of types

Similarly, a Tarski universe satisfies the external axiom K? if for all terms $A:U$ the type $T(A)$ 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 $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$

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

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, pdf)

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