Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Is there any point to having both type of propositions and Prop? The analogous page-name Type is a redirect to type of types.
Not sure why this happened. I have merged the two entries now.
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
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.
Incidentally, I see that this entry is lacking any reference to subtype.
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
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.
1 to 12 of 12