M. Escardó. (2019)cite arxiv:1911.00580Comment: 211 pages, extended version of Midlands Graduate School course (2019), includes Agda-verified mathematics. Sources available at github (as explained in the pdf file), but not in LaTeX, last revised September 2022.