Skip to main content
9 votes

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 ...
Andrej Bauer's user avatar
  • 9,593
7 votes
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 ...
Meven Lennon-Bertrand's user avatar
6 votes

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 ...
Trebor's user avatar
  • 4,015
4 votes
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 ...
tarzh's user avatar
  • 291
4 votes
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 ...
Mike Shulman's user avatar
  • 3,190
4 votes

When is hProp equivalent to the subobject classifier?

The precise answer is going to depend on exactly what formulation you are using of the two definitions, but there are a few things to be aware of in any case. For any universe $U$ the projection map $\...
aws's user avatar
  • 301
4 votes
Accepted

(In Lean), why cannot structural recursion on propositions be used?

TL;DR: There is no logical reason I see that Lean can't do this. It just seems like it is not implemented (and possibly it will be implemented in the future as this comment on Zulip suggests). ...
Jason Rute's user avatar
  • 8,960
4 votes

In a dependently typed language, are all types statements?

You can look at the ways to define types as ways to define propositions. One simple definition of Nat is its Boehm-Berarducci encoding: ...
Li-yao Xia's user avatar
  • 1,857
4 votes

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

It's consistent to interpret the type of strict propositions as the type of double negation stable propositions (or more generally as $j$-stable propositions for any given Lawvere-Tierney topology $j$)...
aws's user avatar
  • 301
4 votes

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 ...
Meven Lennon-Bertrand's user avatar
3 votes
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 *...
Meven Lennon-Bertrand's user avatar
2 votes
Accepted

How to combine the PROP of a list of PROP in lean 4?

If you are willing to use Mathlib, you can use List.Forall: ...
Jason Rute's user avatar
  • 8,960

Only top scored, non community-wiki answers of a minimum length are eligible