Synthetic topos theory
[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 \).