2026-01-12 15:22:32 +00:00
|
|
|
|
# Installing Agda
|
|
|
|
|
|
|
|
|
|
|
|
I added these lines to my configuration.nixos to get a workable Agda installation:
|
|
|
|
|
|
|
|
|
|
|
|
(agda.withPackages (p: [ p.standard-library ]))
|
|
|
|
|
|
|
|
|
|
|
|
but there were a few issues, so I removed that and installed with
|
|
|
|
|
|
cabal update
|
|
|
|
|
|
cabal install Agda
|
|
|
|
|
|
which seemed to work nicely after some hackery with zlib, and installing the standard libraries.
|
|
|
|
|
|
|
|
|
|
|
|
# Owen's Geolog definitions
|
|
|
|
|
|
|
|
|
|
|
|
Owen.agda : Definitions fom Owen's first two lectures about Geolog.
|
|
|
|
|
|
|
|
|
|
|
|
These set up the basic machinery for contexts (signatures), theories and interpolation.
|
|
|
|
|
|
|
|
|
|
|
|
Compile with:
|
|
|
|
|
|
agda -c --no-main Owen.agda
|
|
|
|
|
|
|
|
|
|
|
|
# HoTT definitions from Martin Escardo's book "Univalent Foundations" https://arxiv.org/pdf/1911.00580
|
|
|
|
|
|
|
|
|
|
|
|
agda -c --no-main MLTT/Universe.agda
|
|
|
|
|
|
|
|
|
|
|
|
Escardo defines everything from the ground up with his own concepts of sets, universes etc.,
|
|
|
|
|
|
independently of the standard library.
|
|
|
|
|
|
|
2026-01-12 18:01:36 +00:00
|
|
|
|
Got as far as the definition of 𝟙-induction for a single-valued type 𝟙.
|
|
|
|
|
|
The sources (in more consistent versions than in the notes) are here:
|
|
|
|
|
|
https://github.com/martinescardo/HoTT-UF-Agda-Lecture-Notes
|
|
|
|
|
|
|
