Repository logo
 

Code supporting Decomposing the Univalence Axiom

Repository URI

https://www.repository.cam.ac.uk/handle/1810/277791

Repository DOI

https://doi.org/10.17863/CAM.25036
Thumbnail Image

Files

decomposing-univalence.zip (193.59 KB)

Type

Dataset

Change log

Authors

Pitts, Andrew  ORCID logo  https://orcid.org/0000-0001-7775-3471

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)

Version

Software / Usage instructions

To be used with Agda 2.5.4

Keywords

dependent type theory, homotopy type theory, univalent type theory, univalence, cubical type theory, cubical sets

Publisher

Rights and licensing

Attribution 4.0 International (CC BY 4.0)
Except where otherwised noted, this item's license is described as Attribution 4.0 International (CC BY 4.0)
Sponsorship
EPSRC (1641673)
Orton was supported by a UK EPSRC PhD studentship, funded by grants EP/L504920/1, EP/M506485/1.

Relationships

Supplements:
https://arxiv.org/abs/1712.04890
https://doi.org/10.4230/LIPIcs.TYPES.2017.6
Is derived from:
https://doi.org/10.4230/LIPIcs.TYPES.2017.6

Collections

Research Data - Computer Science and Technology