Repository logo
 

Code supporting Axioms for Modelling Cubical Type Theory in a Topos


No Thumbnail Available

Type

Software

Change log

Authors

Orton, Ian 

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

Publisher

Rights

Relationships
Supplements: