Categorical structures for type theory in univalent foundations
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 58691400
- Type
- D - Journal article
- DOI
-
10.23638/LMCS-14(3:18)2018
- Title of journal
- Logical Methods in Computer Science
- Article number
- 18
- First page
- -
- Volume
- 14
- Issue
- 3
- ISSN
- 1860-5974
- Open access status
- Compliant
- Month of publication
- September
- 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
-
2
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This work compares different categorical structures for the semantics of type theories. Its novelity is that the comparison is carried out in univalent foundations. This entails that the comparison can be done on the level of types, instead of on the level of categories (as would be necessary in set-theoretic foundations). The article shows that the comparison may depend on whether the underlying category is univalent - another new aspect of this work. This paper is a revision of a publication in CSL 2017, submitted upon invitation, and peer-reviewed according to journal standards. The article is accompanied by computer-checked proofs.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -