Guarded Cubical Type Theory

This paper improves the treatment of equality in guarded dependent type theory (\(\mathsf {GDTT}\)), by combining it with cubical type theory (\(\mathsf {CTT}\)). \(\mathsf {GDTT}\) is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement \(\mathsf {GDTT}\) with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. \(\mathsf {CTT}\) is a variation of Martin–Löf type theory in which the identity type is replaced by abstract paths between terms. \(\mathsf {CTT}\) provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory (\(\mathsf {GCTT}\)), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of \(\mathsf {CTT}\) as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that \(\mathsf {CTT}\) can be given semantics in presheaves on \(\mathcal {C}\times \mathbb {D}\), where \(\mathcal {C}\) is the cube category, and \(\mathbb {D}\) is any small category with an initial object. We then show that the category of presheaves on \(\mathcal {C}\times \omega \) provides semantics for \(\mathsf {GCTT}\).