Code supporting Internal Universes in Models of Homotopy Type Theory
Repository URI
Repository DOI
Change log
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
Publisher
Rights and licensing
Except where otherwised noted, this item's license is described as Attribution 4.0 International (CC BY 4.0)