Advertisement

Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory

  • Maksym Sokhatskyi
  • Pavlo Maslianko
Conference paper
Part of the Advances in Intelligent Systems and Computing book series (AISC, volume 836)

Abstract

This paper represents the very small part of the developed base library for homotopical prover based on Cubical Type Theory (CTT) announced in 2017. We demonstrate the usage of this library by showing how to build a constructive proof of heterogeneous equality, the simple and elegant formulation of the equality problem, that was impossible to achieve in pure Martin-Löf Type Theory (MLTT). The machinery used in this article unveils the internal aspect of path equalities and isomorphism, used e.g. for proving univalence axiom, that became possible only in CTT. As an example of complex proof that was impossible to construct in earlier theories we took isomorphism between Nat and Fix Maybe datatypes and built a constructive proof of equality between elements of these datatypes. This approach could be extended to any complex isomorphic data types.

Keywords

Formal methods Type theory Computer languages Theoretical computer science Applied mathematics Isomorphism Heterogeneous equality Cubical Type Theory Martin-Löf Type Theory 

References

  1. 1.
    Martin-Löf, P., Sambin, G.: The theory of types. Studies in proof theory (1972)Google Scholar
  2. 2.
    Martin-Löf, P., Sambin, G.: Intuitionistic type theory. Studies in proof theory (1984)Google Scholar
  3. 3.
    Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: In Venice Festschrift, pp. 83–111. Oxford University Press (1996)Google Scholar
  4. 4.
    Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom (2017)Google Scholar
  5. 5.
    The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013)Google Scholar
  6. 6.
    Bove, A., Dybjer, P., Norell, U.: A brief overview of agda—a functional language with dependent types. In: Proceedings of the 22-nd International Conference on Theorem Proving in Higher Order Logics, pp. 73–78. Springer-Verlag (2009)Google Scholar
  7. 7.
    Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill Series in Higher Mathematics. McGraw-Hill, New York City (1967)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Igor Sikorsky Kyiv Polytechnical InstituteKyivUkraine

Personalised recommendations