[003V] The topos of types

We take a close look at the simplest and most important topos, the topos of types.

[003W] Definition

Let $$T$$ be a base type theory. We work in $$T$$ . We define the topos of types $\mathcal {E}$ to be $\mathcal {E}(0)$ .

In classical topos theory, the topos of types is also called the object classifier, and its category of sheaves is the category of presheaves on the free lex category over one object. In particular, every object in the free lex category over one object induces an essential point of the topos of types. We construct those essential points synthetically.

[003X] Proposition

Let $$T$$ be a base type theory. We work in the type theory of spaces $$T$$ . Then the point $\mathord {\textnormal {\textsf {1}}}:\mathcal {E}$ is coétale.

Proof

For any $X:\mathcal {E}$ , we have $(\mathord {\textnormal {\textsf {1}}}\Rightarrow X)\simeq X$ , and thus $\mathord {\textnormal {\textsf {1}}}\Rightarrow X$ is in $\mathcal {E}(0)$ .

[003Y] Proposition

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Let $$X$$ be a topos. Then coétale points of $$X$$ are closed under finite colimits that exist in $$X$$ .

Proof

This is because $\mathcal {E}(0)$ is closed under finite limits.

[003Z] Definition

Let $$T$$ be a base type theory. We work in type theory of spaces in $$T$$ . We say a point of $\mathcal {E}$ is finitely presented if it is constructed from $\mathord {\textnormal {\textsf {1}}}$ by finite colimits.

[0040] Proposition

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Then every finitely presented point of $\mathcal {E}$ is coétale.

Proof

By [003Y] and [003Z].

[0041] Proposition

Let $$T$$ be a base type theory. We work in $$T$$ . Then every finitely presented point of $\mathcal {E}$ is essential.

Proof

By [003T] and [0040].