Repository logo
 

Code supporting Internal Universes in Models of Homotopy Type Theory


No Thumbnail Available

Type

Dataset

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

Publisher

Relationships
Supplements:
Is derived from: