Univalent categories and the Rezk completion
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 48271279
- Type
- D - Journal article
- DOI
-
10.1017/S0960129514000486
- Title of journal
- Mathematical Structures in Computer Science
- Article number
- -
- First page
- 1010
- Volume
- 25
- Issue
- 5
- ISSN
- 0960-1295
- Open access status
- Out of scope for open access requirements
- Month of publication
- January
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
https://static.cambridge.org/content/id/urn:cambridge.org:id:article:S0960129514000486/resource/name/S0960129514000486sup001.tar
- 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
-
2
- Research group(s)
-
-
- Citation count
- 13
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Univalent foundations were designed by Fields Medalist Voevodsky as a foundation of mathematics in which constructions on objects can be transported along equivalence of structures. This paper is significant because it fulfills Voevodsky’s vision for the prototypical case of categories. The notion of univalent category introduced here has become the standard. Our framework has served as a prototype, and others have developed analogous results for other higher-dimensional structures ("Univalent Higher Categories via Complete Semi-Segal Types" (POPL 2018), "A Higher Structure Identity Principle"). The results are verified in the computer proof assistant Coq.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
