Agda code accompanying PhD thesis: Cubical Models of Homotopy Type Theory -- An Internal Approach

Agda development covering many of the proofs in my PhD thesis. Many of these proofs were produced by me over the course of my PhD, although some are the result of collaboration with Andrew Pitts, Daniel Licata and Bas Spitters. All the files are contained inside a single .zip file and include a README file which is reproduced below: Agda code accompanying PhD thesis: Cubical Models of Homotopy Type Theory -- An Internal Approach" by Ian Orton. This dataset was finalised in November 2018 by Ian Orton, who was a PhD student at the University of Cambridge the time. He may be contacted at [e-mail]. This dataset consists of numerous computerised proofs which can be checked with the proof assistant Agda. The file `root.agda` describes how these proofs are structured and what is contained in each file. The structure of the files is designed to match the structure of the PhD thesis. These files were put together by Ian Orton, but build on work done in collaboration with Andrew Pitts, Daniel Licata and Bas Spitters. The files which are imported by `chapter7.agda` require an (at the time of writing) experimental branch of Agda known as Agda-flat which can be installed using the following commands: git clone https://github.com/agda/agda cd agda git checkout flat cabal update cabal install --program-suffix=-flat The file `root.agda` has been checked using the following versions of Agda, with the approximate times taken to check the entire file: - Agda 2.5.4 (with chapter7 commented out) in ~ 1 min - Agda-flat 2.6.0-1f943c9 (the whole file) in ~ 3 mins This data is released under the CC BY licence and everyone is free to use, share and modify it.