Tag Info

Hot answers tagged propositions

When is hProp equivalent to the subobject classifier?

$\newcommand{\Type}{\mathsf{Type}}$ $\newcommand{\hProp}{\mathsf{hProp}}$ $\newcommand{\isEmbedding}{\mathsf{isEmbedding}}$ Recall from HoTT book Definition 4.6.1 that $f : A \to B$ is an embedding ...
• 9,593
Accepted

Can we completely erase propositions in the type checker?

The ability to have this kind of "erasure" for propositions is indeed one of the major arguments in favour of having a proper sort of strict propositions (see e.g. Section 9.3 of this ...
• 5,186

In a dependently typed language, are all types statements?

To make the basics clear: languages don't mean anything before you assign them meanings manually, and you can interpret the same language different ways. So if you want to interpret a dependent type ...
• 4,015
Accepted

Definitional vs propositional equality

My understanding is that two terms are definitionally equal if they reduce to the same term via partial evaluation. With add defined as ...
• 291
Accepted

When is hProp equivalent to the subobject classifier?

In Proposition 11.3 of All (∞,1)-toposes have strict univalent universes I proved that the interpretation of type theory in any $(\infty,1)$-topos — with the universes interpreted by object ...
• 3,190

• 301

Can strict propositions (Rocq's SProp, Agda's Prop) be used to show termination?

Sadly, a big issue of strict propositions is that in their current form they validate very little choice principles. For instance, I don't think that your example is provable. Indeed, Pujet and ...
• 5,186
Accepted

Negating universal/existential quantifier in type theory, propositions on elements of the empty type

The universal/existential quantifiers and their negations In type theory, negation is defined as a shortcut for "implying falsity", in other words ~ P is *...
• 5,186