Code supporting Decomposing the Univalence Axiom
Repository URI
Repository DOI
Change log
Authors
Orton, RI
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
Sponsorship
EPSRC (1641673)
Orton was supported by a UK EPSRC PhD studentship, funded by grants EP/L504920/1, EP/M506485/1.