2026-07-30T23:40:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23368 2025-10-27T10:17:23Z ddc:004 open_access

Data Types with Symmetries via Action Containers Joram, Philipp Veltri, Niccolò Containers Homotopy Type Theory Agda 2-categories 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Philipp Joram and Niccolò Veltri 2025 Is Part Of LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2024.6 urn:nbn:de:0030-drops-233681 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.6 eng https://creativecommons.org/licenses/by/4.0/legalcode