[002V] Cross-theory axioms

We have introduced the type theory of spaces and the type theory of sheaves both of which are internal to a base type theory. Now we introduce some axioms that strongly tie these type theories together.

The first axiom ([002S]) is between the base type theory and the type theory of spaces. It asserts that types in the base type theory are equivalent to étale spaces.

[002S] Axiom

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

-The function $\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}:\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}(\mathcal {E}(i))\rightarrow \mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))$ factors through $\mathcal {U}(i)$ .
-Let $A:\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}(\mathcal {E}(i))$ . Then the counit of the adjunction $\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sp}}}}\dashv \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}$ at $$A$$ is an equivalence.
-Let $A:\mathcal {U}(i)$ . Then the unit of the adjunction $\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sp}}}}\dashv \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}$ at $$A$$ is an equivalence.

In short, the adjunction

\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sp}}}}\dashv \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}

restricts to an equivalence

\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}(\mathcal {E}(i))\simeq \mathcal {U}(i)

of categories.

The second axiom ([005E]) is between the base type theory and the type theory of sheaves on a topos. It asserts that a topos is to some extent determined by the category of sheaves on it.

[005E] Axiom

Let $$T$$ be a base type theory. We work in $$T$$ . Let $$X$$ be a topos. Suppose that the functor

\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}:\mathcal {U}(0)\rightarrow \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathcal {U}(0))

is an equivalence of categories. Then

\(X\)

is contractible.

[002S] and [005E] are “too global”. For [002S], what we really want is that étale type families on a topos $$X$$ are equivalent to global types in $\mathord {\textnormal {\textsf {Sh}}}(X)$ . For [005E], what we really want is that a morphism between topose is an equivalence whenever its inverse image functor (introduced later in [003I]) is an equivalence of categories. Both are addressed by the third axiom ([002Y]) which relates type theories of spaces in different base type theories. It asserts that spaces over a topos $$X$$ are equivalent to spaces in $\mathord {\textnormal {\textsf {Sh}}}(X)$ . By this axiom, relative stuff (e.g. type family on a topos $$X$$ ) is reduced to global stuff (e.g. global type) in $\mathord {\textnormal {\textsf {Sh}}}(X)$ . Remember that $\mathord {\textnormal {\textsf {Sh}}}(X)$ is again a base type theory so [002S] and [005E] are also assumed there.

[002W] Exercise

Let $$T$$ be a base type theory, and let $$X$$ be a topos in $$T$$ . We work in $\mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {Sp}}})$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ .

- $\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))$ has products and coproducts indexed over any $A:\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))$ in $$T$$ .
- $\mathcal {E}(i)$ is closed under coproducts indexed over any $A:\mathord {\textnormal {\textsf {Type}}}(i)$ in $$T$$ .

[002X] Notation

Let $$T$$ be a base type theory. We work in $$T$$ . Let $$X$$ be a topos. By [002W], we have a translation

\mathord {\textnormal {\textsf {Sp}}}\rightarrow \mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {Sp}}})

that preserves all the structures of the type theory of spaces. We refer to this translation as

Z\mapsto {X}^{*}(Z)

[002U] Notation

Let $T_{1}$ be a type theory and let $T_{2}$ be a type theory internal to $T_{1}$ . We work in $T_{1}$ . Let $i:\mathord {\textnormal {\textsf {Level}}}$ and let $A:\mathord {\textnormal {\textsf {D}}}_{T_{2}}({}\vdash \mathord {\textnormal {\textsf {Type}}}(i))$ . Then $T_{2}/(x:A)$ denotes the slice type theory over $$A$$ . More precisely, it is described as follows.

-Let $j:\mathord {\textnormal {\textsf {Level}}}$ . Then $\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}/(x:A)}(j)$ is the full subcategory of $\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(j)/(x:A)$ spanned by the display maps over $$x:A$$ of level $$j$$ .
-The types of types and elements are created by the domain projection $\mathord {\textnormal {\textsf {Ctx}}}_{T_{2}/(x:A)}(j)\rightarrow \mathord {\textnormal {\textsf {Ctx}}}_{T_{2}}(\_)$ .

[002Y] Axiom

Let $$T$$ be a base type theory. We work in $$T$$ . Let $$X$$ be a topos.

- $\mathord {\textnormal {\textsf {w}}}_{X}:\mathord {\textnormal {\textsf {D}}}_{\mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {Sp}}})}({}\vdash {X}^{*}(X))$ .
-The translation $\mathord {\textnormal {\textsf {Sp}}}/(x:X)\rightarrow \mathord {\textnormal {\textsf {Glob}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}(\mathord {\textnormal {\textsf {Sp}}})$ defined by $Z\mapsto ({X}^{*}(Z))[x\mathrel {:\equiv }\mathord {\textnormal {\textsf {w}}}_{X}]$ is an equivalence.