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

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

\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

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)