Posts in the category Formalization
Jacques Carette asked on Twitter for a refence to the fact that countable choice holds in setoids. I then spent a day formalizing facts about the axiom of choice in setoids in Agda. I noticed something interesting that is worth blogging about.→ continue reading (4 comments)
- Keynote presentation, viewable online in your browser. Turn on the speaker notes by clicking on the rectangular icon in the top-left corner.
- Slides with speaker notes (PDF). Unfortunately, Keynote does not make the hyperlinks active when exporting PDF.
- Video recording of the talk.
- we developed our mathematics constructively,
- we formalized our mathematics in Martin-Löf type theory, in Agda notation,
- we pressed a button, and
- after a few seconds we saw the integer we expected in front of us.
Well, it was a few seconds for the computer in steps (3)-(4), but three years for us in steps (1)-(2).→ continue reading