Questions tagged [propositions]
The propositions tag has no usage guidance.
4
questions
2
votes
1
answer
123
views
Definitional vs propositional equality
Theorem Proving in Lean highlights a distinction between definitional and propositional equality when creating recursive functions:
The example above shows that the defining equations for ...
- 263
8
votes
3
answers
214
views
When is hProp equivalent to the subobject classifier?
In the definition of an elementary topos, the "object of propositions" $\Omega$ is axiomatized by the universal property of a subobject classifier.
In homotopy type theory, we instead start ...
- 270
2
votes
1
answer
254
views
(In Lean), why cannot structural recursion on propositions be used?
Update: this has been fixed and the fix is available in the latest nightly release of Lean 4.
In Lean 4, structural recursion on functions on types is no issue.
...
- 247
6
votes
1
answer
190
views
Can we completely erase propositions in the type checker?
Related question on semantic side: How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken?
Suppose we have an impredicative universe of ...
- 5,424