Document Open Access Logo

Formalising Inductive and Coinductive Containers

Authors Stefania Damato , Thorsten Altenkirch , Axel Ljungström

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.17.pdf
  • Filesize: 1.44 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • type theory
  • container
  • initial algebra
  • terminal coalgebra
  • Cubical Agda

Metrics

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

Abstract

Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed categories (LCCCs) with disjoint coproducts and W-types, and uniqueness of identity proofs (UIP) is implicitly assumed throughout. Although it is claimed that these developments can also be interpreted in extensional Martin-Löf type theory, this interpretation is not made explicit. In this paper, we present a formalisation of the results that "containers preserve least and greatest fixed points" in Cubical Agda, thereby giving a formulation in intensional type theory. Our proofs do not make use of UIP and thereby generalise the original results from talking about container functors on Set to container functors on the wild category of types. Our main incentive for using Cubical Agda is that its path type restores the equivalence between bisimulation and coinductive equality. Thus, besides developing container theory in a more general setting, we also demonstrate the usefulness of Cubical Agda’s path type to coinductive proofs.

Cite As Get BibTex

Stefania Damato, Thorsten Altenkirch, and Axel Ljungström. Formalising Inductive and Coinductive Containers. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.17

Author Details

Stefania Damato
  • School of Computer Science, University of Nottingham, UK
Thorsten Altenkirch
  • School of Computer Science, University of Nottingham, UK
Axel Ljungström
  • Department of Mathematics, Stockholm University, Sweden

Funding

  • Ljungström, Axel: This author is supported by the Swedish Research Council (Vetenskapsrådet) under Grant No. 2019-04545.

Acknowledgements

The authors would like to thank Anders Mörtberg, the anonymous reviewers, and the Agda Zulip and Discord communities for useful comments and discussions.

Supplementary Materials

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Categories of containers. In Andrew D. Gordon, editor, Foundations of Software Science and Computation Structures, pages 23-38, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. URL: https://dl.acm.org/doi/10.5555/1754809.1754813.
  2. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Representing nested inductive types using W-types. In Automata, Languages and Programming, 31st International Colloqium (ICALP), pages 59-71, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_8.
  3. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3-27, 2005. Applied Semantics: Selected Topics. URL: https://doi.org/10.1016/j.tcs.2005.06.002.
  4. Michael Gordon Abbott. Categories of Containers. PhD thesis, University of Leicester, 2003. URL: https://hdl.handle.net/2381/30102.
  5. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in homotopy type theory. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17-30, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.17.
  6. Thorsten Altenkirch. Cubical primitives should preserve guardedness. https://github.com/agda/agda/issues/4740, 2020. Online.
  7. Thorsten Altenkirch. Quotient inductive types as categorified containers. https://hott-uf.github.io/2024/abstracts/HoTTUF_2024_paper_10.pdf, 2024. HoTT/UF 2024 abstract.
  8. Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, and Nicolas Tabereau. Setoid type theory - a syntactic translation, 2019. URL: https://doi.org/10.1007/978-3-030-33636-3_7.
  9. Jeremy Avigad, Mario Carneiro, and Simon Hudon. Data Types as Quotients of Polynomial Functors. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6:1-6:19, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.6.
  10. Ulrik Buchholtz. Higher structures in homotopy type theory. In Stefania Centrone, Deborah Kant, and Deniz Sarikaya, editors, Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts, pages 151-172. Springer International Publishing, Cham, 2019. URL: https://doi.org/10.1007/978-3-030-15655-8_7.
  11. Joshua Chen. 2-coherent internal models of homotopical type theory, 2025. URL: https://doi.org/10.48550/arXiv.2503.05790.
  12. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  13. Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 255-264, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209197.
  14. Stefania Damato, Thorsten Altenkirch, and Axel Ljungström. stefaniatadama/formalising-inductive-coinductive-containers. Software, (visited on 2025-09-09). URL: https://github.com/stefaniatadama/formalising-inductive-coinductive-containers/blob/main/cubical/Cubical/Papers/Containers.agda
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24710
  15. Damato, Stefania and Altenkirch, Thorsten and Ljunström, Axel. Formalising inductive and coinductive containers, June 2025. Accompanying formalisation. URL: https://github.com/stefaniatadama/formalising-inductive-coinductive-containers/blob/main/cubical/Cubical/Papers/Containers.agda.
  16. Nicola Gambino and Martin Hyland. Wellfounded trees and dependent polynomial functors. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs, pages 210-225, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-24849-1_14.
  17. Håkon Robbestad Gylterud. Symmetric containers, 2011. Master’s thesis. URL: https://staff.math.su.se/gylterud/thesis_gylterud.pdf.
  18. Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Selected Papers from the 8th International Workshop on Computer Science Logic, CSL '94, pages 427-441, Berlin, Heidelberg, 1994. Springer-Verlag. URL: https://doi.org/10.1007/BFb0022273.
  19. Nicolai Kraus and Jakob von Raumer. Path spaces of higher inductive types in homotopy type theory. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '19. IEEE Press, 2021. URL: https://doi.org/10.5555/3470152.3470159.
  20. Joachim Lambek. A fixpoint theorem for complete categories. Mathematische Zeitschrift, 103:151-161, 1968. URL: http://eudml.org/doc/170906.
  21. Peter LeFanu Lumsdaine and Michael Shulman. Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, 169(1):159-208, 2020. URL: https://doi.org/10.1017/S030500411900015X.
  22. Per Martin-Löf. An Intuitionistic Theory of Types. Clarendon Press, 1972. Appears in `Twenty-Five Years of Constructive Type Theory'. Google Scholar
  23. Per Martin-Löf. Intuitionistic type theory, 1984. Notes by Giovanni Sambin, available at URL: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-1984.pdf.
  24. Per Martin-Löf. Constructive mathematics and computer programming. In L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, and Klaus-Peter Podewski, editors, Logic, Methodology and Philosophy of Science VI, volume 104 of Studies in Logic and the Foundations of Mathematics, pages 153-175. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(09)70189-2.
  25. R.A.G. Seely. Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society, 95:33-48, 1984. URL: https://doi.org/10.1017/S0305004100061284.
  26. The Agda Community. Cubical Agda Library, March 2025. URL: https://github.com/agda/cubical.
  27. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  28. Benno van den Berg and Federico De Marchi. Non-well-founded trees in categories. Annals of Pure and Applied Logic, 146(1):40-59, 2007. URL: https://doi.org/10.1016/j.apal.2006.12.001.
  29. Andrea Vezzosi. Streams for cubical type theory, 2017. Unpublished note, available at URL: https://saizan.github.io/streams-ctt.pdf.
  30. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. Journal of Functional Programming, 31:e8, 2021. URL: https://doi.org/10.1017/S0956796821000034.
  31. Vladimir Voevodsky. The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010), 2014. URL: https://arxiv.org/abs/1402.5556.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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