Document Open Access Logo

Internal Strict Propositions Using Point-Free Equations

Authors István Donkó, Ambrus Kaposi

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.6.pdf
  • Filesize: 0.75 MB
  • 21 pages

Document Identifiers

Author Details

István Donkó
  • Eötvös Loránd University, Budapest, Hungary
Ambrus Kaposi
  • Eötvös Loránd University, Budapest, Hungary

Funding

  • Donkó, István: Supported by the ÚNKP-21-3 New National Excellence Program of the Ministry for Innovation and Technology from the source of the National Research, Development and Innovation Fund.
  • Kaposi, Ambrus: Supported by the Bolyai Fellowship of the Hungarian Academy of Sciences, Project no. BO/00659/19/3, and by the "Application Domain Specific Highly Reliable IT Solutions" project which has been implemented with the support provided from the National Research, Development and Innovation Fund of Hungary, financed under the Thematic Excellence Programme TKP2020-NKA-06 (National Challenges Subprogramme) funding scheme.

Acknowledgements

Thanks to Christian Sattler for discussions on the topics of this paper. Many thanks to the anonymous reviewers for their comments and suggestions.

Cite AsGet BibTex

István Donkó and Ambrus Kaposi. Internal Strict Propositions Using Point-Free Equations. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TYPES.2021.6

Abstract

The setoid model of Martin-Löf’s type theory bootstraps extensional features of type theory from intensional type theory equipped with a universe of definitionally proof irrelevant (strict) propositions. Extensional features include a Prop-valued identity type with a strong transport rule and function extensionality. We show that a setoid model supporting these features can be defined in intensional type theory without any of these features. The key component is a point-free notion of propositions. Our construction suggests that strict algebraic structures can be defined along the same lines in intensional type theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Martin-Löf’s type theory
  • intensional type theory
  • function extensionality
  • setoid model
  • homotopy type theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andreas Abel and Thierry Coquand. Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Log. Methods Comput. Sci., 16(2), 2020. URL: https://doi.org/10.23638/LMCS-16(2:14)2020.
  2. Thorsten Altenkirch. Extensional equality in intensional type theory. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 412-420. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782636.
  3. Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Christian Sattler, and Filippo Sestini. Constructing a universe for the setoid model. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12650 of Lecture Notes in Computer Science, pages 1-21. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_1.
  4. Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, and Nicolas Tabareau. Setoid type theory - a syntactic translation. In Graham Hutton, editor, Mathematics of Program Construction, pages 155-196, Cham, 2019. Springer International Publishing. Google Scholar
  5. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 18-29, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2837614.2837638.
  6. Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Type Theory, in Type Theory. Logical Methods in Computer Science, Volume 13, Issue 4, October 2017. URL: https://doi.org/10.23638/LMCS-13(4:1)2017.
  7. Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. The next 700 syntactical models of type theory. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 182-194, New York, NY, USA, 2017. ACM. URL: https://doi.org/10.1145/3018610.3018620.
  8. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with families: Unityped, simply typed, and dependently typed. CoRR, abs/1904.00827, 2019. URL: http://arxiv.org/abs/1904.00827.
  9. Thierry Coquand. About the setoid model, 2013. URL: http://www.cse.chalmers.se/~coquand/setoid.pdf.
  10. Thierry Coquand. Canonicity and normalization for dependent type theory. Theor. Comput. Sci., 777:184-191, 2019. URL: https://doi.org/10.1016/j.tcs.2019.01.015.
  11. Thierry Coquand. Reduction free normalisation for a proof irrelevant type of propositions. CoRR, abs/2103.04287, 2021. URL: http://arxiv.org/abs/2103.04287.
  12. István Donkó and Ambrus Kaposi. Agda formalization for the paper "Internal strict propositions using point-free equations". https://bitbucket.org/akaposi/prop, 2022.
  13. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. Proc. ACM Program. Lang., 3(POPL):3:1-3:28, 2019. URL: https://doi.org/10.1145/3290316.
  14. Martin Hofmann. Conservativity of equality reflection over intensional type theory. In TYPES 95, pages 153-164, 1995. Google Scholar
  15. Martin Hofmann. Extensional constructs in intensional type theory. CPHC/BCS distinguished dissertations. Springer, 1997. Google Scholar
  16. Jasper Hugunin. Why not w? In Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors, 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy, volume 188 of LIPIcs, pages 8:1-8:9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.8.
  17. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL):2:1-2:24, January 2019. URL: https://doi.org/10.1145/3290315.
  18. Ambrus Kaposi and Zongpu Xie. Quotient inductive-inductive types in the setoid model. In Henning Basold, editor, 27th International Conference on Types for Proofs and Programs, TYPES 2021. Universiteit Leiden, 2021. URL: https://types21.liacs.nl/download/quotient-inductive-inductive-types-in-the-setoid-model/.
  19. Nicolai Kraus and Jakob von Raumer. Coherence via well-foundedness: Taming set-quotients in homotopy type theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 662-675. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394800.
  20. Peter Lefanu Lumsdaine and Michael A. Warren. The local universes model: An overlooked coherence construction for dependent type theories. ACM Trans. Comput. Logic, 16(3), July 2015. URL: https://doi.org/10.1145/2754931.
  21. Erik Palmgren. From type theory to setoids and back. arXiv e-prints, page arXiv:1909.01414, September 2019. URL: http://arxiv.org/abs/1909.01414.
  22. Pierre-Marie Pédrot. Russian constructivism in a prefascist theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 782-794. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394740.
  23. The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. Technical report, Institute for Advanced Study, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact