martinescardo / Hott Uf Agda Lecture Notes
Labels
Projects that are alternatives of or similar to Hott Uf Agda Lecture Notes
Introduction to univalent foundations of mathematics with Agda
New. There is a modular version of the Agda files here at https://github.com/martinescardo/TypeTopology under the name MGS*.lagda
.
Sources to generate the lecture notes available at
https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html
Agda 2.6.1 is required. Consult the installation instructions to help you set up Agda and Emacs for the Midlands Graduate School.
-
The (literate)
*.lagda
files are used to generate thehtml
pages with the script./build
. -
This make also generates
./agda/*.agda
files usingilliterator.hs
. -
The program
agdatomd.hs
converts from.lagda
to.md
for use by the scriptfastloop
. -
This script is used for editing the notes in conjunction with
jekyll serve -watch --incremental
so that after an update it is only necessary to reload the page on the browser to view it. -
The script
slowloop
serves the same purpose, but calls Agda instead ofagdatomd
, via the scriptgeneratehtml
, so that we get syntax highlighting in the html pages. This can be very slow depending on whichlagda
file is changed. This means that after the first is reload, one is likely to see the Agda code without syntax highlighting. -
It is possible to run
./slowloop
,./fastloop
andjekyll serve
in parallel, and we do this for editing these notes. -
The loop scripts use
inotifywait
to detectlagda
file changes and trigger the appropriate conversion actions. -
The
install
action of themakefile
allows to run an additional action for particular requirements of users or environments, in a fileadditionally
, which is not distributed and is ignored bygit
. If this file doesn't exist, an empty executable file is created.