research-article

Finite sets in homotopy type theory

Authors:

Herman Geuvers,

Léon Gondelman,

Niels van der WeideAuthors Info & Claims

CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 201 - 214

https://doi.org/10.1145/3167085

Published: 08 January 2018 Publication History

Abstract

We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.

On the foundational side, we use K to define the notions of "Kuratowski-finite type" and "Kuratowski-finite subobject", which we contrast with established notions, e.g. Bishop-finite types and enumerated types. We argue that Kuratowski-finiteness is the most general and flexible one of those and we define the usual operations on finite types and subobjects.

From the computational perspective, we show how to use K(A) for an abstract interface for well-known finite set implementations such as tree- and list-like data structures. This implies that a function defined on a concrete finite sets implementation can be obtained from a function defined on the abstract finite sets K(A) and that correctness properties are inherited. Hence, HoTT is the ideal setting for data refinement. Beside this, we define bounded quantification, which lifts a decidable property on A to one on K(A).

Supplementary Material

Auxiliary Archive (poplws18cpp-id38-aux.zip)

The accompanying Coq sources. The building instructions can be found in the file ReadMe.txt.

Download
54.47 KB

References

[1]

Robin Adams, Marc Bezem, and Thierry Coquand. 2016. A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. CoRR abs/1610.00026 (2016). http://arxiv.org/abs/1610.00026

[2]

Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, and Fredrik Nordvall Forsberg. 2016. Quotient Inductive-Inductive Types. CoRR abs/1612.02346 (2016). http://arxiv.org/abs/1612.02346

[3]

Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus. 2016. Partiality, Revisited: The Partiality Monad as a Quotient InductiveInductive Type. CoRR abs/1610.09254 (2016). http://arxiv.org/abs/1610. 09254

Digital Library

[4]

Thorsten Altenkirch and Ambrus Kaposi. 2016. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal. 6:1–6:16.

[5]

Thorsten Altenkirch and Ambrus Kaposi. 2016. 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 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. 18–29.

Digital Library

[6]

Carlo Angiuli, Edward Morehouse, Daniel R. Licata, and Robert Harper. 2016. Homotopical Patch Theory. J. Funct. Program. 26 (2016), e18.

[7]

Steven Awodey, Nicola Gambino, and Kristina Sojakova. 2012. Inductive Types in Homotopy Type Theory. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. 95–104.

Digital Library

[8]

Henning Basold, Herman Geuvers, and Niels van der Weide. 2017. Higher Inductive Types in Programming. Journal of Universal Computer Science 23, 1 (jan 2017), 63–88.

[9]

Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. The HoT T Library: A Formalization of Homotopy Type Theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017). ACM, New York, NY, USA, 164–172.

Digital Library

[10]

Yves Bertot, Georges Gonthier, Sidi Ould Biha, and Ioana Pasca. 2008. Canonical Big Operators. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings. 86–101.

Digital Library

[11]

Marc Bezem, Thierry Coquand, and Simon Huber. 2013. A Model of Type Theory in Cubical Sets. In 19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France. 107–128.

[12]

Marc Bezem, Keiko Nakata, and Tarmo Uustalu. 2012. On Streams that are Finitely Red. Logical Methods in Computer Science 8, 4 (2012).

[13]

Errett Bishop and Douglas Bridges. 1985. Constructive Analysis. Springer Berlin Heidelberg.

[14]

Andreas Blass. 1995. An Induction Principle and Pigeonhole Principles for K-Finite Sets. The Journal of Symbolic Logic 60, 4 (1995), 1186–1193.

[15]

Jesper Cockx, Dominique Devriese, and Frank Piessens. 2014. Pattern Matching Without K. In ACM SIGPLAN Notices, Vol. 49. ACM, 257–268.

Digital Library

[16]

Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2016. Cubical Type Theory: a Constructive Interpretation of the Univalence Axiom. CoRR abs/1611.02108 (2016). http://arxiv.org/abs/1611. 02108

[17]

Floris van Doorn. 2016. Constructing the Propositional Truncation using Non-Recursive HITs. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs. ACM, 122–129.

Digital Library

[18]

Peter Dybjer and Hugo Moeneclaey. 2017. Finitary Higher Inductive Types in the Groupoid Model. In Proceedings of MFPS 2017, Electronic Notes in Theoretical Computer Science, Vol. to appear. Elsevier.

[19]

Denis Firsov and Tarmo Uustalu. 2015. Dependently Typed Programming with Finite Sets. In Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP@ICFP 2015, Vancouver, BC, Canada, August 30, 2015. 33–44.

Digital Library

[20]

Denis Firsov, Tarmo Uustalu, and Niccolò Veltri. 2016. Variations on Noetherianness. In Proceedings 6th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2016, Eindhoven, Netherlands, 8th April 2016. 76–88.

[21]

Gaëtan Gilbert. 2017. Formalising Real Numbers in Homotopy Type Theory. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017. 112– 124.

Digital Library

[22]

Martin Hofmann and Thomas Streicher. 1994. The Groupoid Model Refutes Uniqueness of Identity Proofs. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS ’94), Paris, France, July 4-7, 1994. 208–212.

[23]

Martin Hofmann and Thomas Streicher. 1998. The Groupoid Interpretation of Type Theory. Twenty-five years of constructive type theory (Venice, 1995) 36 (1998), 83–111.

[24]

Kuen-Bang Hou (Favonia) and Michael Shulman. 2016. The Seifert-van Kampen Theorem in Homotopy Type Theory. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France. 22:1–22:16.

[25]

Peter T Johnstone. 2002. Sketches of an Elephant: a Topos Theory Compendium. Vol. 2. Oxford University Press.

[26]

Nicolai Kraus. 2016. Constructions with Non-Recursive Higher Inductive Types. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science. ACM, 595–604.

Digital Library

[27]

Robbert Krebbers and Bas Spitters. 2011. Type Classes for Efficient Exact Real Arithmetic in Coq. Logical Methods in Computer Science 9, 1 (2011).

[28]

Robbert Krebbers and Freek Wiedijk. 2015. A Typed C11 Semantics for Interactive Theorem Proving. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015. 15–27.

Digital Library

[29]

Casimir Kuratowski. 1920. Sur la Notion d’Ensemble Fini. Fundamenta Mathematicae 1, 1 (1920), 129–131. http://eudml.org/doc/212596

[30]

Stéphane Lescuyer. 2011. First-Class Containers in Coq. Stud. Inform. Univ. 9, 1 (2011), 87–127.

[31]

Stéphane Lescuyer. 2011. Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. (Formalisation et Developpement d’une Tactique Reflexive pour la Demonstration Automatique en Coq). Ph.D. Dissertation. University of Paris-Sud, Orsay, France. https://tel. archives-ouvertes.fr/tel-00713668

[32]

Daniel R Licata and Guillaume Brunerie. 2013. π n ( S n ) in Homotopy Type Theory. In International Conference on Certified Programs and Proofs. Springer, 1–16.

Digital Library

[33]

Daniel R Licata and Eric Finster. 2014. Eilenberg-MacLane Spaces in Homotopy Type Theory. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). ACM, 66.

Digital Library

[34]

Daniel R. Licata and Robert Harper. 2012. Canonicity for 2-Dimensional Type Theory. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012. 337–348.

Digital Library

[35]

Daniel R. Licata and Michael Shulman. 2013. Calculating the Fundamental Group of the Circle in Homotopy Type Theory. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. 223–232.

Digital Library

[36]

Peter LeFanu Lumsdaine and Mike Shulman. 2017. Semantics of Higher Inductive Types. arXiv preprint arXiv:1705.07088 (2017).

[37]

Keiko Nakata, Tarmo Uustalu, and Marc Bezem. 2011. A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction. In Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings. 353–368.

Digital Library

[38]

Erik Parmann. 2014. Investigating Streamless Sets. In 20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France. 187–201.

[39]

Erik Parmann. 2014. Some Varieties of Constructive Finiteness. In 19th Int. Conf. on Types for Proofs and Programs. 67–69.

[40]

Egbert Rijke and Bas Spitters. 2015. Sets in Homotopy Type Theory. Mathematical Structures in Computer Science 25, 5 (2015), 1172–1202.

[41]

Gert Smolka and Kathrin Stark. 2016. Hereditarily Finite Sets in Constructive Type Theory. Springer International Publishing, Cham, 374– 390.

[42]

Kristina Sojakova. 2015. Higher Inductive Types as Homotopy-Initial Algebras. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. 31–42.

Digital Library

[43]

Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings (Lecture Notes in Computer Science), Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar (Eds.), Vol. 5170. Springer, 278–293.

Digital Library

[44]

Arnaud Spiwack and Thierry Coquand. 2010. Constructively Finite? In Contribuciones científicas en honor de Mirian Andrés Gómez, Laureano Lambán Pardo, Ana Romero Ibáñez, and Julio Rubio García (Eds.). Universidad de La Rioja, 217–230. https://hal.inria.fr/inria-00503917

[45]

Wouter Swierstra. 2008. Data Types à la Carte. Journal of functional programming 18, 4 (2008), 423–436.

Digital Library

[46]

The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory. org/book, Institute for Advanced Study.

[47]

Tarmo Uustalu and Niccolò Veltri. 2017. The Delay Monad and Restriction Categories. Springer International Publishing, Cham, 32–50.

[48]

Tarmo Uustalu and Niccolò Veltri. 2017. Finiteness and Rational Sequences, Constructively. J. Funct. Program. 27 (2017), e13.

[49]

Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz. 2017. Homotopy Type Theory in Lean. In International Conference on Interactive Theorem Proving. Springer, 479–495.

[50]

Wim Veldman and Marc Bezem. 1993. Ramsey’s Theorem and the Pigeonhole Principle in Intuitionistic Mathematics. Journal of the London Mathematical Society 2, 2 (1993), 193–211.

[51]

Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. 2017. UniMath: Univalent Mathematics. Available at https://github.com/ UniMath .

[52]

Brent Abraham Yorgey. 2014. Combinatorial Species and Labelled Structures. Ph.D. Dissertation. University of Pennsylvania.

Cited By

Alexandru CChoudhury VRot Jvan der Weide NStark KTimany ABlazy STabareau N(2025)Intrinsically Correct Sorting in Cubical AgdaProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705873(34-49)Online publication date: 10-Jan-2025
https://dl.acm.org/doi/10.1145/3703595.3705873
Kidney DYang ZWu N(2024)Algebraic Effects Meet Hoare Logic in Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328988:POPL(1663-1695)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632898
Lamiaux TLjungström AMörtberg AKrebbers RTraytel DPientka BZdancewic S(2023)Computing Cohomology Rings in Cubical AgdaProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575677(239-252)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575677
Show More Cited By

Index Terms

Finite sets in homotopy type theory
1. Theory of computation
  1. Logic
    1. Constructive mathematics
    2. Type theory

Recommendations

Type theory in type theory using quotient inductive types
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids ...
Type theory in type theory using quotient inductive types
POPL '16

We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids ...
The HoTT library: a formalization of homotopy type theory in Coq
CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2018

306 pages

ISBN:9781450355865

DOI:10.1145/3176245

Program Chairs:
June Andronick
Data61 at CSIRO, Australia / UNSW, Australia
,
Amy Felty
University of Ottawa, Canada

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 January 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Available

Author Tags

Qualifiers

Research-article

Funding Sources

NWO

Conference

CPP '18

Sponsor:

SIGPLAN

CPP '18: Certified Proofs and Programs

January 8 - 9, 2018

CA, Los Angeles, USA

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
214
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Alexandru CChoudhury VRot Jvan der Weide NStark KTimany ABlazy STabareau N(2025)Intrinsically Correct Sorting in Cubical AgdaProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705873(34-49)Online publication date: 10-Jan-2025
https://dl.acm.org/doi/10.1145/3703595.3705873
Kidney DYang ZWu N(2024)Algebraic Effects Meet Hoare Logic in Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328988:POPL(1663-1695)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632898
Lamiaux TLjungström AMörtberg AKrebbers RTraytel DPientka BZdancewic S(2023)Computing Cohomology Rings in Cubical AgdaProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575677(239-252)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575677
Kupke CForsberg FWatters S(2023)A Fresh Look at Commutativity: Free Algebraic Structures via Fresh ListsProgramming Languages and Systems10.1007/978-981-99-8311-7_7(135-154)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_7
Baunsgaard Kristensen MMogelberg RVezzosi A(2022)Greatest HITs: Higher inductive types in coinductive definitions via induction under clocksProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533359(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533359
Møgelberg RVezzosi A(2021)Two Guarded Recursive Powerdomains for Applicative SimulationElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.351.13351(200-217)Online publication date: 29-Dec-2021
https://doi.org/10.4204/EPTCS.351.13
Angiuli CCavallo EMörtberg AZeuner M(2021)Internalizing representation independence with univalenceProceedings of the ACM on Programming Languages10.1145/34342935:POPL(1-30)Online publication date: 4-Jan-2021
https://doi.org/10.1145/3434293
Veltri NVezzosi ABlanchette JHriţcu C(2020)Formalizing 𝜋-calculus in guarded cubical AgdaProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3372885.3373814(270-283)Online publication date: 20-Jan-2020
https://dl.acm.org/doi/10.1145/3372885.3373814
Marmaduke AJenkins CStump A(2020)Quotients by Idempotent Functions in CedilleTrends in Functional Programming10.1007/978-3-030-47147-7_1(1-20)Online publication date: 11-May-2020
https://doi.org/10.1007/978-3-030-47147-7_1
Møgelberg RVeltri N(2019)Bisimulation as path type for guarded recursive typesProceedings of the ACM on Programming Languages10.1145/32903173:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290317

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten