Cubical agda: a dependently typed programming language with univalence and higher inductive types

Andrea Vezzosi, Anders Mörtberg, Andreas Abel

    Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

    Abstract

    Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.
    Original languageEnglish
    Article number87
    JournalProceedings of the ACM on Programming Languages
    Volume3
    Issue numberICFP
    Pages (from-to)87:1-87:29
    Number of pages29
    DOIs
    Publication statusPublished - Aug 2019
    EventInternational Conference on Functional Programming (IFCP 2019) - Hotel Scandic Berlin Potsdamer Platz, Berlin, Germany
    Duration: 18 Aug 201923 Aug 2019
    https://icfp19.sigplan.org/home

    Conference

    ConferenceInternational Conference on Functional Programming (IFCP 2019)
    LocationHotel Scandic Berlin Potsdamer Platz
    Country/TerritoryGermany
    CityBerlin
    Period18/08/201923/08/2019
    Internet address

    Keywords

    • Dependent Type Theory
    • Proof Assistants
    • Cubical Type Theory
    • Univalent Foundations
    • Extensionality Principles

    Fingerprint

    Dive into the research topics of 'Cubical agda: a dependently typed programming language with univalence and higher inductive types'. Together they form a unique fingerprint.

    Cite this