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 \).
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 \).