Skip to main content

New answers tagged

3 votes
Accepted

How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

The surjective pairing rule is really just as written there by Wadler. Andrej's interpretation is correct. What the equation ...
Li-yao Xia's user avatar
1 vote

How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

Is this not just confusion about notation? If the notation (X, y) is used to signify the introduction rule for then it does ...
Andrej Bauer's user avatar
  • 29.2k

Top 50 recent answers are included