Axioms for modelling cubical type theory in a Topos
- Submitting institution
-
University of Cambridge
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1860
- Type
- E - Conference contribution
- DOI
-
10.4230/LIPIcs.CSL.2016.24
- Title of conference / published proceedings
- Leibniz International Proceedings in Informatics, LIPIcs
- First page
- 1
- Volume
- 62
- Issue
- 24
- ISSN
- 1868-8969
- Open access status
- Compliant
- Month of publication
- August
- Year of publication
- 2016
- 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
-
1
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Full version of a conference article in the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). The authors were invited to submit a full version of the work by the editors of a special edition of the journal LMCS. The first author was the second author's PhD student. The paper's axiomatic treatment of many aspects of Cohen-Coquand-Huber-Mortberg "cubical" model of univalence has been very influential, having been used and adapted by several research groups working in the new field of homotopy type theory (such as Birkedal's in Aarhus and Harper's in CMU).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -