Internal Universes in Models of Homotopy Type Theory
- Submitting institution
-
University of Cambridge
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1927
- Type
- E - Conference contribution
- DOI
-
10.4230/LIPIcs.FSCD.2018.22
- Title of conference / published proceedings
- Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108
- First page
- 22:1
- Volume
- 108
- Issue
- -
- ISSN
- 1868-8969
- Open access status
- Compliant
- Month of publication
- July
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This breakthrough paper completes the axiomatic approach to cubical models of homotopy type theory initiated by the second and third authors. It does so by showing how to construct universes, starting from the assumption that the interval is "tiny", a property that the interval in cubical sets does indeed have. The results are formalized using a modal extension to the Agda theorem-proving system that has subsequently been adopted by official releases of Agda.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -