[004M] The topos of propositions

[004N] Definition

Let $$T$$ be a base type theory. We work in $$T$$ . We define the topos of propositions $\Omega$ to be $\lbrace X:\mathcal {E}\mid \mathord {\textnormal {\textsf {IsTrunc}}}_{-1}(X)\rbrace$ .

In classical topos theory, the topos of propositions is also called the Sierpinski topos, and its category of sheaves is the arrow category of the category of types.

[004O] Exercise

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Then the point $\top :\Omega$ is coétale.

[004P] Proposition

Let $$T$$ be a base type theory. We work in the type theory of spaces in $$T$$ . Then the point $\bot :\Omega$ is coétale.

Proof

By [003Y].

[004Q] Exercise

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

\mathcal {S}(\Omega ,i)\rightarrow \mathord {\textnormal {\textsf {G}}}_{1}\pitchfork \mathcal {U}(i)

induced by the morphism

\bot \rightarrow \top

\Omega

is an equivalence.