Formal proofs supporting the thesis "Domain Theory in Constructive and Predicative Univalent Foundations"

This deposit consists of formal proofs in Agda and Coq, together with the software libraries that these proofs depend on. Moreover, the HTML renderings of these proofs, generated for presentation and reading, are also included. The readme file has additional details describing each file.