Skip to content
Lecture notes on univalent foundations of mathematics with Agda
Branch: master
Clone or download
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
_layouts minor changes Apr 2, 2019
agda fix typo in exercise Apr 18, 2019
css css Mar 29, 2019
.gitignore readd Mar 29, 2019
HoTT-UF-Agda.lagda get rid of hyphen Apr 19, 2019
INSTALL.md Set default font for Emacs to fix unicode issues Apr 18, 2019
LICENSE Initial commit Mar 20, 2019
README.md Merge branch 'master' of github.com:martinescardo/HoTT-UF-Agda-Lectur… Apr 15, 2019
Universes.lagda
_config.yml moved from repository TypeTopology Mar 20, 2019
agdatomd.hs move to monolitic agda file so that pdf file has internal links Mar 29, 2019
build
buildlocally
buildloop move to monolitic agda file so that pdf file has internal links Mar 29, 2019
fastloop move to monolitic agda file so that pdf file has internal links Mar 29, 2019
generatehtml move to monolitic agda file so that pdf file has internal links Mar 29, 2019
generatepdf
illiterate move to monolitic agda file so that pdf file has internal links Mar 29, 2019
illiterator.hs
replace move to monolitic agda file so that pdf file has internal links Mar 29, 2019
slowloop move to monolitic agda file so that pdf file has internal links Mar 29, 2019

README.md

Introduction to univalent foundations of mathematics with Agda

Sources and scripts 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.0 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 the html pages with the script ./build.

  • This script also generates (illiterate) ./agda/*.agda files using the script illiterate, which calls the Haskell program illiterator.hs.

  • The program agdatomd.hs converts from .lagda to .md for use by the script fastloop.

  • This script is used for editing the notes in conjunction with jekyll serve so that after an update it is only necessary to reload the page on the brouwser to view it.

  • The script slowloop serves the same purpose, but calls Agda instead of agdatomd, via the script generatehtml, to that we get syntax highlighting in the html pages. This can be very slow depending on which lagda file is changed. This means that after the first reload, one is likely to see the Agda code without syntax highlighting.

  • It is possible to run ./slowloop, ./fastloop and jekyll serve in parallel, and we do this for editing these notes.

  • The loop scripts use inotifywait to detect lagda file changes and trigger the appropriate conversion actions.

You can’t perform that action at this time.