Questions tagged [propositions]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2 votes
1 answer

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

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

(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. ...
6 votes
1 answer

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