[INCLUDE TH/speedbar.blogme] [SETFAVICON dednat4/dednat4-icon.png] [SETFAVICON IMAGES/forthsun.png] [# (defun c () (interactive) (find-blogme3-sh0-if "eev-agda")) (defun u () (interactive) (find-blogme-upload-links "eev-agda")) ;; http://angg.twu.net/eev-agda.html ;; file:///home/edrx/TH/L/eev-agda.html #] [lua: require "sandwiches-all" -- (find-blogme3 "sandwiches-all.lua") def [[ _ 2 shorthand,text R(short_:expand(shorthand), nilify(text) or shorthand) ]] short_:add [[ eev -> index.html#eev sexp-hyperlinks => (find-eev-quick-intro "3. Elisp hyperlinks") org-for-non-users -> 2021-org-for-non-users.html agda-inst => (find-es "agda" "agda-inst") using-stack -> https://plfa.github.io/GettingStarted/#install-agda-using-stack PLFA -> https://plfa.github.io/ favc -> http://angg.twu.net/LATEX/2020favorite-conventions.pdf#page=33 (favp 33 "basic-example-full") (fava "basic-example-full") martin-lof -> https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf (find-books "__logic/__logic.el" "martin-lof") selinger -> https://www.mathstat.dal.ca/~selinger/agda-lectures/ eev2021-slides -> http://angg.twu.net/LATEX/2021emacsconf.pdf (find-LATEX "2021planar-HAs-2.tex" "2._J-operators") J-ops-p10 -> http://angg.twu.net/LATEX/2021planar-HAs-2.pdf#page=10 (find-math-b-links "zhas-for-children-2" "2021planar-HAs-2") PH2 -> http://angg.twu.net/math-b.html#zhas-for-children-2 find-agdatype.el => (find-angg "AGDA/find-agdatype.el") Postulate1.agda => (find-angg "AGDA/Postulate1.agda") TestStrings.agda => (find-angg "AGDA/TestStrings.agda") TestPublic.agda => (find-angg "AGDA/TestPublic.agda") Logic1.agda => (find-angg "AGDA/Logic1.agda") Logic2.lagda.tex => (find-angg "AGDA/Logic2.lagda.tex") (find-LATEX "2022agda-logic-1.tex") (find-pdf-page "~/LATEX/2022agda-logic-1.pdf") 2022agda-logic-1.pdf -> http://angg.twu.net/LATEX/2022agda-logic-1.pdf Dednat6 -> http://angg.twu.net/dednat6/tug-slides.pdf 2022Cats3.pdf -> http://angg.twu.net/LATEX/2022Cats3.pdf 2022Cats6.pdf -> http://angg.twu.net/LATEX/2022Cats6.pdf C-c-C-n-quirk -> https://lists.chalmers.se/pipermail/agda/2022/012862.html ]] def [[ PLEFT 1 body "

$body

" ]] def [[ FIG 2 target,img "" ]] ] [SETHEADSTYLE [LUCIDA]] [htmlize [J Eev hacks for Agda] [P I 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 Org for non-users]".] [P My [_ eev]-based recipe for installing Agda on Debian is [_ agda-inst here]. [BR] It is based (IIRC!) on [_ using-stack these] instructions from [_ PLFA]. [BR] To understand how I run that, see [_ eev2021-slides these slides]. ] [P 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 [_ favc 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 "[_ martin-lof Intuitionistic Type Theory]" - for the [IT n]-th time in 20 years, for [IT n] big - and finally its canonical forms made sense to me...] [P I am now following Peter Selinger's [_ selinger lectures], and going back to PLFA occasionally.] [br] [# __ ___ _ ___ # \ \ / (_) __| | ___ ___ / _ \ # \ \ / /| |/ _` |/ _ \/ _ \ | | | | # \ V / | | (_| | __/ (_) | | |_| | # \_/ |_|\__,_|\___|\___/ \___/ #] [H4 Links to types and normal forms] [P The video in the first thumbnail below - click to play it; its title is [IT "find-agdatype and find-agdatype2 - two eev hacks for inspecting types of expressions in Agda"] - explains the first non-trivial eev hack that I wrote for Agda. The second thumbnail below is a screenshot - click to enlarge it - that shows a similar hack, called "find-agdanorm", that I wrote some time after recording the video.] [PLEFT [FIG http://angg.twu.net/eev-videos/2021-find-agdatype.mp4 IMAGES/2021-find-agdatype-small.png] [FIG IMAGES/2022-find-agdanorm.png IMAGES/2022-find-agdanorm-small.png] ] [P In short: we can put [_ sexp-hyperlinks sexp hyperlinks] like these in comments in an Agda file:] [BE' -- (find-agdatype "expr1") -- (find-agdanorm "expr2") ] [P Following the link (find-agdatype "[IT expr1]") shows the type of [IT expr1] in the window at the right, and following the link (find-agdanorm "[IT expr2]") shows the result of normalizing [IT expr2]. The elisp code for find-agdatype and find-agdanorm is in [_ find-agdatype.el]. Here are some Agda files in which I used find-agdatype and find-agdanorm: [_ Postulate1.agda], [_ TestStrings.agda], [_ TestPublic.agda].] [# - and [_ C-c-C-n-quirk here] is an e-mail that I sent to the mailing list about a quirk. #] [br] [H4 Natural Deduction] [P One 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 [_ 2022agda-logic-1.pdf here].] [PLEFT [FIG IMAGES/2022-agda-logic-simple-1-2.png IMAGES/2022-agda-logic-simple-1-2-small.png] [FIG IMAGES/2022-agda-logic-distrib-1.png IMAGES/2022-agda-logic-distrib-1-small.png] ] [P Actually I first attempted to translate [_ J-ops-p10 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.] [P 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 [_ 2022Cats3.pdf 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. =/] [br] [H4 Categories] [P I am trying to formalize [_ favc this] skeleton of a proof of the Yoneda Lemma in Agda. My current attempt is [_ 2022Cats6.pdf 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 [_ 2022Cats3.pdf 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!!!] ] [# # Local Variables: # coding: raw-text-unix # modes: (fundamental-mode blogme-mode) # End: #]