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.
M. Bezem, T. Coquand, P. Dybjer, and M. Escardó. TYPES, volume 269 of LIPIcs, page 13:1-13:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2022)