Code supporting Internal Universes in Models of Homotopy Type Theory
Repository URI
Repository DOI
Change log
Authors
Pitts, AM
Orton, Ian
Licata, Daniel R
Spitters, Bas
Description
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.
Version
Software / Usage instructions
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
Keywords
cubical sets, dependent type theory, homotopy type theory, internal language,, modalities, univalent foundations