Skip to main content
SpringerLink
Log in

Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory

  • Conference paper
  • First Online:
Recent Developments in Data Science and Intelligent Analysis of Information (ICDSIAI 2018)

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 836))

  • 437 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://github.com/mortberg/cubicaltt.

  2. 2.

    http://github.com/mortberg/cubicaltt.

  3. 3.

    http://github.com/groupoid/infinity.

  4. 4.

    http://github.com/UniMath.

  5. 5.

    http://github.com/groupoid/infinity/.

  6. 6.

    http://github.com/groupoid/infinity/tree/master/priv/iso.ctt.

  7. 7.

    https://homotopytypetheory.org/2012/11/21/on-heterogeneous-equality/.

References

  1. Martin-Löf, P., Sambin, G.: The theory of types. Studies in proof theory (1972)

    Google Scholar 

  2. Martin-Löf, P., Sambin, G.: Intuitionistic type theory. Studies in proof theory (1984)

    Google Scholar 

  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. Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom (2017)

    Google Scholar 

  5. The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013)

    Google Scholar 

  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. Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill Series in Higher Mathematics. McGraw-Hill, New York City (1967)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Igor Sikorsky Kyiv Polytechnical Institute, Kyiv, Ukraine

    Maksym Sokhatskyi & Pavlo Maslianko

Authors
  1. Maksym Sokhatskyi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pavlo Maslianko
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maksym Sokhatskyi .

Editor information

Editors and Affiliations

  1. Applied Mathematics Department, Igor Sikorsky Kyiv Polytechnic Institute, Kyiv, Ukraine

    Oleg Chertov

  2. Department of Economics, University of Pittsburgh, Pittsburgh, Pennsylvania, USA

    Tymofiy Mylovanov

  3. Department of Intelligent Information Systems, Petro Mohyla Black Sea National University, Mykolaiv, Ukraine

    Yuriy Kondratenko

  4. Systems Research Institute, Polish Academy of Sciences, Warsaw, Poland

    Janusz Kacprzyk

  5. Department of Computer Science, University of Texas at El Paso, El Paso, Texas, USA

    Vladik Kreinovich

  6. Institute for Information Transmission Problems, Russian Academy of Sciences, Moscow, Russia

    Vadim Stefanuk

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Sokhatskyi, M., Maslianko, P. (2019). Constructive Proofs of Heterogeneous Equalities in Cubical Type Theory. In: Chertov, O., Mylovanov, T., Kondratenko, Y., Kacprzyk, J., Kreinovich, V., Stefanuk, V. (eds) Recent Developments in Data Science and Intelligent Analysis of Information. ICDSIAI 2018. Advances in Intelligent Systems and Computing, vol 836. Springer, Cham. https://doi.org/10.1007/978-3-319-97885-7_30

Download citation

Publish with us

Policies and ethics

Search

Navigation