[0027] Type theory of spaces

Given a type theory $$T$$ , we introduce the type theory of spaces in $$T$$ . It is a type theory internal to $$T$$ .

Our primary interest is the type theory of toposes ([0052]), but it lacks general function types and unbounded hierarchy of universes. For convenience, the type theory of toposes is embedded into the type theory of spaces which has richer type-theoretic structures.

[002B] Notation

Let $$T$$ be a type theory. Inside $$T$$ , the type theory of spaces in $$T$$ is referred to as $\mathord {\textnormal {\textsf {Sp}}}$ .

[0029] Rule

Let $$T$$ be a type theory. We work in the type theory of spaces in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ . Then $\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))$ has the unit type, pair types, identity types, function types, inductive types, and products and coproducts indexed over any $A:\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))$ in $$T$$ . Moreover, $\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))$ is represented by a univalent universe $\mathcal {V}(\mathord {\textnormal {\textsf {succ}}}(i)):\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(\mathord {\textnormal {\textsf {succ}}}(i)))$ .

[002A] Rule

Let $$T$$ be a type theory. We work in the type theory of spaces in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ .

-A univalent universe $\mathcal {E}(i)$ in $\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))$ of étale types is constructed.
- $\mathcal {E}(i)$ is closed under the unit type, pair types, identity types, finite colimits, and coproducts indexed over any $A:\mathord {\textnormal {\textsf {Type}}}(i)$ .

[0052] Rule

Let $$T$$ be a type theory. We work in the type theory of spaces in $$T$$ .

-A univalent universe $\mathcal {T}:\mathord {\textnormal {\textsf {Type}}}(1)$ of toposes is constructed.
- $\mathcal {E}(0)$ is in $\mathcal {T}$ .
-Let $A:\mathcal {E}(0)$ . Then $$A$$ is in $\mathcal {T}$ .
- $\mathcal {T}$ is closed under the unit type, pair types, identity types, products indexed over any $A:\mathord {\textnormal {\textsf {Type}}}(0)$ , and function types whose domains are in $\mathcal {E}(0)$ .

The type theory of toposes should have a $$2$$ -categorical structure. Following [Riehl--Shulman--2017-0000], we use an interval.

[0057] Axiom

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ .

- $\mathbb {I}:\mathcal {T}$
- $\le :\mathbb {I}\rightarrow \mathbb {I}\rightarrow \lbrace X:\mathcal {T}\mid \mathord {\textnormal {\textsf {IsTrunc}}}_{-1}(X)\rbrace$
- $\mathord {\textnormal {\textsf {b}}}:\mathbb {I}$
- $\mathord {\textnormal {\textsf {t}}}:\mathbb {I}$
- $\le$ is a partial order on $\mathbb {I}$ .
- $\mathord {\textnormal {\textsf {b}}}$ is the least element.
- $\mathord {\textnormal {\textsf {t}}}$ is the greatest element.
- $\mathord {\textnormal {\textsf {b}}}$ and $\mathord {\textnormal {\textsf {t}}}$ are distinct.

$\mathbb {I}$ is different from the interval of [Riehl--Shulman--2017-0000] in that $\mathbb {I}$ is not assumed to be totally ordered.

[0058] Definition

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Let $n:\mathord {\textnormal {\textsf {Nat}}}$ . We define $\Delta \lbrack n\rbrack :\mathcal {T}$ to be the type of (non-strictly) increasing sequences in $\mathbb {I}$ of length $$n$$ . Face maps and degeneracy maps between $\Delta \lbrack n\rbrack$ 's can also be defined.

[0059] Definition

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ . We say a type $A:\mathord {\textnormal {\textsf {Type}}}(i)$ is categorical fibrant if it is local for the following functions.

- $(\mathord {\textnormal {\textsf {d}}}^{2},\mathord {\textnormal {\textsf {d}}}^{0}):\Delta \lbrack 1\rbrack \mathbin {{}_{\mathord {\textnormal {\textsf {d}}}^{0}}\mathord {+_{\mathord {\textnormal {\textsf {d}}}^{1}}}}\Delta \lbrack 1\rbrack \rightarrow \Delta \lbrack 2\rbrack$
- $\Delta \lbrack 3\rbrack \mathbin {{}_{(\mathord {\textnormal {\textsf {d}}}^{3}\circ \mathord {\textnormal {\textsf {d}}}^{1},\mathord {\textnormal {\textsf {d}}}^{0}\circ \mathord {\textnormal {\textsf {d}}}^{1})}\mathord {+_{\mathord {\textnormal {\textsf {s}}}^{0}+\mathord {\textnormal {\textsf {s}}}^{0}}}}(\Delta \lbrack 0\rbrack +\Delta \lbrack 0\rbrack )\rightarrow \Delta \lbrack 0\rbrack$
- $((\mathord {\textnormal {\textsf {s}}}^{0},\mathord {\textnormal {\textsf {s}}}^{1}),(\mathord {\textnormal {\textsf {s}}}^{1},\mathord {\textnormal {\textsf {s}}}^{0})):\Delta \lbrack 2\rbrack \mathbin {{}_{\mathord {\textnormal {\textsf {d}}}^{1}}\mathord {+_{\mathord {\textnormal {\textsf {d}}}^{1}}}}\Delta \lbrack 2\rbrack \rightarrow \Delta \lbrack 1\rbrack \times \Delta \lbrack 1\rbrack$

The locality for the first two functions in [0059] is the Segal condition and the Rezk condition, respectively. Since our interval $\mathbb {I}$ is not totally ordered, we need the locality for the third function for categorically fibrant types to be well-behaved. With this adjustment, categorically fibrant types will be essentially the same as Rezk types of [Riehl--Shulman--2017-0000].

[005B] Definition

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $A:\mathord {\textnormal {\textsf {Type}}}(i)$ , and let $B(x):\mathord {\textnormal {\textsf {Type}}}(i)$ under assumption $$x:A$$ . We say $$B$$ is a left fibration if it is right orthogonal to the function $\mathord {\textnormal {\textsf {d}}}^{1}:\Delta \lbrack 0\rbrack \rightarrow \Delta \lbrack 1\rbrack$ .

[005C] Axiom

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ .

-Every topos is categorically fibrant.
-Let $i:\mathord {\textnormal {\textsf {Level}}}$.
- - $\mathcal {E}(i)$ is categorically fibrant.
- - $(X:\mathcal {E}(i))\mapsto X$ is a left fibration.

[0038] Notation

Let $$T$$ be a type theory. We work in the type theory of spaces in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ , let $A:\mathord {\textnormal {\textsf {Type}}}(i)$ , and let $a_{1},a_{2}:A$ . We write $a_{1}\Rightarrow a_{2}:\mathord {\textnormal {\textsf {Type}}}(i)$ for the type of morphisms from $a_{1}$ to $a_{2}$ .

[005D] Axiom

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ . Then $\mathcal {E}(i)$ satisfies directed univalence. That is, for any $A,B:\mathcal {E}(i)$ , the canonical function

(A\Rightarrow B)\rightarrow (A\rightarrow B)

induced by the axiom that

(X:\mathcal {E}(i))\mapsto X

is a left fibration is an equivalence.

[004B] Proposition

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ . Then $\mathcal {E}(i)$ is closed under propositional truncation.

Proof

This is because propositional truncation is constructed by countable coproducts, finite limits, and finite colimits by the join construction [Rijke--2017-0000].