Guarded Cubical Type Theory
Tóm tắt
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}$$
.
Tài liệu tham khảo
Abel, A., Vezzosi, A.: A formalized proof of strong normalization for guarded recursive types. In: APLAS, pp. 140–158 (2014)
Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now! In: PLPV, pp. 57–68 (2007)
Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: ICFP, pp. 197–208 (2013)
Birkedal, L., Rasmus, E.M.: Intensional type theory with guarded recursive types qua fixed points on universes. In: LICS, pp. 213–222 (2013)
Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: POPL, pp. 119–132 (2011)
Birkedal, L., Møgelberg, R.E., Schwinghammer, J., Støvring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. In: LMCS, vol. 8, no. 4 (2012)
Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H.B., Spitters, B., Vezzosi, A.: Guarded cubical type theory: path equality for guarded recursion. In: CSL, vol. 3, p. 37 (2016)
Birkhoff, G.: Rings of sets. Duke Math. J. 3(3), 443–54 (1937)
Bizjak, A., Møgelberg, R.E.: A model of guarded recursion with clock synchronisation. In: MFPS, pp. 83–101 (2015)
Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded dependent type theory with coinductive types. In: FoSSaCS, pp. 20–35 (2016)
Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types. Log. Methods Comput. Sci. (2016). https://doi.org/10.1007/978-3-662-46678-0_26
Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom. In: Post-proceedings of the 21st International Conference on Types for Proofs and Programs, TYPES 2015 (2016)
Coquand, T.: Internal version of the uniform Kan filling condition. http://www.cse.chalmers.se/~coquand/shape.pdf (2015). Accessed 13 June 2018
Cornish, W., Fowler, P.: Coproducts of de Morgan algebras. Bull. Aust. Math. Soc. 16(1), 1–13 (1977)
Dybjer, P.: Internal type theory. In: TYPES ’95, pp. 120–134 (1996)
Hofmann, M.: Extensional Constructs in Intensional Type Theory. Springer, Berlin (1997)
Hofmann, M., Streicher, T.: Lifting Grothendieck universes. http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf (1999). Accessed 13 June 2018
Huber, S.: Canonicity for cubical type theory. arXiv:1607.04156 (2016)
Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium. Oxford University Press, Oxford (2002)
Kapulkin, C., Lumsdaine, P.L.: The simplicial model of univalent foundations (after Voevodsky). arXiv:1211.2851 (2012)
Mac Lane, S.: Categories for the Working Mathematician, vol. 5. Springer, Berlin (1978)
Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic. Springer, Berlin (1992)
Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Logic Colloquium ’73, pp. 73–118 (1975)
The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0 (2004)
McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1–13 (2008)
Møgelberg, R.E.: A type theory for productive coprogramming via guarded recursion. In: CSL-LICS (2014)
Nakano, H.: A modality for recursion. In: LICS, pp. 255–266 (2000)
Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. Thesis, Chalmers University of Technology (2007)
Orton, I., Pitts, A.M.: Axioms for modelling cubical type theory in a topos. In: CSL (2016)
Phoa, W.: An introduction to fibrations, topos theory, the effective topos and modest sets. Technical Report ECS-LFCS-92-208, LFCS, University of Edinburgh (1992)
Sacchini, J.L.: Well-founded sized types in the calculus of constructions. In: TYPES 2015 talk (2015) http://cs.ioc.ee/types15/programme-slides.html (2015). Accessed 13 June 2018
Spitters, B.: Cubical sets as a classifying topos. In: TYPES (2015)
The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study (2013)
Vickers, S.: Locales and toposes as spaces. In: Aiello, M., Pratt-Hartmann, I.E., van Benthem, J.F.A.K. (eds.) Handbook of Spatial Logics, pp. 429–496. Springer, Berlin (2007)
Voevodsky, V.: Martin-Lof identity types in the C-systems defined by a universe category. arXiv:1505.06446 (2015)