More reorganizing of this page - moved subsection titled “the empty proposition and falsehood” under a new section “Properties” and showed how to directly construct the empty type from the type of propositions and dependent function types, and how to show that the empty type is a proposition.

]]>Moved the sections on the “type of decidable propositions” and “type of booleans” from this article over to boolean domain, since those definitions are really talking about defining the boolean domain

]]>added a sentence to the Idea-section which cross-links back to *subtype*.

Incidentally, I see that this entry is lacking any reference to *subtype*.

Added rules for the type of all propositions as a Russell universe.

Anonymouse

]]>added section on the type of all decidable propositions, or the type of booleans

Anonymous

]]>That’s effectively being done already when you say every proposition is classified by $\Omega$. To derive your proposed rule, consider the proposition in context $\Gamma.(b : B)$ of preimages of $b$ under $i$.

Side note: we don’t currently have models of the type of all propositions (as currently defined, with a meta-equality $\mathsf{El}(A_\Omega) \equiv A$) in HoTT.

]]>Should be possible to define the type of propositions via the universal property of the subobject classifier, something like

$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \Omega \; \mathrm{type}}$ $\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{true}:\Omega}$ $\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type} \quad \Gamma \vdash i:A \hookrightarrow B}{\Gamma \vdash \chi_B:B \to \Omega}$et cetera

]]>added rules for the type of all propositions

Anonymous

]]>added a section on the definition of types of propositions

Anonymous

]]>Not sure why this happened. I have merged the two entries now.

]]>Is there any point to having both type of propositions and Prop? The analogous page-name Type is a redirect to type of types.

]]>