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 ...
- 11k
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 ...
- 5,908
6
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 ...
- 5,908
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 ...
- 4,344
5
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
...
- 301
5
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). ...
- 10.2k
5
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$)...
- 311
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: ...
- 2,242
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 $\...
- 311
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 ...
- 3,270
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 *...
- 5,908
2
votes
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:
...
- 10.2k
1
vote
Which natural deduction rule is this "application"?
To further complement answers, here is a toy experiment shallowly embedding (a little fragment of propositional) natural deduction in Coq's interactive proof mode. -- This quite sums up my ...
- 567
1
vote
Accepted
Which natural deduction rule is this "application"?
Complementing Andrej's answer, here is the corresponding proof in natural deduction:
...
- 126
Only top scored, non community-wiki answers of a minimum length are eligible