Code supporting Decomposing the Univalence Axiom
Description
This Agda code contains a formal development of some of the proofs in the paper Ian Orton and Andrew M. Pitts, "Decomposing the Univalence Axiom", 3rd International Conference on Types for Proofs and Programs (TYPES 2017)
Format
To be used with Agda 2.5.4
Keywords
dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets
Relationships
Sponsorship
Orton was supported by a UK EPSRC PhD studentship, funded by grants EP/L504920/1, EP/M506485/1.
Funder references
EPSRC (1641673)
Identifiers
This record's DOI: https://doi.org/10.17863/CAM.25036
Rights
Attribution 4.0 International, Attribution 4.0 International, Attribution 4.0 International, Attribution 4.0 International, Attribution 4.0 International, Attribution 4.0 International, Attribution 4.0 International, Attribution 4.0 International, Attribution 4.0 International
Licence URL: http://creativecommons.org/licenses/by/4.0/http://creativecommons.org/licenses/by/4.0/http://creativecommons.org/licenses/by/4.0/http://creativecommons.org/licenses/by/4.0/http://creativecommons.org/licenses/by/4.0/http://creativecommons.org/licenses/by/4.0/http://creativecommons.org/licenses/by/4.0/http://creativecommons.org/licenses/by/4.0/http://creativecommons.org/licenses/by/4.0/
Except where otherwise noted, this item's licence is described as Attribution 4.0 International