Code supporting Axioms for Modelling Cubical Type Theory in a Topos
Repository URI
Repository DOI
Change log
Authors
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
Publisher
Rights and licensing
Except where otherwised noted, this item's license is described as CC-BY