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

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

\tableofcontents

In intensional type theory? , there and are typically two ways to construct a “type of small types”. One way is by Russell universes, where ahomotopy 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 using inintensional type theory? and homotopy type theory using derivations? and rules?, such as the type reflection rule

for Tarski universes. However, Furthermore, one could also study Tarski universes mathematically are usually defined as being closed under all type formers inside the type theory, regardless of the type theory.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 However, article this treats approach of defining Tarski universes as means actual that mathematical the objects, notion rather of than “Tarski as universe” something means that Tarski universes differ from type theory to type theory. By this approach, a Tarski universe in the bare intensional foundations Martin-Löf of type mathematics theory? , to which do has mathematics in.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?.

\section{Definition} 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 internalJames 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?.

We From work inside of a dependent global perspective, however, all of these types should be considered Tarski universes, since they model some notion of type theory of with small types, even though the small types in the universe do not behave as the external types in the type judgments theory and do. term And judgments that and 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 identity abelian types group , to get adependent sum types?ring , and adependent product types?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.

The Traditionally, terms Tarski universes do not have a requirement that they be univalent. However, in following the tradition started in$A:U$set theory? represent with the internal types of the universe, or equivalently, the$U$-small typespreorder . An vs internal type family or alocally $U$-smallpartial order , type and family continued in$B$intensional type theory? in and$U$homotopy type theory indexed with by a internal type$A:U$precategory is vs represented by a function$B:T(A) \to U$univalent category? ; , for we each shall term refer to Tarski universes without univalence as$a:T(A)$Tarski preuniverses , and the term Tarski universes with univalence as$B(a)$univalent Tarski universes . is a dependent type, and the term$b(a):T(B(A))$ is a dependent term or section.

Already, A we could define certain external properties a Tarski universe could have.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: