Questions tagged [propositions]
The propositions tag has no usage guidance.
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 ...
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 ...
(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. ...
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 ...