## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorMike Shulman
• CommentTimeDec 1st 2016

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

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeDec 1st 2016

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

1. added a section on the definition of types of propositions

Anonymous

2. added rules for the type of all propositions

Anonymous

• CommentRowNumber5.
• CommentAuthorGuest
• CommentTimeOct 17th 2022

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

• CommentRowNumber6.
• CommentAuthorChristian Sattler
• CommentTimeOct 17th 2022
• (edited Oct 17th 2022)

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.

3. added section on the type of all decidable propositions, or the type of booleans

Anonymous

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

Anonymouse

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeAug 2nd 2023

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

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeAug 2nd 2023

5. 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

6. 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.