[001T] Topical type theory

We introduce the topical type theory. It consists of a bunch of type theories related to each other. Those type theories fall into three categories: base type theory; type theory of spaces; type theory of sheaves. We begin with a base type theory \(T\). The type theory of spaces in \(T\) is a type theory internal to \(T\). Toposes in \(T\) are certain special types in the type theory of spaces in \(T\). For every topos \(X\) in \(T\), the type theory of sheaves on \(X\) is internal to \(T\).

A base type theory ([0022]) is a univalent type theory with all standard type constructors. This is thought of as a metatheory of topos theory.

The type theory of spaces in \(T\) ([0027]) is a type theory that has universes of étale types. Although it has standard type constructors for convenience, the most relevant ones are limits, colimits of étale types, and exponentials by étale types.

The type theory of sheaves on \(X\) ([0028]) is again a base type theory. This means that we have the topical type theory whose base type theory is the type theory of sheaves on \(X\). So, the topical type theory is somehow a coinductive family of type theories.

We need some axioms to relate these kinds of type theories. One axiom asserts that a base type theory is embedded into the type theory of spaces in it, and its image is the étale types. Another axiom asserts that a topos is determined by the category of sheaves on it. Yet another axiom asserts that the type theory of spaces in the type theory of sheaves on a topos \(X\) is equivalent to the type theory of spaces over \(X\). These axioms are assumed in all base type theories, so they are more powerful than they look.

The presentation of the topical type theory here is rather informal. A formal definition of the topical type theory and its semantics have not been developed yet.