Code supporting Axioms for Modelling Cubical Type Theory in a Topos
Repository URI
Repository DOI
Change log
Authors
Orton, Ian
Pitts, Andrew 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, "Axioms for Modelling Cubical Type Theory in a Topos" (Journal of Logical Methods in Computer Science, Special Issue for CSL2016)
Version
1
Software / Usage instructions
Known to compile using Agda version 2.5.3
Keywords
models of dependent type theory,, homotopy type theory, cubical sets, cubical type theory, topos, univalence