Code supporting Internal Universes in Models of Homotopy Type Theory
Licata, Daniel R
MetadataShow full item record
Pitts, A., Orton, I., Licata, D. R., & Spitters, B. (2018). Code supporting Internal Universes in Models of Homotopy Type Theory [Dataset]. https://doi.org/10.17863/CAM.22369
Agda code accompanying the paper "Internal Universes in Models of Homotopy Type Theory" by Dan R. Licata, Ian Orton, Andrew M. Pitts and Bas Spitters, in Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108, pp. 22:1-28:, 2018.
Compile with agda-flat, an extension of the Agda system by Andrea Vezzosi which implements the local type theory described in the paper; installation instructions for agda-flat are in ~/code/agda-flat/install.txt
cubical sets, dependent type theory, homotopy type theory, internal language,, modalities, univalent foundations
This record's DOI: https://doi.org/10.17863/CAM.22369