Computer Science Thesis Proposal
- Gates Hillman Centers
- EVAN CAVALLO
- Ph.D. Student
- Computer Science Department
- Carnegie Mellon University
Higher Inductive Types and Parametricity in Cubical Type Theory
Cubical type theory is a novel extension of dependent type theory with a form of equality called a path. Path equality enjoys extensionality properties missing from traditional treatments of equality, and it is proof-relevant: paths are data, and there can be many different paths between the same pair of objects. In particular, any isomorphism of types gives rise to a path between them; as everything respects equality, this means that constructions can be transferred between isomorphic objects just as in informal mathematical practice.
By providing a sensible equality, cubical type theory also enables sensible quotient types. However, the proof-relevant setting also motivates a more general notion of quotient known as a higher inductive type. The idea is to regard a quotient as an inductive definition where the generating operations may construct paths as well as ordinary elements. From this starting point, several directions of generalization are possible, just as with ordinary inductive types: there are indexed higher inductive types, higher inductive-inductive types, and so on. Originally proposed for homotopy type theory, a progenitor of cubical type theory, instances of higher inductive types have been used to great effect, but their general theory is still emerging. In this proposal, I describe a bare-bones schema for indexed higher inductive types, complete with a computational interpretation. I propose to extend this work to a fully-featured schema including inductive-inductive types and to implement it as part of a cubical proof assistant.
Working with proof-relevant equality has its own challenges, and effectively reasoning with higher inductive types is still a murky business. I propose that parametricity is a useful tool for this purpose, and describe an extension of cubical type theory with internal parametricity primitives. I propose to establish a connection between the extended theory and ordinary cubical type theory, to use it to simplify presently difficult proofs, and to implement the parametric extension.
Robert Harper (Chair)
Daniel R. Licata (Wesleyan University)
Anders Mörtberg (Stockholm University)
Copy of Proposal Document