## Eev hacks for AgdaI am trying to learn Agda. My brain seems to be wired in an atypical way, so I am trying to create notes, examples, and tests in a format that works well for me. I'm doing that for Org Mode too: see the video "Org for non-users". My eev-based recipe for installing Agda on Debian is here.
I gave up trying to follow PLFA because I was getting stuck all the
time on ideas that it pretends that are obvious... for example, its
first chapters use only inductive types, but 1) I'm not very
familiar with them, 2) my motivation for learning Agda was to
formalize things like this, that use non-inductive types.
But in one of these times in which I was stuck I tried to reread
Martin-Löf's "Intuitionistic Type Theory" - for the
I am now following Peter Selinger's lectures, and going back to PLFA occasionally. ## Links to types and normal formsThe video in the first thumbnail below - click to play it; its
title is In short: we can put sexp hyperlinks like these in comments in an Agda file:
Following the link (find-agdatype " ## Natural DeductionOne exercise that I did was to translate some proofs in Natural Deduction to Agda - see the screenshots below. My code in Agda is in Logic1.agda and Logic2.lagda.tex, and the PDF that I used in the screenshots below is here. Actually I first attempted to translate these proofs from PH2 to Agda, but I found that they were far above my level - and still are! - so I tried something more basic. Some time after writing the proofs above I found a way to use Dednat6 in .lagda.tex files. The code still needs to be cleaned up, but here's an example of output... that, by the way, also shows how I am still struggling to write proofs of chains of equalities in a human-readable way. =/ ## CategoriesI am trying to formalize this skeleton of a proof of the Yoneda Lemma in Agda. My current attempt is here; it is very incomplete, it needs diagrams, most of its symbols need to be renamed to match the diagrams, I haven't yet translated the proofs of functoriality from an older version to that one, etc, etc, etc... but I only learned how to write the composition in the category catB as B.o in 2022feb01! Work in progress!!! |