Document Open Access Logo

Data Types with Symmetries via Action Containers

Authors Philipp Joram , Niccolò Veltri

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2024.6.pdf
  • Filesize: 1.25 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Categorical semantics
Keywords
  • Containers
  • Homotopy Type Theory
  • Agda
  • 2-categories

Metrics

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

Abstract

We study two kinds of containers for data types with symmetries in homotopy type theory, and clarify their relationship by introducing the intermediate notion of action containers. Quotient containers are set-valued containers with groups of permissible permutations of positions, interpreted as (possibly non-finitary) analytic functors on the category of sets. Symmetric containers encode symmetries in a groupoid of shapes, and are interpreted accordingly as polynomial functors on the 2-category of groupoids.
Action containers are endowed with groups that act on their positions, with morphisms preserving the actions. We show that, as a category, action containers are equivalent to the free coproduct completion of a category of group actions. We derive that they model non-inductive single-variable strictly positive types in the sense of Abbott et al.: The category of action containers is closed under arbitrary (co)products and exponentiation with constants. We equip this category with the structure of a locally groupoidal 2-category, and prove that it locally embeds into the 2-category of symmetric containers. This follows from the embedding of a 2-category of groups into the 2-category of groupoids, extending the delooping construction.

Cite As Get BibTex

Philipp Joram and Niccolò Veltri. Data Types with Symmetries via Action Containers. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TYPES.2024.6

Author Details

Philipp Joram
  • Department of Software Science, Tallinn University of Technology, Estonia
Niccolò Veltri
  • Department of Software Science, Tallinn University of Technology, Estonia

Funding

This work was supported by the Estonian Research Council grant PSG749.
  • Joram, Philipp: Participation at TYPES'24 was supported by the COST Action CA20111 - European Research Network on Formal Proofs (EuroProofNet)

Supplementary Materials

References

  1. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Categories of Containers. In Andrew D. Gordon, editor, Proc. of 6th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS'03, volume 2620 of Lecture Notes in Computer Science, pages 23-38. Springer Berlin Heidelberg, 2003. URL: https://doi.org/10.1007/3-540-36576-1_2.
  2. Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3-27, 2005. URL: https://doi.org/10.1016/j.tcs.2005.06.002.
  3. Michael Abbott, Thorsten Altenkirch, Neil Ghani, and Conor McBride. Constructing Polymorphic Programs with Quotient Types. In Dexter Kozen and Carron Shankland, editors, Proc. of 7th Int. Conf. on Mathematics of Program Construction, MPC’04, volume 3125 of Lecture Notes in Computer Science, pages 2-15. Springer Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-27764-4_2.
  4. Jiří Adámek and Jiří Rosický. How nice are free completions of categories? Topology and its Applications, 273:106972, 2020. URL: https://doi.org/10.1016/j.topol.2019.106972.
  5. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-Wellfounded Trees in Homotopy Type Theory. In Thorsten Altenkirch, editor, Proc. of 13th Int. Conf. on Typed Lambda Calculi and Applications, TLCA'15, volume 38 of LIPIcs, pages 17-30. Schloss Dagstuhl, 2015. URL: https://doi.org/10.4230/LIPICS.TLCA.2015.17.
  6. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide. Bicategories in univalent foundations. Mathematical Structures in Computer Science, 31(10):1232-1269, 2021. URL: https://doi.org/10.1017/s0960129522000032.
  7. Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. Logical Methods in Computer Science, 15(1), March 2019. URL: https://doi.org/10.23638/lmcs-15(1:20)2019.
  8. Thorsten Altenkirch, Paul Blain Levy, and Sam Staton. Higher-Order Containers. In Fernando Ferreira, Benedikt Löwe, Elvira Mayordomo, and Luís Mendes Gomes, editors, 6th Conf. on Computability in Europe, CiE'10, volume 6158 of LNCS, pages 11-20. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13962-8_2.
  9. Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry. https://github.com/UniMath/SymmetryBook. Commit: 8546527.
  10. Håkon Robbestad Gylterud. Symmetric Containers. Master’s thesis, Department of Mathematics, Faculty of Mathematics and Natural Sciences, University of Oslo, 2011. URL: https://hdl.handle.net/10852/10740.
  11. Ryu Hasegawa. Two applications of analytic functors. Theoretical Computer Science, 272(1–2):113-175, February 2002. URL: https://doi.org/10.1016/s0304-3975(00)00349-2.
  12. Pieter Hofstra and Martti Karvonen. Inner automorphisms as 2-cells. Theory and Applications of Categories, 42(2):19-40, 2024. URL: http://www.tac.mta.ca/tac/volumes/42/2/42-02abs.html.
  13. Niles Johnson and Donald Yau. 2-Dimensional Categories. Oxford University Press, January 2021. URL: https://doi.org/10.1093/oso/9780198871378.001.0001.
  14. Philipp Joram and Niccolò Veltri. Constructive Final Semantics of Finite Bags. In Adam Naumowicz and René Thiemann, editors, Proc. of 14th Int. Conf. on Interactive Theorem Proving, ITP'23, volume 268 of LIPIcs, pages 12:1-12:19. Schloss Dagstuhl, 2023. URL: https://doi.org/10.4230/LIPICS.ITP.2023.20.
  15. André Joyal. Foncteurs analytiques et espèces de structures. In Gilbert Labelle and Pierre Leroux, editors, Combinatoire énumérative, volume 1234 of Lecture Notes in Mathematics, pages 126-159. Universite du Quebec a Montreal, Springer Berlin Heidelberg, May 1986. URL: https://doi.org/10.1007/bfb0072514.
  16. Daniel R. Licata and Eric Finster. Eilenberg-MacLane spaces in homotopy type theory. In Thomas A. Henzinger and Dale Miller, editors, Proc. of the Joint Meeting of the 23rd EACSL Ann. Conf. on Computer Science Logic (CSL) and the 29th Ann. ACM/IEEE Symp. on Logic in Computer Science (LICS), CSL-LICS'14, pages 66:1-66:9. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603153.
  17. Max New, Steven Shaefer, and contributors. cubical-categorical-logic, 2024. URL: https://github.com/maxsnew/cubical-categorical-logic.
  18. Andrew M. Pitts. Nominal sets. Number 57 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. Google Scholar
  19. The agda/cubical development team. The agda/cubical library, 2018. URL: https://github.com/agda/cubical/.
  20. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact