Data Types with Symmetries via Action Containers

Joram, Philipp; Veltri, Niccolò

doi:10.4230/LIPIcs.TYPES.2024.6

Data Types with Symmetries via Action Containers

Philipp Joram

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

Department of Software Science, Tallinn University of Technology, Estonia

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.

Keywords and phrases:

Containers, Homotopy Type Theory, Agda, 2-categories

Funding:

Philipp Joram: Participation at TYPES’24 was supported by the COST Action CA20111 – European Research Network on Formal Proofs (EuroProofNet)

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Type theory ; Theory of computation

\rightarrow

Categorical semantics

Supplementary Material:

Software (Agda): https://github.com/phijor/cubical-containers
archived at

swh:1:dir:a77c8b642661074b9804670b14cf97cc844aff16

Funding:

This work was supported by the Estonian Research Council grant PSG749.

DOI:

10.4230/LIPIcs.TYPES.2024.6

Event:

30th International Conference on Types for Proofs and Programs (TYPES 2024)

Editors:

Rasmus Ejlers Møgelberg and Benno van den Berg

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Containers are a representation of strictly positive data types, introduced by Abbott et al. [1]. A container consists of a type of shapes and a type of positions associated to each shape. For example, the container of ordered lists consists of natural numbers $n : ℕ$ as shapes and finite ordinals $\operatorname{\mathsf{Fin}}(n)$ as positions, the idea being that each list has a length $n$ and $\operatorname{\mathsf{Fin}}(n)$ -many locations that can hold data. Containers can be interpreted as polynomial endofunctors, the latter being the polymorphic data types that the containers represent. For example, the interpretation of the list container is the $\operatorname{\mathsf{List}}$ functor.

Containers form a category. Its morphisms represent polymorphic functions between data types, which are interpreted as natural transformations between the corresponding polynomial endofunctors. This category is rich in structure; among other things it is cocartesian closed, is closed under the construction of initial algebras and terminal coalgebras, and admits a notion of derivative.

Traditionally, the theory of containers is studied in $\mathsf{Set}$ -like categories. When interpreted in such categories, the data of containers may however be too restrictive to encode certain data types of interest. This is especially the case if one wants to account for symmetries, i.e. identify configurations of positions when one can turn into the other via the action of certain permutations. For example, one can represent ordered lists, but it is not possible to represent cyclic lists or finite multisets as a container.

Some efforts have been made to enhance the expressivity of containers to represent data types with symmetries. Abbott et al. [3] introduced quotient containers, which are containers in which the assignment of values to positions is invariant under a collection of permutations on positions. This is realized by requiring the presence of a subgroup of the symmetric group on positions, corresponding to the collection of admissible permutations. Interpretation of quotient containers embeds them as a subcategory of set-endofunctors, targeting certain quotients of polynomial endofunctors. For quotient containers with finitary positions, these correspond to Joyal’s analytic functors [15].

Symmetric containers, introduced by Gylterud [10], consist of a groupoid of shapes, with positions being a set-valued functor over this groupoid. This means that the symmetries are encoded directly in the isomorphisms of the shape groupoid. From the perspective of (homotopy) type theory, symmetric containers correspond to set-bundles over homotopy-groupoids. They form a locally univalent 2-category, and are interpreted as polynomial endofunctors on the 2-category of groupoids.

Quotient and symmetric containers are two different ways to extend the expressivity of ordinary containers to include symmetries between positions. Our interest lies in understanding how these two approaches are related. To this end, we introduce an intermediate notion: action containers. An action container consists of a set of shapes and, for each shape $s$ , a set of positions $P_{s}$ and a group $G_{s}$ acting on $P_{s}$ . On one side, such containers generalize quotient containers, as the allowed permutations are determined by the action of an arbitrary group, and are not restricted to subgroups of the symmetric groups. On the other, they are a special case of symmetric containers: a $G_{s}$ -action is a functor from $G_{s}$ (as a 1-object groupoid) to $\mathsf{Set}$ , and summation of these functors over all shapes $s$ yields a symmetric container.

We describe a notion of morphisms of action containers, inspired by (pre)morphisms of quotient containers. Differently from the latter, morphisms of action containers have to explicitly preserve the structure of the groups acting on positions. Action containers form a category, and we show that this category is the free coproduct completion of a category of group actions in the form of the $\operatorname{Fam}$ -construction. From this we derive closure under arbitrary products and coproducts, as well as exponentials with constant domain.

To compare action containers with the 2-category of symmetric containers, we define a notion of invertible 2-cell between these morphisms, enriching them to a 2-category. Crucially, we observe that this 2-category can again be modularly constructed starting from a 2-category of groups, group homomorphisms and conjugators [12] using the techniques of displayed bicategories [6]: we first define a 2-category of group actions, displayed over this 2-category of groups, then repeat a 2-categorical version of the $\operatorname{Fam}$ -construction, presenting the 2-category of action containers as that of families of group actions.

We construct a 2-functor between the 2-categories of action containers and symmetric containers; again in multiple steps. First we notice that the delooping of a group extends to a 2-functor $\mathbf{B}{}:\operatorname{\mathsf{Group}}\to\operatorname{\mathsf{hGpd}}$ between the 2-categories of groups and groupoids, and that this is locally a weak equivalence. We show, again using the displayed machinery, how to lift this to a local weak equivalence $\mathbf{\bar{B}}{}:\operatorname{\mathsf{Action}}\to\operatorname{\mathsf{% SetBundle}}$ between the 2-categories of group actions and set bundles.

The $\operatorname{Fam}$ -construction yields a 2-functor $\operatorname{Fam}(\mathbf{\bar{B}}{}):\operatorname{Fam}(\operatorname{% \mathsf{Action}})\to\operatorname{Fam}(\operatorname{\mathsf{SetBundle}})$ between the 2-categories of families of group actions, i.e. action containers, and families of set bundles. We show that the action of $\operatorname{Fam}$ preserves local fully-faithfullness, but that preservation of local essential surjectivity requires an application of the axiom of choice. Finally, we describe a 2-functor $\Sigma:\operatorname{Fam}(\operatorname{\mathsf{SetBundle}})\to\operatorname{% \mathsf{SetBundle}}$ performing summations of family of set bundles, implicitly employing the universal property of the $\operatorname{Fam}$ -construction as free coproduct completion. The latter does not seem to be fully faithful, however its restriction to set bundles with connected bases is. This implies that the composite 2-functor $\Sigma\circ\operatorname{Fam}(\mathbf{\bar{B}}{}):\operatorname{Fam}(% \operatorname{\mathsf{Action}})\to\operatorname{\mathsf{SetBundle}}$ is locally fully faithful. This means that, not only do action containers correspond to certain symmetric containers, but so do their morphisms: conjugators between action container morphisms represent exactly identifications of symmetric container morphisms.

We implement our results using the Agda proof assistant, building on top of the agda/cubical [19] and cubical-categorical-logic [17] libraries. Our code is freely available at https://github.com/phijor/cubical-containers. The repository contains a README linking results of this paper to the corresponding formalization in the code.

1.1 Notation and Background

Our work takes place in homotopy type theory, which is a well-suited foundational framework for our investigation. This is mostly due to the fact that we can work with syntethic groupoids, i.e. h-groupoids, in place of categorical groupoids, which considerably simplify the described constructions. We take full advantage of higher inductive types (HITs) to define mere existence via propositional truncation, set quotients and the delooping of groups. In this short section, we recall some basic terminology and fix the notation we use. More details can be found in the HoTT book [20].

We write $\prod_{a:A}B(a)$ for dependent products, $A\to B$ for their non-dependent variant, and $\sum_{a:A}B(a)$ for dependent sums. Two-argument function application is written $f(a,b)$ or, to reduce visual clutter, $f_{a}(b)$ . Most of our constructions are universe-polymorphic, but for the sake of readability in the paper we use only the lowest universe of types, denoted $\mathcal{U}$ . The type of $h$ -sets is $\operatorname{\mathsf{hSet}}$ , the type of $h$ -groupoids is $\operatorname{\mathsf{hGpd}}$ . We will often simply talk about sets and groupoids instead of $h$ -sets and $h$ -groupoids. We suppress proofs of truncation level when they are routine, e.g. for nested $\Sigma$ - and $\Pi$ -types. The type of natural numbers is $ℕ$ and the finite ordinals $\operatorname{\mathsf{Fin}}:ℕ\to\operatorname{\mathsf{hSet}}$ . For $x, y : A$ , we denote their type of identifications by $x=y$ , and call $p:x=y$ either an identification or a path. Given a family $B$ over $A$ and terms $x^{\prime}:B(x)$ , $y^{\prime}:B(y)$ , we write $x^{\prime}\mathrel{=_{B(p)}}y^{\prime}$ for the type of dependent paths, or $x^{\prime}\mathrel{=_{p}}y^{\prime}$ when $B$ can be inferred. Defining equalities are denoted $x\mathrel{:=}y$ ; for judgmentally equal $x$ and $y$ , we write $x\mathrel{\doteq}y$ . For functions into $\Sigma$ -types, we use binders to name the projections: given $f:X\to\sum_{a:A}B(a)$ , we write $\lambda x\mathpunct{.}(a(x),b(x))$ or $\lambda x\mathpunct{.}(a_{x},b_{x})$ for $a\mathrel{:=}\operatorname{\mathsf{fst}}\circ f$ and $b\mathrel{:=}\operatorname{\mathsf{snd}}\circ f$ .

The propositional truncation of a type $X$ is $\lVert X\rVert_{{\shortminus 1}}$ , the set truncation of $X$ is $\lVert X\rVert_{0}$ . Notice that there are two competing conventions for indexing truncation levels: (-2)-based (HoTT-book style) and 0-based (Voevodsky-style). Our formalization, done in Cubical Agda, is 0-based, yet this paper, which is written in HoTT-book style, starts indexing at -2. Whenever possible however, we will explicitly use the words “proposition”, “set” and “groupoid” to avoid confusion. Mere existential quantification is defined as $\operatorname*{\vphantom{\sum}\mathchoice{\vbox{\hbox{$\exists$}}}{\vbox{\hbox% {$\exists$}}}{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}}_{a:A}B(a)% \mathrel{:=}\lVert\sum_{a:A}B(a)\rVert_{{\shortminus 1}}$ . The set quotient of a type $A$ by a (possibly non-propositional) relation $R$ is $A/R$ . The circle $S^{1}$ is a HIT with constructors $\mathord{\bullet}:S^{1}$ and $\operatorname{\mathsf{loop}}:\mathord{\bullet}=\mathord{\bullet}$ . Propositional and set truncations, as well as set quotients and the circle, are defined as higher inductive types. The main HIT employed in this paper is the delooping of a group, introduced in Section 2.3.

Given a pointed type $(X,x_{0})$ , its loop space is $\operatorname{\Omega}(X,x_{0})\mathrel{:=}(x_{0}=x_{0})$ , and its fundamental group is its set truncation $\operatorname{\pi_{1}}(X,x_{0})\mathrel{:=}\lVert\operatorname{\Omega}(X,x_{0}% )\rVert_{0}$ . The connected components of a type $X$ are collected in its set truncation $\operatorname{\pi_{0}}(X)\mathrel{:=}\lVert X\rVert_{0}$ . We say that $X$ is connected if $\lVert X\rVert_{0}$ is contractible.

For groups $G$ and $H$ we denote the type of group homomorphisms by $G\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.2}{\kern-1.% 07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}H$ . We denote the type of subgroup inclusions by $G\leq H\mathrel{:=}\sum{(\iota:G\mathrel{\vbox{\offinterlineskip\halign{\hfil#% \hfil\cr\scalebox{1.2}{\kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}H)}% \mathpunct{.}\operatorname{\mathsf{isInjective}}(\iota)$ . The symmetric group of a set $X$ is $\operatorname{\mathfrak{S}}(X)\mathrel{:=}\operatorname{\Omega}(\operatorname{% \mathsf{hSet}},X)$ . The unit of this group is reflexivity $\operatorname{\mathsf{refl}}$ , multiplication is composition of paths $p\cdot q$ , inverse is path reversal. Recall that, by univalence, $\operatorname{\mathfrak{S}}(X)$ is equivalent to the type of equivalences $X\simeq X$ . We abbreviate $\operatorname{\mathfrak{S}}(n)\mathrel{:=}\operatorname{\mathfrak{S}}(% \operatorname{\mathsf{Fin}}(n))$ . An action of $G$ on a set $X$ is a group homomorphism $\sigma:G\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.2}{% \kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}\operatorname{\mathfrak{S}}% (X)$ . For $g : G$ , we denote $\operatorname{\mathsf{transport}}(\sigma(g)):X\to X$ simply by $\sigma(g)$ , and apply it to some $x : X$ either as $\sigma(g,x)$ or $\sigma_{g}(x)$ . The action is said to be faithful if $\sigma$ is injective. The set of $\sigma$ -orbits is denoted $X/G$ , and defined as the set quotient of $X$ by the orbit relation $x\sim y\mathrel{:=}\exists{g:G}\mathpunct{.}x=\sigma_{g}(y)$ .

1.2 2-Categories

In this paper, we make use of higher categories in the form of (2,1)-categories. We follow the definitions of bicategorical concepts of [13], and adapt them to the setting of homotopy type theory: a 2-category $\mathsf{C}$ consist of a type of objects $x,y:\mathsf{C}_{0}$ , 1-cells $f,g:\mathsf{C}_{1}(x,y)$ , and 2-cells $r,s:\mathsf{C}_{2}(f,g)$ , with horizontal composition of 1- and 2-cells, and vertical composition of 2-cells, subject to suitable axioms. In particular, all types of 2-cells $\mathsf{C}_{2}(f,g)$ are assumed to be $h$ -sets. Composition of 1-cells is unital and associative up to a chosen identification, not just a 2-cell. All instances of 2-categories considered here are either locally strict (i.e. 1-cells form sets) or locally univalent; such 2-categories always admit a unique coherently strict structure.

If $\mathsf{C}$ is understood from context, we write $f,g:x\to y$ for $f,g:\mathsf{C}_{1}(x,y)$ , and $r:f\Rightarrow g$ for $r:\mathsf{C}_{2}(f,g)$ . We compose cells in diagrammatic order. Juxtaposition denotes horizontal composition, whereas vertical composition of 2-cells is denoted $r\mathbin{\bullet}s$ .

Let $f,g:x\to y$ . Under vertical composition, 2-cells $\mathsf{C}_{2}(f,g)$ form the morphisms of an (ordinary) category, called the local category at $x$ and $y$ , denoted by its type of objects $\mathsf{C}_{1}(x,y)$ . If a proposition $P$ holds for all local categories of a 2-category, we say that it is locally $P$ . A (2,1)-category is thus defined to be a locally groupoidal 2-category, that is, one for which 2-cells in each local category are invertible. A 2-category is locally thin if $\mathsf{C}_{2}(f,g)$ is a proposition for each pair of 1-cells $f,g:\mathsf{C}_{1}(x,y)$ , i.e. there is at most one 2-cell from $f$ to $g$ . Any ordinary category $\mathcal{C}$ forms a locally thin 2-category: 2-cells are homotopies of 1-cells, $\mathcal{C}_{2}(f,g)\mathrel{:=}(f=g)$ .

We use the machinery of displayed bicategories [6] to define complex 2-categories from modular gadgets. A displayed 2-category $\mathsf{D}$ over a base 2-category $\mathsf{C}$ consists of a family of objects $\mathsf{D}_{0}:\mathsf{C}_{0}\to\mathcal{U}$ , a family of 1-cells $\mathsf{D}_{1}:\mathsf{C}_{1}(x,y)\to\mathsf{D}_{0}(x)\to\mathsf{D}_{0}(y)\to% \mathcal{U}$ , and a family of 2-cells $\mathsf{D}_{2}:\mathsf{C}_{2}(f,g)\to\mathsf{D}_{1}(f;\bar{x},\bar{y})\to% \mathsf{D}_{1}(g;\bar{x},\bar{y})\to\mathcal{U}$ , satisfying dependent analogues of the 2-category axioms. If unambiguous, we write $\bar{f}:\bar{x}\to_{f}\bar{y}$ for $\bar{f}:\mathsf{D}_{1}(f;\bar{x},\bar{y})$ , as well as $\bar{r}:\bar{f}\Rightarrow_{r}\bar{g}$ for $\bar{r}:\mathsf{D}_{2}(r;\bar{f},\bar{g})$ . The total 2-category of $\mathsf{D}$ over $\mathsf{C}$ is denoted $\int\mathsf{D}$ , and is a 2-categorical analouge of $\sum$ -types: objects are pairs of objects ${\int_{0}\!\mathsf{D}}\mathrel{:=}\sum_{x:\mathsf{C}_{0}}\mathsf{D}_{0}(x)$ , 1-cells are ${\int_{1}\!\mathsf{D}}\big{(}(x,\bar{x}),(y,\bar{y})\big{)}\mathrel{:=}\sum_{f% :\mathsf{C}_{1}(x,y)}\mathsf{D}_{1}(f;\bar{y},\bar{x})$ , and 2-cells ${\int_{2}\!\mathsf{D}}\big{(}(f,\bar{f}),(g,\bar{g})\big{)}\mathrel{:=}\sum_{r% :\mathsf{C}_{2}(f,g)}\mathsf{D}_{2}(r;\bar{f},\bar{g})$ . To highlight the dependency on $\mathsf{C}$ , we sometimes write $\int_{\mathsf{C}}\mathsf{D}$ or even $\int_{x:\mathsf{C}}\mathsf{D}(x)$ .

We go between 2-categories via 2-functors. For a 2-functor $F:\mathsf{C}\to\mathsf{D}$ we denote its action on objects, 1-, and 2-cells by $F_{0}$ , $F_{1}$ and $F_{2}$ respectively. They are assumed to strictly preserve composition and units of 1-cells, that is up to an identification of 1-cells in the codomain. The actions on 1- and 2-cells define functors of local categories, and we call $F$ locally $P$ if all local functors satisfy a proposition $P$ .

We define a notion of displayed 2-functor $\bar{F}:\bar{\mathsf{C}}\to_{F}\bar{\mathsf{D}}$ between 2-categories displayed over $\mathsf{C}$ and $\mathsf{D}$ and a (base) 2-functor $F:\mathsf{C}\to\mathsf{D}$ . To cells in $\bar{\mathsf{C}}$ it assigns cells in $\bar{\mathsf{D}}$ displayed over the image of $F$ : it consists of assignments of objects $\bar{F}_{0}:\bar{\mathsf{C}}_{0}(x)\to\bar{\mathsf{D}}_{0}(F_{0}(x))$ , 1-cells $\bar{F}_{1}:\bar{\mathsf{C}}_{1}(f;\bar{x},\bar{y})\to\bar{\mathsf{D}}_{1}(F_{% 1}(f);\bar{F}_{0}(\bar{x}),\bar{F}_{0}(\bar{y}))$ and 2-cells $\bar{F}_{2}:\bar{\mathsf{C}}_{2}(r;\bar{f},\bar{g})\to\bar{\mathsf{D}}_{2}({F_% {2}}r;\bar{F}_{1}\bar{f},\bar{F}_{1}\bar{g})$ , satisfying dependent analogues of the 2-functor axioms. A displayed 2-functor induces a 2-functor between total 2-categories, denoted ${\int}\bar{F}:\int\mathsf{C}\to\int\mathsf{D}$ .

The 2-category of $h$ -groupoids is denoted by $\operatorname{\mathsf{hGpd}}$ . Its 1-cells are functions between the underlying types and 2-cells are homotopies between functions.

2 Quotient and Symmetric Containers

In this section we recall the notions of quotient and symmetric containers, as well as their morphisms.

2.1 Quotient Containers

Quotient containers were introduced by Abbott et al. [3] as a way to add symmetries to containers in an extensional type theory with quotient types. Here we state their definition in HoTT.

Definition 1.

A quotient container $(S\mathbin{\triangleright}P\mathord{/}G)$ consists of a set of shapes $S$ , a family of positions $P:S\to\operatorname{\mathsf{hSet}}$ and symmetry groups $\iota_{s}:G_{s}\leq\operatorname{\mathfrak{S}}(P_{s})$ for each $s : S$ .

Each group element $g:G_{s}$ defines a path $\iota_{s}(g):P_{s}=P_{s}$ . By $\operatorname{\mathsf{transport}}$ , this induces a map $P_{s}\to P_{s}$ ; in the remainder, we will identify $g$ and this map.

Example 2.

The quotient container of unordered $n$ -tuples $\operatorname{\mathsf{U}}_{n}\mathrel{:=}(1\mathbin{\triangleright}% \operatorname{\mathsf{Fin}}(n)\mathord{/}\operatorname{\mathfrak{S}}(n))$ has a single shape, and over it positions $\operatorname{\mathsf{Fin}}(n)$ . On these $n$ positions, the full group of permutations $\operatorname{\mathfrak{S}}(\operatorname{\mathsf{Fin}}(n))$ acts as its symmetry group. We call $\operatorname{\mathsf{U}}_{1}$ the identity container; it has a single shape, on which the trivial group acts.

Like an ordinary container, a quotient container defines an endofunctor on the category of sets, called its extension. Whereas for ordinary containers this is a polynomial functor, for quotient containers it is a sum of quotients of representables:

Definition 3 (extension of quotient containers).

The extension of $(S\mathbin{\triangleright}P\mathord{/}G)$ is the map $\llbracket S\mathbin{\triangleright}P\mathord{/}G\rrbracket_{/}:\operatorname{% \mathsf{hSet}}\to\operatorname{\mathsf{hSet}}$ given by

\displaystyle\llbracket S\mathbin{\triangleright}P\mathord{/}G\rrbracket_{/}(X)

\displaystyle\mathrel{:=}\sum_{s:S}\frac{P_{s}\to X}{\sim_{s}},

\displaystyle v\sim_{s}w

\displaystyle\mathrel{:=}{\textstyle\operatorname*{\vphantom{\sum}\mathchoice{% \vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{% \vbox{\hbox{$\exists$}}}}_{g:G_{s}}v=w\circ g}

\lrcorner

When positions are finite sets, the extension is an analytic functor in the sense of Joyal [15].

Example 4 (unordered $n$ -tuples).

The extension of $\operatorname{\mathsf{U}}_{n}$ is the type of unordered $n$ -tuples:

\llbracket\operatorname{\mathsf{U}}_{n}\rrbracket_{/}(X)\mathrel{:=}\sum_{% \mathunderscore:1}{(\operatorname{\mathsf{Fin}}(n)\to X)/{\sim}}={X^{n}}/{\sim% _{\operatorname{\mathfrak{S}}(n)}}

where $x\sim_{\operatorname{\mathfrak{S}}(n)}y$ if and only if $x_{i}=y_{\sigma(i)}$ for some permutation $\sigma:\operatorname{\mathfrak{S}}(n)$ . When $n=1$ , we obtain the identity function $\llbracket\operatorname{\mathsf{U}}_{1}\rrbracket_{/}X=X$ .

Definition 5.

A premorphism of quotient containers, $(u\mathbin{\triangleright}f):(S\mathbin{\triangleright}P\mathord{/}G)% \rightharpoonup(T\mathbin{\triangleright}Q\mathord{/}H)$ consists of a map of shapes $u:S\to T$ , a map of positions $f:\prod_{s:S}Q_{us}\to P_{s}$ , and a proof that $f$ preserves symmetries, $\prod_{s:S}\prod_{g:G_{s}}\operatorname*{\vphantom{\sum}\mathchoice{\vbox{% \hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{\vbox{% \hbox{$\exists$}}}}_{h:H_{us}}g\circ f_{s}=f_{s}\circ h$ .

Morphisms of quotient containers are defined up to permutation of positions, i.e. as equivalence classes of premorphisms.

Definition 6.

The type of morphisms $F\to G$ of quotient containers is the set quotient of the type of premorphisms $F\rightharpoonup G$ by the relation (defined by path induction)

\displaystyle(u\mathbin{\triangleright}f)\mathrel{\approx}(u^{\prime}\mathbin{% \triangleright}f^{\prime})

\displaystyle\mathrel{:=}\sum_{p:u=u^{\prime}}f\mathrel{\approx}^{\prime}_{p}f% ^{\prime},

\displaystyle f\mathrel{\approx}^{\prime}_{\operatorname{\mathsf{refl}}_{u}}f^% {\prime}

\displaystyle\mathrel{:=}\prod_{s:S}\operatorname*{\vphantom{\sum}\mathchoice{% \vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{\vbox{\hbox{$\exists$}}}{% \vbox{\hbox{$\exists$}}}}_{h:H_{us}}f_{s}=f^{\prime}_{s}\circ h

\lrcorner

Whenever $u\mathrel{\doteq}u^{\prime}$ , this relation posits the mere existence of a triangle filler

(u\mathbin{\triangleright}f)\mathrel{\approx}(u\mathbin{\triangleright}f^{% \prime})\quad\simeq\quad\begin{matrix}\includegraphics{dagpub-standalone-% combined-2025-05-20-15-53-28-page-1.pdf2svg.svg}\end{matrix}

Definition 7.

Quotient containers and their morphisms form a category $\mathsf{QuotCont}$ .

Extension of quotient containers is a functor $\llbracket-\rrbracket_{/}:\mathsf{QuotCont}\to\operatorname{\mathsf{Endo}}(% \operatorname{\mathsf{hSet}})$ , which is full and faithful. Each premorphism $(u\mathbin{\triangleright}f):F\rightharpoonup G$ defines a natural transformation $\llbracket u\mathbin{\triangleright}f\rrbracket_{/}:\llbracket F\rrbracket_{/}% \Rightarrow\llbracket G\rrbracket_{/}$ , with component at $X:\operatorname{\mathsf{hSet}}$ a map

\llbracket u\mathbin{\triangleright}f\rrbracket_{/}^{X}:\sum_{s:S}(P_{s}\to X/% {\sim_{s}})\to\sum_{t:T}(Q_{t}\to X/{\sim_{t}})

defined by induction on set quotients as $\llbracket u\mathbin{\triangleright}f\rrbracket_{/}^{X}(s,[\ell])\mathrel{:=}(% us,[\ell\circ f])$ . This is well-defined on morphisms of quotient containers: If $(u\mathbin{\triangleright}f)\mathrel{\approx}(u^{\prime}\mathbin{% \triangleright}f^{\prime})$ then $\llbracket u\mathbin{\triangleright}f\rrbracket_{/}^{X}=\llbracket u^{\prime}% \mathbin{\triangleright}f^{\prime}\rrbracket_{/}^{X}$ .

2.2 Symmetric Containers

Symmetric containers were introduced by Gylterud [10] as a way of defining polynomial functors between categorical groupoids. In this section we reformulate their definition in the language of HoTT using homotopy groupoids instead.

Definition 8.

A symmetric container $(S\mathbin{\triangleleft}P)$ consists of shapes $S:\operatorname{\mathsf{hGpd}}$ and a family of positions $P:S\to\operatorname{\mathsf{hSet}}$ .

Definition 9.

A morphism of symmetric containers $(u\mathbin{\triangleleft}f):(S\mathbin{\triangleleft}P)\to(T\mathbin{% \triangleleft}Q)$ consists of a map of shapes $u:S\to T$ and a family $f:\prod_{s:S}Q_{us}\to P_{s}$ of maps of positions.

In a (homotopy) type-theoretic setting, the types of morphisms $\mathsf{C}(x,y)$ of a category $\mathsf{C}$ are understood to be $h$ -sets. Morphisms of symmetric containers, however, form $h$ -groupoids.¹¹1 Observe that $(S\mathbin{\triangleleft}0)\to(T\mathbin{\triangleleft}0)\simeq(S\to T)$ , which is an $h$ -groupoid since $T$ is.

Definition 10.

The 2-category $\mathsf{SymmCont}$ has as objects symmetric containers, as 1-cells morphisms of symmetric containers, and as 2-cells identifications of such morphisms.

Definition 11.

The extension of a symmetric container $(S\mathbin{\triangleleft}P)$ is a function of $h$ -groupoids, $\llbracket S\mathbin{\triangleleft}P\rrbracket:\operatorname{\mathsf{hGpd}}\to% \operatorname{\mathsf{hGpd}}$ , defined as $\llbracket S\mathbin{\triangleleft}P\rrbracket(X)\mathrel{:=}\sum_{s:S}P_{s}\to X$ .

Extension of symmetric containers defines a 2-functor $\llbracket-\rrbracket:\operatorname{\mathsf{Symm}}\to\operatorname{\mathsf{% Endo}}(\operatorname{\mathsf{hGpd}})$ . For any morphism $(u\mathbin{\triangleleft}f):(S\mathbin{\triangleleft}P)\to(T\mathbin{% \triangleleft}Q)$ , there is a pseudonatural transformation $\llbracket u\mathbin{\triangleleft}f\rrbracket:\llbracket S\mathbin{% \triangleleft}P\rrbracket\Rightarrow\llbracket T\mathbin{\triangleleft}Q\rrbracket$ with components given by precomposition

\displaystyle\llbracket u\mathbin{\triangleleft}f\rrbracket_{X}

\displaystyle:\sum_{s:S}(P_{s}\to X)\to\sum_{t:T}(Q_{t}\to X)

\displaystyle\llbracket u\mathbin{\triangleleft}f\rrbracket_{X}(s,v)

\displaystyle\mathrel{:=}(us,Q_{us}\xrightarrow{f_{s}}P_{s}\xrightarrow{v}X)

This 2-functor is locally an equivalence of 2-categories [10, Theorem 2.2.1], thus embeds symmetric containers into endofunctors of groupoids.

One advantage of internalizing symmetric containers as $h$ -groupoids is that we are free to define groupoids of shapes as higher inductive types, encoding the desired symmetries directly in their constructors. For example, cyclic lists can be described using the symmetries of the circle, $S^{1}$ :

Example 12.

The symmetric container of cyclic lists, $\operatorname{\mathsf{Cyc}}$ , is defined as follows:

$\blacksquare$

Shapes are pairs $\mathbb{N}\times S^{1}$ . The first component contains the length of the list. The second has a single point, $\operatorname{\mathsf{base}}:S^{1}$ , but its loops $\operatorname{\mathsf{base}}=\operatorname{\mathsf{base}}$ are going to induce cyclic shifts on positions.
$\blacksquare$

Positions $\operatorname{\mathsf{Sh}}:\mathbb{N}\times S^{1}\to\operatorname{\mathsf{hSet}}$ are defined by induction on the circle $S^{1}$ . Over the point, we have $n$ distinct positions, $\operatorname{\mathsf{Sh}}(n,\operatorname{\mathsf{base}})\mathrel{:=}% \operatorname{\mathsf{Fin}}(n)$ . On the non-trivial path, $\operatorname{\mathsf{Sh}}$ identifies positions by a cyclic shift, $\operatorname{\mathsf{Sh}}(\operatorname{\mathsf{refl}}_{n},\operatorname{% \mathsf{loop}})\mathrel{:=}\operatorname{\mathsf{shift}}$ . Here, $\operatorname{\mathsf{shift}}:\operatorname{\mathsf{Fin}}(n)=\operatorname{% \mathsf{Fin}}(n)$ is the path obtained by univalence from the successor equivalence

$\displaystyle\operatorname{\mathsf{suc}}$ $\displaystyle:\operatorname{\mathsf{Fin}}(n)\simeq\operatorname{\mathsf{Fin}}(n)$

$\displaystyle\operatorname{\mathsf{suc}}(k)$ $\displaystyle\mathrel{:=}(k+1)\mod n$

Since $S^{1}$ is freely generated by a single non-trivial path, $\operatorname{\mathsf{Sh}}$ identifies positions by arbitrary cyclic shifts. Let $v\mathrel{:=}(x,y,z)$ , $w\mathrel{:=}(y,z,x)$ terms of type $\operatorname{\mathsf{Fin}}(3)\to X$ . We are going to exhibit a path $\big{(}(3,\operatorname{\mathsf{base}}),v\big{)}=\big{(}(3,\operatorname{% \mathsf{base}}),w)$ in $\llbracket\operatorname{\mathsf{Cyc}}\rrbracket(X)$ . Since $\llbracket\operatorname{\mathsf{Cyc}}\rrbracket(X)$ is an iterated $\Sigma$ -type, such a path is given by a triple of paths $p:3=3$ , $q:\operatorname{\mathsf{base}}=\operatorname{\mathsf{base}}$ , and $r:v=_{q}w$ . Set $p\mathrel{:=}\operatorname{\mathsf{refl}}$ and $q\mathrel{:=}\operatorname{\mathsf{loop}}\cdot\operatorname{\mathsf{loop}}$ . The path $r$ is dependent over $q$ , and it suffices to give a path $v=w\circ\operatorname{\mathsf{shift}}\circ\operatorname{\mathsf{shift}}$ . But we see that the right side computes to $(x,y,z)$ , which is $v$ .

2.3 Lifting Quotient Containers

The data of both quotient and symmetric containers define semantics for datatypes with symmetries. As we will see, it is possible to see any quotient container as a symmetric one. However, this analogy does not extend to (polymorphic) functions between such types, since it is generally not possible to lift a morphism of quotient containers to one of symmetric containers, as the former truncate evidence on how symmetries are preserved.

In order to create a symmetric container from a quotient container, we have to come up with a groupoid of shapes that encodes the symmetries present in the quotient container. We borrow an idea from algebraic topology: any group $G$ gives rise to a unique pointed, connected groupoid $(\mathbf{B}{}{G},\mathord{\bullet})$ such that $\operatorname{\Omega}(\mathbf{B}{}{G},\mathord{\bullet})\simeq G$ , called its delooping. This type is an instance of an Eilenberg–MacLane space, i.e. a type with a single non-trivial homotopy group. Eilenberg–MacLane spaces have been studied in HoTT [16], and our presentation of $\mathbf{B}{}{G}$ coincides with $K(G,1)$ there. We define $\mathbf{B}{}{G}$ as a higher inductive type with constructors

plus one constructor asserting that $\mathbf{B}{}{G}$ is an $h$ -groupoid. Its recursion principle states that, to define a map $\mathbf{B}{}{G}\to X$ for some groupoid $X$ , it suffices to give a point $x_{0}:X$ and a group homomorphism $\varphi:G\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.2}{% \kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}\operatorname{\Omega}{(X,x_% {0})}$ : a map $f:\mathbf{B}{}{G}\to X$ is then determined by $f(\mathord{\bullet})\mathrel{:=}x_{0}$ and $f(\operatorname{\mathsf{loop}}{g})\mathrel{:=}\varphi(g)$ . The recursor characterizes functions out of $\mathbf{B}{}{G}$ , in the following sense:

Proposition 13.

The recursor is an equivalence $\cramped{(\sum_{x_{0}:X}G\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil% \cr\scalebox{1.2}{\kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}% \operatorname{\Omega}{(X,x_{0})})}\simeq(\mathbf{B}{}{G}\to X)$ , for $X$ a groupoid. When $X$ is a set, we have $(\cramped{\sum_{x_{0}:X}G\to x_{0}=x_{0}})\simeq(\mathbf{B}{}{G}\to X)$ .

The dependent eliminator lets us define sections $\prod_{x:\mathbf{B}{}{G}}B(x)$ of families ${B:\mathbf{B}{}{G}\to\operatorname{\mathsf{hGpd}}}$ by providing a point $b_{0}:B(\mathord{\bullet})$ , dependent paths $\varphi:\prod_{g:G}(b_{0}\mathrel{=_{B(\operatorname{\mathsf{loop}}{g})}}b_{0})$ , and a coherence condition for composition of dependent paths: for all $g, h : G$ , there needs to be a path from $\varphi(g)\cdot\varphi(h)$ to $\varphi(gh)$ , dependent over $\operatorname{\mathsf{loop-comp}}(g,h)$ .

Note that $\operatorname{\mathsf{loop-comp}}:G\to\operatorname{\Omega}(\mathbf{B}{}{G},% \mathord{\bullet})$ preserves the product of $G$ , hence is a morphism of groups. This lets us derive other expected coherences, such as $\operatorname{\mathsf{loop}}{1_{G}}=\operatorname{\mathsf{refl}}$ and $\cramped{\operatorname{\mathsf{loop}}{(g^{\shortminus 1})}=(\operatorname{% \mathsf{loop}}{g})^{\shortminus 1}}$ .

Delooping acts on group homomorphisms:

Definition 14.

Any group homomorphism $\varphi:G\to H$ induces a map of groupoids $\mathbf{B}{}{\varphi}:\mathbf{B}{}{G}\to\mathbf{B}{}{H}$ , defined by induction:

\displaystyle\mathbf{B}{}{\varphi}(\mathord{\bullet})

\displaystyle\mathrel{:=}\mathord{\bullet},

\displaystyle\mathbf{B}{}{\varphi}(\operatorname{\mathsf{loop}}{g})

\displaystyle\mathrel{:=}\operatorname{\mathsf{loop}}{\varphi(g)}

A $G$ -action is a particular homomorphism, so the above defines a type family $\mathbf{B}{}{G}\to\operatorname{\mathsf{hSet}}$ . Let us spell this out:

Definition 15 (associated bundle).

Let $G$ act on a set $X$ via $\sigma:G\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.2}{% \kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}\operatorname{\mathfrak{S}}% (X)$ . Its associated bundle $\mathbf{\bar{B}}{}{\sigma}:\mathbf{B}{}{G}\to\operatorname{\mathsf{hSet}}$ is defined by recursion on $\mathbf{B}{}{G}$ as

\displaystyle\mathbf{\bar{B}}{}{\sigma}(\mathord{\bullet})

\displaystyle\mathrel{:=}X,

\displaystyle\mathbf{\bar{B}}{}{\sigma}(\operatorname{\mathsf{loop}}{g})

\displaystyle\mathrel{:=}\sigma(g),

Note that for each $g : G$ , $\sigma(g)$ is a path $X=X$ .

In the context of quotient containers, we are dealing with faithful group actions, that is actions of $G$ on $X$ such that ${\sigma:G\to\operatorname{\mathfrak{S}}(X)}$ is an embedding. In this case, the associated bundle is an embedding on its path spaces, i.e. a set-truncated function [20, 7.6.1]:

Proposition 16.

If $\sigma:G\hookrightarrow\operatorname{\mathfrak{S}}(X)$ acts faithfully, the fibers of $\mathbf{\bar{B}}{}{\sigma}:\mathbf{B}{}{G}\to\operatorname{\mathsf{hSet}}$ are sets.

Proof.

By [20, Lemma 7.6.2], $\mathbf{\bar{B}}{}{\sigma}$ has set-valued fibers iff $\operatorname{\mathsf{cong}}\mathbf{\bar{B}}{}{\sigma}:x=y\to\mathbf{\bar{B}}{% }{\sigma}(x)=\mathbf{\bar{B}}{}{\sigma}(y)$ is an embedding for all $x,y:\mathbf{B}{}{G}$ . This is a proposition, therefore it suffices to show this at $x\mathrel{\doteq}y\mathrel{\doteq}\mathord{\bullet}$ . There, we have $\operatorname{\mathsf{cong}}(\mathbf{\bar{B}}{}{\sigma})\circ\operatorname{% \mathsf{loop}}{}\mathrel{\doteq}\sigma$ . But $\operatorname{\mathsf{loop}}{}:G\to\mathord{\bullet}=\mathord{\bullet}$ is an equivalence and $\sigma$ an embedding, hence $\operatorname{\mathsf{cong}}\mathbf{\bar{B}}{}{\sigma}$ is an embedding as well. $\hfill\blacktriangleleft$

For any quotient container we define a groupoid that is the collection of its delooped symmetry groups:

Definition 17.

The delooping of a quotient container $(S\mathbin{\triangleright}P\mathord{/}G)$ is the symmetric container $\mathbf{B}{}{(S\mathbin{\triangleright}P\mathord{/}G)}\mathrel{:=}(\mathbf{S}% \mathbin{\triangleleft}\mathbf{P})$ consisting of

$\blacksquare$

shapes $\mathbf{S}\mathrel{:=}\sum_{s:S}\mathbf{B}{}{G_{s}}$ , and
$\blacksquare$

positions $\mathbf{P}:\sum_{s:S}\mathbf{B}{}{G_{s}}\to\operatorname{\mathsf{hSet}}$ , $\mathbf{P}(s,-)\mathrel{:=}\mathbf{\bar{B}}{}{(\iota_{s})}$ ,

where $\iota_{s}$ is the inclusion of symmetry groups $G_{s}\hookrightarrow\operatorname{\mathfrak{S}}(X)$ .

We think of the shapes $\mathbf{S}$ as consisting of the points of $S$ , with loops given by elements in $G_{s}$ freely added. Indeed, if we compute its connected components, we see that

\displaystyle\operatorname{\pi_{0}}(\mathbf{S})\simeq{\textstyle\lVert\sum_{s:% S}\mathbf{B}{}{G_{s}}\rVert_{0}}\simeq{\textstyle\sum_{s:S}\lVert\mathbf{B}{}{% G_{s}}\rVert_{0}}\simeq S

where the last step follows from connectivity of $\mathbf{B}{}{G_{s}}$ . Similarly, we compute its first fundamental group: $S$ is a set and $s=s$ is contractible, thus

\displaystyle\operatorname{\pi_{1}}(\mathbf{S},(s,x))\simeq{\textstyle\sum_{p:% s=s}(x\mathrel{=_{p}}x)}\simeq(x=x)\simeq\operatorname{\pi_{1}}(\mathbf{B}{}{G% _{s}},x)\simeq G_{s}

That each $G_{s}$ acts faithfully is reflected in the action of the groupoid $\mathbf{S}$ , in the sense that the bundle $\mathbf{P}$ embeds paths of $\mathbf{S}$ :

Proposition 18.

The family $\mathbf{P}:\mathbf{S}\to\operatorname{\mathsf{hSet}}$ is a set-truncated function.

Proof.

For each $X:\operatorname{\mathsf{hSet}}$ , we have $\operatorname{\mathsf{fiber}}_{\mathbf{P}}X\simeq\sum_{s:S}\operatorname{% \mathsf{fiber}}_{\mathbf{\bar{B}}{}{\iota_{s}}}X$ , which is a set: $S$ is a set, and since we assume $\iota_{s}$ to be faithful, so are the fibers of $\mathbf{\bar{B}}{}{\iota_{s}}$ by Proposition 16. $\hfill\blacktriangleleft$

This way of obtaining a symmetric container is in some sense conservative: when comparing the associated extensions (and set-truncating that of the symmetric container), we see that they are the same function of sets:

Theorem 19.

For a quotient container $Q$ and $X:\operatorname{\mathsf{hSet}}$ , there is an equivalence of sets

\lVert\,\llbracket\mathbf{B}{}{Q}\rrbracket(X)\,\rVert_{0}\simeq\llbracket Q% \rrbracket_{/}(X)

Proof.

Let us unfold the definitions of $\llbracket-\rrbracket$ and $\mathbf{B}{}$ ,

	$\displaystyle\lVert\,\llbracket\mathbf{B}{}{Q}\rrbracket(X)\,\rVert_{0}$	$\displaystyle\simeq\left\lVert{\,\textstyle\sum_{s:S}\sum_{x:\mathbf{B}{}{G_{s% }}}\mathbf{\bar{B}}{}{\iota_{s}}(x)\to X\,}\right\rVert_{0}$	(1)
and, as $S$ is a set, move the truncation under the sum
		$\displaystyle\simeq{\textstyle\sum_{s:S}\left\lVert{\,\sum_{x:\mathbf{B}{}{G_{% s}}}\mathbf{\bar{B}}{}{\iota_{s}}(x)\to X\,}\right\rVert_{0}}$	(2)
Notice that $G_{s}$ acts on the function type $P_{s}\to X$ via precomposition, and that its associated bundle is $(\mathbf{\bar{B}}{}{\iota_{s}}(-)\to X):\mathbf{B}{}{G_{s}}\to\operatorname{% \mathsf{hSet}}$ . By Lemma 20 below, the connected components of this bundle correspond to orbits of the action,
		$\displaystyle\simeq\sum_{s:S}(P_{s}\to X)/G_{s}$	(3)
which is exactly how extension of a quotient container is defined:
		$\displaystyle\simeq{\sum_{s:S}(P_{s}\to X)/{\sim_{s}}}\simeq\llbracket Q% \rrbracket_{/}(X)\$	(4)

$\hfill\blacktriangleleft$

Lemma 20.

Let $\sigma$ a $G$ -action on $X$ . The connected components of the total space of its associated bundle and $\sigma$ -orbits are in bijection, that is $\lVert\,\sum_{x:\mathbf{B}{}{G}}\mathbf{\bar{B}}{}{\sigma}(x)\,\rVert_{0}% \simeq X/G$ .

Proof.

Let us define the left-to-right direction. Since the codomain is a set, it suffices to give $f:\prod_{x:\mathbf{B}{}{G}}\mathbf{\bar{B}}{}{\sigma}(x)\to X/G$ by induction on $\mathbf{B}{}{G}$ . Let $f(\mathord{\bullet})\mathrel{:=}[-]:X\to X/G$ the surjection onto the quotient. It remains to show that this is well-defined on loops, which reduces to $\prod_{g:G}\prod_{x:X}[x]=[\sigma_{g}(x)]$ . This holds since $x\sim\sigma_{g}(x)$ by definition of the orbit relation. The inverse is defined by recursion on the set quotient $X/G$ and maps $x : X$ to $(\mathord{\bullet},x):\sum_{x:\mathbf{B}{}{G}}\mathbf{\bar{B}}{}{\sigma}(x)$ . From $p:x=\sigma_{g}(y)$ , one constructs a path $(\mathord{\bullet},x)=(\mathord{\bullet},y)$ : the first component is given by $\operatorname{\mathsf{loop}}{g}$ , the second as dependent path from $p$ . $\hfill\blacktriangleleft$

Theorem 19 states that, as functions between types, the diagram commutes. We are interested to see whether this generalizes to a natural isomorphism of functors. To do so, we would have to suitably extend $\mathbf{B}{}{}$ to a functor. Unfortunately, it is not clear how to define its action on morphisms of quotient containers. Given a premorphism $(u\mathbin{\triangleright}f):(S\mathbin{\triangleright}P\mathord{/}G)% \rightharpoonup(T\mathbin{\triangleright}Q\mathord{/}H)$ , we would have to provide a morphism of shapes

	$\displaystyle{\textstyle\sum_{s:S}\mathbf{B}{}{G_{s}}}$	$\displaystyle\to{\textstyle\sum_{t:T}\mathbf{B}{}{H_{t}}}$
	$\displaystyle(s,x)$	$\displaystyle\mapsto(us,?)$

To define $?:\mathbf{B}{}{G_{s}}\to\mathbf{B}{}{H_{us}}$ , it would suffice to provide a morphism of groups $G_{s}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.2}{% \kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}H_{us}$ . However, we are not given this information: we know that $f$ preserves symmetries, but this only tells us that, for each $g:G_{s}$ , there is merely some $h:H_{us}$ . Even if we were given an explicit function $G_{s}\to H_{us}$ , it would not have to be a group homomorphism. In fact, it is easy to construct counterexamples:

Example 21.

Consider $(\operatorname{\mathsf{id}}\mathbin{\triangleright}{!}):\operatorname{\mathsf{% U}}_{1}\rightharpoonup\operatorname{\mathsf{U}}_{2}$ . The terminal map ${!}:2\to 1$ trivially preserves symmetries: the diagram

commutes for any choice of $\varphi_{g}$ , in particular for $\varphi:\operatorname{\mathfrak{S}}(1)\to\operatorname{\mathfrak{S}}(2),% \varphi_{-}\mathrel{:=}\operatorname{\mathsf{swap}}$ , which is not a group homomorphism.

Since morphisms of quotient containers are equivalence classes, it might be possible to find another premorphism in the same class for which this assignment is a morphism of groups. In fact, in the above example one could pick $\varphi_{g}\mathrel{:=}\operatorname{\mathsf{id}}$ , which clearly is. Doing so however for arbitrary symmetry groups seems constructively impossible, without invoking some form of choice principle.

Instead, we will be looking to enhance the definition of quotient containers to include the necessary information, and investigate their relation to symmetric containers more closely.

3 Action Containers

In this section we define action containers and assemble them into a 1-category. Morphisms in this category are akin to premorphisms of quotient containers. In particular, they are not quotiented by a relation on positions. Later, in Section 4, we enrich this category to obtain a (2,1)-category whose 2-cells capture this relation.

Different from quotient containers, the symmetries of action containers are not limited to subgroups of permutations of positions. Instead, an action container has, for each shape, a chosen group acting on the set of positions. This lets us flexibly introduce symmetries, e.g. by letting the integers under addition act on a finite set, instead of having to identify the image of this action, see the forthcoming Example 23.

The category of action containers admits a number of limits and colimits, and we will derive the usual container algebra of products and coproducts from a presentation of this category as a category of families in Section 3.1.

Definition 22.

An action container $(S\mathbin{\triangleright}P\mathbin{\triangleleft^{\sigma}}G)$ consists of a set of shapes $S$ , a family of positions $P:S\to\operatorname{\mathsf{hSet}}$ and group actions $\sigma_{s}:G_{s}\to\operatorname{\mathfrak{S}}(P_{s})$ for each $s : S$ .

In the following, the word “container” refers to action containers; other kinds of containers are qualified explicitly. In Example 12, we defined cyclic lists as a symmetric container in which loops of the circle act by cyclic shifts. Since $\operatorname{\Omega}(S^{1})=\mathbb{Z}$ , we are inspired to define a container of cyclic lists by means of a $\mathbb{Z}$ -action:

Example 23 (cyclic lists as an action container).

The container $\operatorname{\mathsf{Cyc}}\mathrel{:=}(ℕ\mathbin{\triangleright}\operatorname% {\mathsf{Fin}}\mathbin{\triangleleft^{\sigma}}\mathbb{Z})$ has $\mathbb{Z}$ acting on $\operatorname{\mathsf{Fin}}(n)$ as follows: for each $n$ , let $\sigma_{n}:\mathbb{Z}\to\operatorname{\mathfrak{S}}(n)$ , $\sigma_{n}(k)\mathrel{:=}\lambda\ell.\,(\ell+k)\mod n$ . Note that this action is not faithful: the kernel of $\sigma_{n}$ consists of the integers $n\mathbb{Z}=\{\,nk\mid k\in\mathbb{Z}\,\}$ .

In general, it is easy to define $\mathbb{Z}$ -actions: $\mathbb{Z}$ is the free group on one generator, thus it suffices to define the action of $1:\mathbb{Z}$ . In the example of cyclic lists, it suffices to define the cyclic shift by one position, $\sigma_{n}(1)\mathrel{:=}\lambda\ell\mathpunct{.}(\ell+1)\mod n$ . This is impossible for quotient containers with finitely many positions: $\mathbb{Z}$ is simply never a subgroup of finite symmetry groups.

Unlike premorphisms of quotient containers, morphism of action containers are required to preserve the full structure of containers, including their symmetries:

Definition 24.

A morphism of action containers $(u\mathbin{\triangleright}f\mathbin{\triangleleft}\varphi):(S\mathbin{% \triangleright}P\mathbin{\triangleleft^{\sigma}}G)\to(T\mathbin{\triangleright% }Q\mathbin{\triangleleft^{\tau}}H)$ consists of a map of shapes $u:S\to T$ , a map of positions $f:\prod_{s:S}Q_{us}\to P_{s}$ , a family of group homomorphisms $\varphi:\prod_{s:S}G_{s}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr% \scalebox{1.2}{\kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}H_{us}$ , and a proof that $f$ is equivariant: for all $s : S$ and $g:G_{s}$ a commutative square

Calling $f$ equivariant is justified: each $f_{s}$ is a morphism between $G_{s}$ -sets $(P_{s},\sigma_{s})$ and $(Q_{us},\tau_{us}\circ\varphi_{s})$ [18, Definition 1.2]. Theorem 27 will explain how this notion of morphism arises naturally from a category of group actions and equivariant maps between them.

Definition 25.

Action containers and their morphisms form a category $\mathsf{ActCont}$ .

3.1 Algebra of Action Containers

Like other categories of containers, action containers are closed under a number of constructions. In particular, $\mathsf{ActCont}$ has all products and coproducts. To show this, we could define each of them by hand. In that process, we would have to carefully track the variance of parts of a container. For example, the binary product of containers is a product of shapes and symmetry groups, but a (pointwise) coproduct of families of positions.

Instead, we opt to present $\mathsf{ActCont}$ as a category of families of group actions, from which (co)limits are easy to read off. First, we define a category of group actions. It is a version of the category of $G$ -sets (for a fixed group $G$ ), in which equivariant maps are permitted to go between sets with actions of different groups.

Definition 26.

We denote by $\operatorname{\mathsf{Action}}$ the category of group actions and equivariant maps. It is obtained as the total category of the following category displayed over $\operatorname{\mathsf{Group}}\times\operatorname{\mathsf{hSet}}^{\operatorname% {\mathbf{op}}}$ :

$\blacksquare$

Given objects $G:\operatorname{\mathsf{Group}}_{0}$ and $X:\operatorname{\mathsf{hSet}}_{0}^{\operatorname{\mathbf{op}}}$ , displayed objects are $G$ -actions on $X$ , i.e. group homomorphisms $\operatorname{\mathsf{Action}}_{0}(G,X)\mathrel{:=}(G\mathrel{\vbox{% \offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.2}{\kern-1.07639pt{.}}\cr% \kern 0.43057pt\cr$\to$\cr}}}\operatorname{\mathfrak{S}}(X))$ .
$\blacksquare$

Displayed morphisms between actions $\sigma:\operatorname{\mathsf{Action}}_{0}(G,X)$ and $\tau:\operatorname{\mathsf{Action}}_{0}(H,Y)$ over $(\varphi:G\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.2}% {\kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}H,f:X\leftarrow Y)$ are proofs of the proposition “ $f$ is equivariant over $\varphi$ ”: Let $\operatorname{\mathsf{Action}}_{1}((\varphi,f);\sigma,\tau)\mathrel{:=}% \operatorname{\mathsf{isEquivariant}}_{\varphi,f}(\sigma,\tau)\mathrel{:=}% \prod_{g:G}\sigma(g)\circ f=f\circ\tau(\varphi g)$ .

Diagrammatically, equivariant maps compose by horizontal pasting of proofs of equivariance:

\begin{matrix}\includegraphics{dagpub-standalone-combined-2025-05-20-15-53-28-% page-5.pdf2svg.svg}\end{matrix}\mathbin{;}\begin{matrix}\includegraphics{% dagpub-standalone-combined-2025-05-20-15-53-28-page-6.pdf2svg.svg}\end{matrix}% \mathrel{:=}\begin{matrix}\includegraphics{dagpub-standalone-combined-2025-05-% 20-15-53-28-page-7.pdf2svg.svg}\end{matrix}

Observe how over each shape, the data of a container $(S\mathbin{\triangleright}P\mathbin{\triangleleft^{\sigma}}G)$ is exactly that of a group action: for any $s : S$ , $G_{s}$ acts on $P_{s}$ via $\sigma_{s}$ . Thus, on objects, the category of action containers consists of “families” of group actions. Let us ensure that this analogy extends to morphisms of this category.

Recall that for any category $\mathcal{C}$ , its free coproduct completion is the category of families $\operatorname{Fam}(\mathcal{C})$ [4, §2]. Its objects are families $\sum_{I:\operatorname{\mathsf{hSet}}}I\to\mathcal{C}_{0}$ , morphisms are families of maps between them.

Theorem 27.

The category of action containers is equivalent to families of group actions. In particular, the functor $\mathsf{F}:\mathsf{ActCont}\to\operatorname{Fam}(\operatorname{\mathsf{Action}})$ with action on objects given by $\mathsf{F}(S\mathbin{\triangleright}P\mathbin{\triangleleft^{\sigma}}G)% \mathrel{:=}(S,\lambda s.\,(G_{s},P_{s},\sigma_{s}))$ is an equivalence of categories.

$\blacktriangleright$ Remark (univalence of $\mathsf{ActCont}$ ).

The above implies that $\mathsf{ActCont}$ is a univalent category: $\operatorname{Fam}$ preserves univalence, and $\operatorname{\mathsf{Action}}$ is a univalent displayed category by [7, Proposition 7.3].

From this presentation of $\mathsf{ActCont}$ , we read off closure under sums and products:

Proposition 28.

$\operatorname{\mathsf{Action}}$ has $K$ -indexed products for all sets $K$ . In particular, the trivial group acting on the singleton set is an initial object.

Corollary 29.

Action containers are closed under products and coproducts.

Proof.

$\operatorname{Fam}(\mathcal{C})$ is the free coproduct completion of any category $\mathcal{C}$ , thus $\mathsf{ActCont}$ is closed under coproducts. Similarly, $\operatorname{\mathsf{Action}}$ is closed under products (Proposition 28), and Theorem 2.11 of [4] implies that families over it are as well. $\hfill\blacktriangleleft$

Like ordinary containers [2, Proposition 3.9], constant action containers are exponentiable:

Proposition 30 (constant containers are exponentiable).

The constant container of a set $K$ is $\mathbf{k}K\mathrel{:=}(K\mathbin{\triangleright}0\mathbin{\triangleleft^{% \operatorname{id}}}1)$ . Given a container $F=(S\mathbin{\triangleright}P\mathbin{\triangleleft^{\sigma}}G)$ , the exponential container $F^{K}\mathrel{:=}(S^{*}\mathbin{\triangleright}P^{*}\mathbin{\triangleleft^{% \sigma^{*}}}G^{*})$ is defined to have

$\blacksquare$

shapes $S^{*}\mathrel{:=}K\to S$ ,
$\blacksquare$

positions $P^{*}_{f}\mathrel{:=}\sum_{k:K}P_{fk}$ ,
$\blacksquare$

symmetries $G^{*}_{f}\mathrel{:=}\prod_{k:K}G_{fk}$ , and
$\blacksquare$

actions $\sigma^{*}_{f}:G^{*}_{f}\to\operatorname{\mathfrak{S}}(P^{*}_{f})$ given by action of $\sigma$ on the second component of $P^{*}_{f}$ : for $g:\prod_{k}G_{fk}$ , let $\sigma^{*}_{f}(g)\mathrel{:=}\lambda(k,p).\,(k,\sigma_{fk}(g))$

Let $f:K\to S$ and $k : K$ . The evaluation morphism $\operatorname{ev}:F^{K}\times\mathbf{k}K\to F$ is given by function application $f k : S$ on shapes, pairing $P_{fk}\to 0+\sum_{k}P_{fk}$ on positions, and the projection homomorphisms $1\times\prod_{k^{\prime}}G_{fk^{\prime}}\mathrel{\vbox{\offinterlineskip% \halign{\hfil#\hfil\cr\scalebox{1.2}{\kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$% \to$\cr}}}G_{fk}$ on symmetries.

We believe that the above is an instance of constant exponentials in families: Let $\mathsf{C}$ have $K$ -fold products for any set $K$ ; in particular an initial object $1_{\mathsf{C}}$ and binary products. It should be possible to show that the constant family $(K,\lambda k\mathpunct{.}1_{\mathsf{C}})$ is exponentiable.

$\blacktriangleright$ Remark (composition of action containers).

When seen as endofunctors, composite data types are constructed as compositions of functors. For ordinary containers [2, 3.6] and symmetric containers [10, 2.2.5], this construction is reflected along $\llbracket-\rrbracket$ : Given containers $F$ and $G$ , there is a container $F[G]$ such that $\llbracket F[G]\rrbracket\cong\llbracket F\rrbracket\circ\llbracket G\rrbracket$ , upgrading $\llbracket-\rrbracket$ to a strong monoidal functor. In a set-theoretic setting, Hasegawa [11, Corollary 1.18] gives a construction of composition for analytic functors in terms of wreath products of symmetry groups. Analytic functors are presented by quotient containers with finitary positions, and such a restriction of positions to a subuniverse of sets seems necessary when porting the result to action containers: positions and symmetries of the composite can otherwise not be defined coherently by induction on set quotients. This indicates to us that the definition of a composition-monoidal structure of action containers is not entirely straightforward, and we postpone its study for now.

4 The 2-Category of Action Containers

In Section 2.3 we observed that quotient containers lift to symmetric containers, but that the same does not apply to their morphisms. We defined the category of action containers to include the missing data, and are now ready to define an appropriate lifting:

Proposition 31.

The delooping of a container $(S\mathbin{\triangleright}P\mathbin{\triangleleft^{\sigma}}G)$ is the symmetric container $\mathbf{B}{}{(S\mathbin{\triangleright}P\mathbin{\triangleleft^{\sigma}}G)}% \mathrel{:=}(\sum_{s:S}\mathbf{B}{}{G_{s}}\mathbin{\triangleleft}\mathbf{\bar{% B}}{}{\sigma_{s}})$ . Each morphism $(u\mathbin{\triangleright}f\mathbin{\triangleleft}\varphi):(S\mathbin{% \triangleright}P\mathbin{\triangleleft^{\sigma}}G)\to(T\mathbin{\triangleright% }Q\mathbin{\triangleleft^{\tau}}H)$ defines a morphism between deloopings, $(\bar{\varphi}\mathbin{\triangleleft}\bar{f}):\mathbf{B}{}{(S\mathbin{% \triangleright}P\mathbin{\triangleleft^{\sigma}}G)}\to\mathbf{B}{}{(T\mathbin{% \triangleright}Q\mathbin{\triangleleft^{\tau}}H)}$ .

Proof.

The family $\varphi$ yields a map of shapes of type $\bar{\varphi}:{\textstyle\sum_{s:S}\mathbf{B}{}{G_{s}}}\to{\textstyle\sum_{t:T% }\mathbf{B}{}{H_{t}}}$ , defined as $\bar{\varphi}(s,x)\mathrel{:=}(us,\mathbf{B}{}{\varphi_{s}}(x))$ . The map on positions has (uncurried) type

\bar{f}:{\textstyle\prod_{s:S}\prod_{x:\mathbf{B}{}{G_{s}}}\mathbf{\bar{B}}{}{% \tau_{us}}(\mathbf{B}{}{\varphi}(x))\to\mathbf{\bar{B}}{}{\sigma_{s}}(x)}

and is defined by induction on $x:\mathbf{B}{}{G_{s}}$ . On the point, let $\bar{f}(s,\mathord{\bullet})\mathrel{:=}f_{s}:Q_{us}\to P_{s}$ . It remains to show that $\bar{f}$ is well-defined on loops in $\mathbf{B}{}{G_{s}}$ . For all $g$ , we have to provide a dependent path $f_{s}\mathrel{=_{F(\operatorname{\mathsf{loop}}{g})}}f_{s}$ where $F(x)=\mathbf{\bar{B}}{}{\tau_{us}}(\mathbf{B}{}{\varphi}(x))\to\mathbf{\bar{B}% }{}{\sigma_{s}}(x)$ . By [20, Lemma 2.9.6], this is equivalent to giving paths $\prod_{q:Q_{us}}\sigma_{s}(f_{s}(q))=f_{s}((\tau_{us}\varphi_{s}\,g)\,q)$ , which we obtain from the proof that $f_{s}$ is equivariant. $\hfill\blacktriangleleft$

As noted in Section 2.2, symmetric containers do not form an ordinary category, but a 2-category. Thus, in order to show that the above construction is functorial, we must first enrich action containers by a type of 2-cells, defining a 2-category. We do so by pulling back 2-cells of symmetric containers, and will see that this corresponds to the quotiented sets of quotient container morphisms.

We split the construction of the 2-functor taking action containers into symmetric containers into smaller steps. As in Section 3, we first seek to understand the problem for a single action, before considering entire families of such. We observe that symmetric containers, from a homotopical viewpoint, are set-bundles over groupoids: both consist of some base $B:\operatorname{\mathsf{hGpd}}$ together with a family of fibers $F:B\to\operatorname{\mathsf{hSet}}$ . Previously, we have seen that each action defines such a bundle, namely its associated bundle (Definition 15). We define 2-categories of actions ( $\operatorname{\mathsf{Action}}$ , Definition 37) and set bundles (Definition 38), and show that taking the associated bundle is a weak equivalence of their local categories (Theorem 42). This means that maps of actions are in 1-to-1 correspondence with functions on their associated bundles. By changing our point of view, and seeing actions as single-shape containers and bundles as symmetric containers, this fully classifies morphisms of (single-shape) action containers in terms of morphisms of symmetric containers.

To understand the case of many-shape containers, we give an analogue of the $\operatorname{Fam}$ -construction in 2-categories, and define the 2-category of action containers as $\mathsf{ActCont}\mathrel{:=}\operatorname{Fam}(\operatorname{\mathsf{Action}})$ . The objects and 1-cells of this category are exactly as in Definition 26. We unfold the type of 2-cells induced by this construction (Proposition 47) and show that it is closely related to the quotient on premorphisms of quotient containers (Definition 6). We observe that set-bundles are, in a suitable sense, closed under $\Sigma$ -types, and we lift the functor $\mathbf{\bar{B}}{}:\operatorname{\mathsf{Action}}\to\operatorname{\mathsf{% SetBundle}}$ to

finally establishing the connection between action containers and symmetric containers.

4.1 A 2-Category of Groups

We think of the type of $h$ -groupoids, $\operatorname{\mathsf{hGpd}}$ , as an internal notion of categorical groupoids: The 2-category $\operatorname{\mathsf{hGpd}}$ has as objects $h$ -groupoids, as morphisms functions of such, and as 2-cells homotopies between them. Our goal is to extend the delooping to a 2-functor taking groups into $\operatorname{\mathsf{hGpd}}$ in a way that characterizes 2-cells in $\operatorname{\mathsf{hGpd}}$ . We thus equip the 1-category of groups with the structure of a (2,1)-category [12]:

Definition 32.

The category $\operatorname{\mathsf{Group}}$ of groups and group homomorphisms forms a (2,1)-category if equipped with the following 2-cells: Let $\varphi,\psi:\operatorname{\mathsf{Group}}_{1}(G,H)$ . We say that $r : H$ is a conjugator of $\varphi$ and $\psi$ if

\operatorname{\mathsf{isConjugator}}_{\varphi,\psi}(r)\mathrel{:=}\prod_{g:G}% \varphi(g)\cdot r=r\cdot\psi(g)

The 2-cells $\operatorname{\mathsf{Group}}_{2}(\varphi,\psi)\mathrel{:=}\sum_{r:H}% \operatorname{\mathsf{isConjugator}}_{\varphi,\psi}(r)$ compose vertically by multiplication in $H$ . The horizontal composites of $r:\operatorname{\mathsf{Group}}_{2}(\varphi,\psi)$ and $s:\operatorname{\mathsf{Group}}_{2}(\varphi^{\prime},\psi^{\prime})$ is $s\cdot\psi^{\prime}(r)$ .

Note that $\operatorname{\mathsf{Group}}$ is not locally univalent: the identity type of group homomorphisms, $\varphi=\psi$ , is a proposition, but the type of conjugators $\operatorname{\mathsf{Group}}_{2}(\varphi,\psi)$ is a set.

Lemma 33.

Delooping extends to a 2-functor $\mathbf{B}{}:\operatorname{\mathsf{Group}}\to\operatorname{\mathsf{hGpd}}$ .

Proof.

A 1-cell $\varphi:\operatorname{\mathsf{Group}}_{1}(G,H)$ is sent to $\mathbf{B}{}{\varphi}:\mathbf{B}{}{G}\to\mathbf{B}{}{H}$ , as in Definition 14. On 2-cells, let $r:\operatorname{\mathsf{Group}}_{2}(\varphi,\psi)$ a conjugator of homomorphisms. Delooping assigns a 2-cell $\mathbf{B}{}{\varphi}=\mathbf{B}{}{\psi}$ as follows: By function extensionality, it suffices to give $\mathbf{B}{}{\varphi}(x)=\mathbf{B}{}{\psi}(x)$ for any $x:\mathbf{B}{}{G}$ . By induction on $x$ , we are left to give some $q:\mathord{\bullet}=\mathord{\bullet}$ in $\mathbf{B}{}{H}$ such that for all $g : G$ , $\operatorname{\mathsf{loop}}{\varphi(g)}\cdot q=q\cdot\operatorname{\mathsf{% loop}}{\psi(g)}$ . Choose $q\mathrel{:=}\operatorname{\mathsf{loop}}{r}$ , and compute

\displaystyle\operatorname{\mathsf{loop}}{\varphi(g)}\cdot\operatorname{% \mathsf{loop}}{r}=\operatorname{\mathsf{loop}}{(\varphi(g)r)}\mathrel{{\mathop% {=}\limits^{(\ast)}}}\operatorname{\mathsf{loop}}{(r\psi(g))}=\operatorname{% \mathsf{loop}}{r}\cdot\operatorname{\mathsf{loop}}{\psi(g)},

where $(\ast)$ uses that $r$ is a conjugator of $\varphi$ and $\psi$ . By a similar argument, one shows that these assignments preserve composition and identities. $\hfill\blacktriangleleft$

Defined this way, we see that $\mathbf{B}{}$ preserves the local structure of $\operatorname{\mathsf{Group}}$ :

Theorem 34.

The functor $\mathbf{B}{}:\operatorname{\mathsf{Group}}\to\operatorname{\mathsf{hGpd}}$ is locally a weak equivalence of categories, i.e. for all groups $G, H$ , there merely exists an inverse functor $\operatorname{\mathsf{hGpd}}_{1}(\mathbf{B}{}{G},\mathbf{B}{}{H})\to% \operatorname{\mathsf{Group}}_{1}(G,H)$ .

Note that this cannot be strengthened to a full equivalence with explicit inverse: equivalence of categories preserves properties, but $\operatorname{\mathsf{hGpd}}$ is by definition locally univalent, whereas $\operatorname{\mathsf{Group}}$ is not.

We prove Theorem 34 by showing that locally, $\mathbf{B}{}$ is fully faithful and essentially surjective.

Proposition 35.

Delooping is a locally fully faithful functor: For groups $G, H$ , the local functor $\mathbf{B}{}:\operatorname{\mathsf{Group}}_{1}(G,H)\to\operatorname{\mathsf{% hGpd}}_{1}(\mathbf{B}{}{G},\mathbf{B}{}{H})$ is an equivalence of categories.

Proof.

Let $\varphi,\psi:\operatorname{\mathsf{Group}}_{1}(G,H)$ . We establish a chain of equivalences between the sets of 2-cells $\operatorname{\mathsf{Group}}_{2}(\varphi,\psi)$ and $\mathbf{B}{}{\varphi}=\mathbf{B}{}{\psi}$ . Starting from the definition,

	$\displaystyle\operatorname{\mathsf{Group}}_{2}(\varphi,\psi)$	$\displaystyle\simeq\sum_{h:H}\prod_{g:G}\varphi(g)h=h\psi(g)$
we apply the equivalence of groups, $\operatorname{\mathsf{loop}}{}:H\simeq\operatorname{\Omega}(\mathbf{B}{}{H})$ twice
		$\displaystyle\simeq\sum_{h:H}\prod_{g:G}\operatorname{\mathsf{loop}}{\varphi(g% )}\cdot\operatorname{\mathsf{loop}}{h}=\operatorname{\mathsf{loop}}{h}\cdot% \operatorname{\mathsf{loop}}{\psi(g)}$
		$\displaystyle\simeq\sum_{\ell:\operatorname{\Omega}(\mathbf{B}{}{H})}\prod_{g:% G}\operatorname{\mathsf{loop}}{\varphi(g)}\cdot\ell=\ell\cdot\operatorname{% \mathsf{loop}}{\psi(g)}$
By the recursion principle, this is exactly a type of dependent functions out of $\mathbf{B}{}{G}$ , namely
		$\displaystyle\simeq\prod_{x:\mathbf{B}{}{G}}\mathbf{B}{}{\varphi}(x)=\mathbf{B% }{}{\psi}(x)$
which, by function extensionality, is equivalent to
		$\displaystyle\simeq\mathbf{B}{}{\varphi}=\mathbf{B}{}{\psi}$

One verifies that the map underlying this chain is that of Lemma 33. $\hfill\blacktriangleleft$

Proposition 36.

Delooping is a locally essentially surjective functor.

Proof.

Let $G, H$ groups, and $f:\mathbf{B}{}{G}\to\mathbf{B}{}{H}$ a morphism of groupoids. We show the mere existence of some $\varphi:\operatorname{\mathsf{Group}}_{1}(G,H)$ together with an isomorphism $\mathbf{B}{}{\varphi}\cong f$ in the local category $\operatorname{\mathsf{hGpd}}(\mathbf{B}{}{G},\mathbf{B}{}{H})$ . By definition, morphisms in this category are homotopies, and it suffices to exhibit some $h:\prod_{x:\mathbf{B}{}{G}}\mathbf{B}{}{\varphi}(x)=f(x)$ . Since $\mathbf{B}{}{H}$ is a connected groupoid, there merely exists a path $p:f(\mathord{\bullet})=\mathord{\bullet}$ , and conjugation by $p$ induces an equivalence of groups,

	$\displaystyle\operatorname{\mathsf{conj}}(p):\operatorname{\Omega}(\mathbf{B}{% }{H},f(\mathord{\bullet}))$	$\displaystyle\to\operatorname{\Omega}(\mathbf{B}{}{H},\mathord{\bullet})$
	$\displaystyle(q:f(\mathord{\bullet})=f(\mathord{\bullet}))$	$\displaystyle\mapsto p^{\shortminus 1}\cdot q\cdot p$

We define $\varphi$ to be the composite

G\xrightarrow{\operatorname{\mathsf{loop}}{}}\operatorname{\Omega}(\mathbf{B}{% }{G},\mathord{\bullet})\xrightarrow{\operatorname{\mathsf{cong}}(f)}% \operatorname{\Omega}(\mathbf{B}{}{H},f(\mathord{\bullet}))\xrightarrow{% \operatorname{\mathsf{conj}}(p)}\operatorname{\Omega}(\mathbf{B}{}{H},\mathord% {\bullet})\xrightarrow{\operatorname{\mathsf{loop}}^{\shortminus 1}{}}H

By induction on $x:\mathbf{B}{}{G}$ , we show that $\prod_{x:\mathbf{B}{}{G}}\mathbf{B}{}{\varphi}(x)=f(x)$ . On the point, this is given by $p^{\shortminus 1}:\mathord{\bullet}=f(\mathord{\bullet})$ . On loops, we construct $\prod_{g:G}\mathbf{B}{}{\varphi}(\operatorname{\mathsf{loop}}{g})\cdot p^{% \shortminus 1}=p^{\shortminus 1}\cdot f(\operatorname{\mathsf{loop}}{g})$ as follows: let $g : G$ , then $\cramped{\mathbf{B}{}{\varphi}(\operatorname{\mathsf{loop}}{g})\cdot p^{% \shortminus 1}=\operatorname{\mathsf{loop}}{(\operatorname{\mathsf{loop}}^{% \shortminus 1}{(p^{\shortminus 1}\cdot f(\operatorname{\mathsf{loop}}{g})\cdot p% )})}\cdot p^{\shortminus 1}=p^{\shortminus 1}\cdot f(\operatorname{\mathsf{% loop}}{g})}$ $\hfill\blacktriangleleft$

4.2 A 2-Category of Group Actions

Any $G$ -action $\sigma$ comes with an associated bundle, $\mathbf{\bar{B}}{}{\sigma}:\operatorname{\mathsf{loop}}{G}\to\operatorname{% \mathsf{hSet}}$ (Definition 15). Let us define 2-categories of actions and of set bundles, and show that “taking the associated bundle” is a functorial construction.

Definition 37 (2-category of actions).

The 2-category $\operatorname{\mathsf{Action}}$ of group actions displayed over $\operatorname{\mathsf{Group}}$ consists of the following data:

$\blacksquare$

For each group $G$ , objects are $G$ -actions $\operatorname{\mathsf{Action}}_{0}(G)\mathrel{:=}\sum_{X:\operatorname{\mathsf% {hSet}}}G\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr\scalebox{1.2}{% \kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}\operatorname{\mathfrak{S}}% (X)$ .
$\blacksquare$

1-cells between actions $(X,\sigma):\operatorname{\mathsf{Action}}_{0}(G)$ and $(Y,\tau):\operatorname{\mathsf{Action}}_{0}(H)$ over $\varphi:\operatorname{\mathsf{Group}}_{1}(G,H)$ are equivariant maps $\operatorname{\mathsf{Action}}_{1}(\varphi;(G,\sigma),(H,\tau))\mathrel{:=}% \sum_{f:X\leftarrow Y}\operatorname{\mathsf{isEquivariant}}_{\varphi,f}(\sigma% ,\tau),$ where $\operatorname{\mathsf{isEquivariant}}$ is as in Definition 26.
$\blacksquare$

The type of 2-cells between $f:\operatorname{\mathsf{Action}}_{1}(\varphi;(X,\sigma),(Y,\tau))$ and $g:\operatorname{\mathsf{Action}}_{1}(\psi;(X,\sigma),(Y,\tau))$ over a conjugator $r:\operatorname{\mathsf{Group}}_{2}(\varphi,\psi)$ is $\operatorname{\mathsf{Action}}_{2}(r;f,g)\mathrel{:=}(f=g\circ\tau(r))$ . $\lrcorner$

The type of 2-cells says that 1-cells agree up to a permutation of their domain. Since it is a proposition, verifying the axioms of a displayed 2-category reduces to defining some identity- and composite 2-cells. The vertical composite $p\mathbin{\bullet}q:f\Rightarrow_{rs}h$ of 2-cells $p:f\Rightarrow_{r}g$ and $q:g\Rightarrow_{s}h$ , is some identification $f=h\circ\tau(rs)$ . Since $\tau$ is an action, we define the composite as $p\mathbin{\bullet}q\mathrel{:=}\big{(}f\overset{p}{=}g\circ\tau(r)\overset{q}{% =}h\circ{\tau(s)\circ\tau(r)}=h\circ{\tau(rs)}\big{)}$ . Similarly, horizontal composition depends on 2-cells of $\operatorname{\mathsf{Group}}$ being conjugators of group homomorphisms.

Definition 38 (set bundles).

The 2-category of set bundles, displayed over $\operatorname{\mathsf{hGpd}}$ , consists of the following data:

$\blacksquare$

Given $G:\operatorname{\mathsf{hGpd}}_{0}$ , set bundles on $G$ are families $\operatorname{\mathsf{SetBundle}}_{0}(G)\mathrel{:=}G\to\operatorname{\mathsf{% hSet}}$ .
$\blacksquare$

Over $\varphi:\operatorname{\mathsf{hGpd}}_{1}(G,H)$ , morphisms from $X:\operatorname{\mathsf{SetBundle}}(G)$ to $Y:\operatorname{\mathsf{SetBundle}}(H)$ are dependent functions, $\operatorname{\mathsf{SetBundle}}_{1}(\varphi;X,Y)\mathrel{:=}\prod_{g:G}Y(% \varphi g)\to X(g)$
$\blacksquare$

Displayed 2-cells between $f:\operatorname{\mathsf{SetBundle}}_{1}(\varphi;X,Y)$ and $g:\operatorname{\mathsf{SetBundle}}_{1}(\psi;X,Y)$ over a 2-cell $p:\varphi=\psi$ are dependent identifications, $\operatorname{\mathsf{SetBundle}}_{2}(p;f,g)\mathrel{:=}f=_{p}g$ . $\lrcorner$

For an object $(G,F):\operatorname{\mathsf{SetBundle}}_{0}$ in the total category, we call $G$ the base of the bundle, and $F$ its fibers.

We are now ready to show that taking the bundle associated to an action is a well-behaved functorial operation. In particular, each equivariant map of actions induces a morphism between associated bundles:

Definition 39.

Let $\sigma:\operatorname{\mathsf{Action}}(G,X)$ , $\tau:\operatorname{\mathsf{Action}}(H,Y)$ , and $\varphi:\operatorname{\mathsf{Group}}_{1}(G,H)$ . Let $f:Y\leftarrow X$ and $p:\operatorname{\mathsf{isEquivariant}}_{\varphi,f}(\sigma,\tau)$ . The bundle morphism associated to $f$ has type $\mathbf{\bar{B}}{}{f}:\prod_{x:\mathbf{B}{}{G}}\mathbf{\bar{B}}{}{\tau}(% \mathbf{B}{}{\varphi}x)\to\mathbf{\bar{B}}{}{\sigma}(x),$ and is defined using the induction principle of $\mathbf{B}{}{G}$ . On the point it has type $\mathbf{\bar{B}}{}{f}(\mathord{\bullet}):Y\to X$ and is given by $f$ . On a loop, we need to prove that $\mathbf{\bar{B}}{}{\sigma}(\operatorname{\mathsf{loop}}{g})\circ f=f\circ% \mathbf{\bar{B}}{}{\tau}(\mathbf{B}{}{\varphi}(\operatorname{\mathsf{loop}}{g}))$ for all $g : G$ . This reduces to $\sigma(g)\circ f=f\circ\tau(\varphi(g))$ , which is given by $p$ .

Both $\operatorname{\mathsf{Action}}$ and $\operatorname{\mathsf{SetBundle}}$ are total categories, and $\mathbf{B}{}:\operatorname{\mathsf{Group}}\to\operatorname{\mathsf{hGpd}}$ is a 2-functor between their bases. We thus define a 2-functor only on the displayed parts:

Definition 40.

Taking associated bundles is a displayed 2-functor $\mathbf{\bar{B}}{}:\operatorname{\mathsf{Action}}\to_{\mathbf{B}{}}% \operatorname{\mathsf{SetBundle}}$ , consisting of the following data:

$\blacksquare$

On objects, it sends a $G$ -action $\sigma$ to its associated bundle $\mathbf{\bar{B}}{}{\sigma}:\mathbf{B}{}{G}\to\operatorname{\mathsf{hSet}}$ .
$\blacksquare$

On 1-cells, it associates to an equivariant map $f:\operatorname{\mathsf{Action}}_{1}(\varphi;\sigma,\tau)$ its morphism of bundles $\mathbf{\bar{B}}{}{f}:\operatorname{\mathsf{SetBundle}}_{1}(\mathbf{B}{}{% \varphi};\mathbf{\bar{B}}{}{\sigma},\mathbf{\bar{B}}{}{\tau})$ .
$\blacksquare$

Over a 2-cell $r:\operatorname{\mathsf{Group}}_{2}(G,H)$ , a proof $p:\operatorname{\mathsf{Action}}_{2}(r;f,g)\mathrel{\doteq}(f=g\tau(r))$ is sent to a homotopy of bundle maps using the induction principle of $\mathbf{B}{}{G}$ .

Both actions on 1- and 2-cells are defined by induction, and thus are equivalences in the sense of Proposition 13:

Lemma 41.

The action on 1-cells $\mathbf{\bar{B}}{}_{1}:\operatorname{\mathsf{Action}}_{1}(\varphi;\sigma,\tau)% \to\operatorname{\mathsf{SetBundle}}_{1}(\mathbf{B}{}{\varphi};\mathbf{\bar{B}% }{}{\sigma},\mathbf{\bar{B}}{}{\tau})$ and 2-cells $\mathbf{\bar{B}}{}_{2}:\operatorname{\mathsf{Action}}_{2}(r;f,g)\to% \operatorname{\mathsf{SetBundle}}_{2}(\mathbf{B}{}{r};\mathbf{\bar{B}}{}{f},% \mathbf{\bar{B}}{}{g})$ are equivalences of types.

Theorem 42.

Taking associated bundles $\int\mathbf{\bar{B}}{}:\operatorname{\mathsf{Action}}\to\operatorname{\mathsf{% SetBundle}}$ is locally a weak equivalence.

Proof.

The total functor $\int\mathbf{\bar{B}}{}$ is locally fully faithful if $\int_{2}\mathbf{\bar{B}}{}$ is an equivalence, but this is a map on $\Sigma$ -types built from $\mathbf{B}{}_{2}$ and $\mathbf{\bar{B}}{}_{2}$ , which are both equivalences by Theorems 34 and 41. Local essential surjectivity is proved similarly to Proposition 36, and uses that $\mathbf{\bar{B}}{}_{1}$ is an equivalence of types. $\hfill\blacktriangleleft$ The above theorem implies that the local category $\operatorname{\mathsf{SetBundle}}(\mathbf{B}{}{G},\mathbf{B}{}{H})$ is the Rezk completion of $\operatorname{\mathsf{Action}}(G,H)$ . As such the 2-category $\operatorname{\mathsf{SetBundle}}$ should be the local univalent completion of $\operatorname{\mathsf{Action}}$ in the sense of [6, Conjecture 5.6].

4.3 A 2-Categorical $\operatorname{Fam}$ -Construction

In the previous section we have seen how containers with a single action relate to set bundles. To lift this relationship to families of actions, we introduce a 2-categorical $\operatorname{Fam}$ -construction, again employing displayed machinery.

Definition 43 (2-category of families).

Let $C$ be a 2-category. The 2-category $\operatorname{Fam}(C)$ displayed over $\operatorname{\mathsf{hSet}}$ consists of the following data:

$\blacksquare$

For $J:\operatorname{\mathsf{hSet}}_{0}$ , the displayed objects are families of $C$ -objects, $\operatorname{Fam}_{0}(J)\mathrel{:=}J\to C_{0}$ .
$\blacksquare$

Let $J,K:\operatorname{\mathsf{hSet}}_{0}$ and families $X:\operatorname{Fam}_{0}(J)$ , $Y:\operatorname{Fam}_{0}(K)$ . The type of 1-cells displayed over some $\varphi:\operatorname{\mathsf{hSet}}_{1}(J,K)$ is $\operatorname{Fam}_{1}(\varphi;X,Y)\mathrel{:=}\prod_{j:J}C_{1}(X_{j},Y_{% \varphi j})$ .
$\blacksquare$

Displayed 2-cells are a family ${\operatorname{Fam}_{2}:(\varphi=\psi)\to\operatorname{Fam}_{1}(\varphi,X,Y)% \to\operatorname{Fam}_{1}(\psi,X,Y)\to\mathcal{U}}$ defined by path-induction on 2-cells in $\operatorname{\mathsf{hSet}}$ : $\operatorname{Fam}_{2}(\operatorname{\mathsf{refl}}_{\varphi};f,g)\mathrel{:=}% \prod_{j:J}C_{2}(f_{j},g_{j})$

Definition 44.

Any 2-functor $F:\mathsf{C}\to\mathsf{D}$ lifts to a functor $\operatorname{Fam}(F):\operatorname{Fam}(\mathsf{C})\to\operatorname{Fam}(% \mathsf{D})$ . This lifting is defined as a total functor $\operatorname{Fam}(F):\int\nolimits_{{J:\operatorname{\mathsf{hSet}}}}% \operatorname{Fam}(\mathsf{C})(J)\to\int\nolimits_{{J:\operatorname{\mathsf{% hSet}}}}\operatorname{Fam}(\mathsf{D})(J)$ over the identity 2-functor on the base $\operatorname{\mathsf{hSet}}$ .

Proposition 45.

Lifting $F:\mathsf{C}\to\mathsf{D}$ to a 2-functor of families inherits the following properties:

1.

If $F$ is locally fully-faithful, so is $\operatorname{Fam}(F)$ .
2.

If $F$ is locally split-essentially surjective, so is $\operatorname{Fam}(F)$ .
3.

Assuming the axiom of choice for $h$ -sets and that $\mathsf{C}$ is locally strict, if $F$ is locally essentially surjective, so is $\operatorname{Fam}(F)$ .

Proof.

Local fully-faithfulness follows from the pointwise definition of $\operatorname{Fam}_{2}$ : if $\mathsf{C}_{2}(f,g)$ is an equivalence, then so is $\operatorname{Fam}_{2}(\operatorname{\mathsf{refl}};-,-)\mathrel{\doteq}% \lambda f,g\mathpunct{.}\prod_{j}\mathsf{C}_{2}(f_{j},g_{j})$ . Local split essential surjectivity follows from a similar pointwise argument.

In the non-split case, fix $x,y:\operatorname{Fam}_{0}(\mathsf{C})$ , and a 1-cell $(\psi,g):\operatorname{Fam}_{0}(x)\to\operatorname{Fam}_{0}(y)$ . It suffices to provide merely a family of sections, $\lVert\prod_{j:J}\sum_{f}F_{1}(f)\cong g_{j}\rVert_{{\shortminus 1}}$ ; the conclusion follows using the induction principle of the truncation. The assumption that $F$ is locally eso yields $\prod_{j:J}\lVert\sum_{f:\mathsf{C}_{1}(x_{j},y_{\psi j})}F_{1}(f)\cong g_{j}% \rVert_{{\shortminus 1}}$ , and we use choice to move the truncation outward: $J$ is a set, and so are $\mathsf{C}_{1}(x_{j},y_{\psi j})$ (by local strictness of $\mathsf{C}$ ) and local isomorphisms $F_{1}(f)\cong g_{j}$ . $\hfill\blacktriangleleft$

4.4 Action Containers as a 2-Category of Families

As promised, we define the 2-category of action containers as a 2-category of families:

Definition 46 (2-category of action containers).

The 2-category of action containers is that of families of actions, $\mathsf{ActCont}\mathrel{:=}\operatorname{Fam}(\operatorname{\mathsf{Action}})$ .

By algebra of $\Sigma$ - and $\Pi$ -types, we see that the objects and 1-cells coincide with those of the 1-category of action containers (cf. Definition 25). In particular, we have for objects

\displaystyle\mathsf{ActCont}_{0}

\displaystyle\simeq\sum_{S:\operatorname{\mathsf{hSet}}}\sum_{P:S\to% \operatorname{\mathsf{hSet}}}\sum_{G:S\to\operatorname{\mathsf{Group}}}\prod_{% s:S}\operatorname{\mathsf{Action}}(G_{s},P_{s}),

and for 1-cells,

	$\displaystyle\mathsf{ActCont}_{1}((S,\lambda s\mathpunct{.}(P_{s},G_{s},\sigma% _{s})),(T,\lambda t\mathpunct{.}(Q_{t},H_{t},\tau_{t})))$
	$\displaystyle\simeq\sum_{u:S\to T}\prod_{s:S}\sum_{\varphi:G_{s}\to H_{us}}% \smashoperator[r]{\sum_{f:P_{s}\leftarrow Q_{us}}^{}}\,{\operatorname{\mathsf{% isEquivariant}}_{\varphi,f}(\sigma_{s},\tau_{us})}$

Unfolding the newly added type of 2-cells, we recover a familiar condition:

Proposition 47.

Let $E,F:\mathsf{ActCont}_{0}$ and denote $E\mathrel{\doteq}(S,\lambda s\mathpunct{.}(P_{s},G_{s},\sigma_{s}))$ and $F\mathrel{\doteq}(T,\lambda t\mathpunct{.}(Q_{t},H_{t},\tau_{t}))$ . Let $u:S\to T$ and $f,g:\mathsf{ActCont}_{1}(u;E,F)$ . The type of 2-cells $\mathsf{ActCont}_{2}((u,f),(u,g))$ is equivalent to

\prod_{s:S}\sum_{r:H_{us}}\operatorname{\mathsf{isConjugator}}_{\varphi_{s},% \psi_{s}}(r)\times f^{\prime}_{s}=g^{\prime}_{s}\circ\tau_{us}(r),

in which $\varphi,\psi:\prod_{s}G_{s}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil% \cr\scalebox{1.2}{\kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}H_{us}$ and $f^{\prime},g^{\prime}:\prod_{s}Q_{us}\to P_{s}$ are the maps of symmetries and positions of $f$ and $g$ , respectively.

Note the occurrence of the proposition $f^{\prime}_{s}=g^{\prime}_{s}\circ\tau_{us}(r)$ : it has already appeared in the definition of quotient container morphisms as a quotient of premorphisms (Definition 6). In [3, Definition 4.1] it is explained as a necessary condition for labellings of container maps to be defined upto quotient. In our case it is necessary to characterize homotopies between induced bundle maps $\mathbf{\bar{B}}{}_{1}(f^{\prime}_{s})$ and $\mathbf{\bar{B}}{}_{1}(g^{\prime}_{s})$ (Lemma 41).

Lifting the 2-functor $\mathbf{\bar{B}}{}:\operatorname{\mathsf{Action}}\to\operatorname{\mathsf{% SetBundle}}$ to families, we immediately obtain the following characterization of 1-cells of action containers. Substituting $\mathsf{ActCont}\mathrel{\doteq}\operatorname{Fam}(\operatorname{\mathsf{% SetBundle}})$ and $\mathsf{SymmCont}\mathrel{\doteq}\operatorname{\mathsf{SetBundle}}$ , we see:

Corollary 48.

The lifting $\operatorname{Fam}(\mathbf{\bar{B}}{}):\mathsf{ActCont}\to\operatorname{Fam}(% \mathsf{SymmCont})$ is:

1.

locally fully faithful
2.

assuming the axiom of choice, locally a weak equivalence

Proof.

By application of Proposition 45: The 2-category $\operatorname{\mathsf{Action}}$ is locally strict, and $\mathbf{\bar{B}}{}$ locally a weak equivalence (Theorem 42). $\hfill\blacktriangleleft$ This says that constructively, morphisms of action containers correspond to a subcategory of morphisms of (families of) symmetric containers. By using the axiom of choice, one sees that this construction indeed covers all such morphism.

To connect action containers to symmetric ones, and not just families of the latter, note the following: Any family of set bundles (hence symmetric containers) can be combined into a single bundle: given $(J,(\lambda j\mathpunct{.}(B_{j},F_{j})):\operatorname{Fam}(\operatorname{% \mathsf{SetBundle}})$ , we can consider the bundle of fibers over the sum of bases, $\sum_{j:J}B_{j}$ . This construction defines a 2-functor:

Definition 49 (summation of set bundles).

Summation of set bundles is a 2-functor $\Sigma:\operatorname{Fam}(\operatorname{\mathsf{SetBundle}})\to\operatorname{% \mathsf{SetBundle}}$ , with the following data

1.

$\Sigma_{0}(J,\lambda j\mathpunct{.}(B_{j},F_{j}))$ consists of the base $\sum_{j:J}B_{j}$ , and fibers $\lambda(j,b)\mathpunct{.}F_{j}(b)$ .
2.

$\Sigma_{1}(u,\lambda j\mathpunct{.}(\varphi_{j},f_{j}))$ is a pair of a reindexing function $(u,\varphi):\sum_{J}B\to\sum_{K}C$ and a map of fibers, $f:\prod_{(j,b)}G_{uj}(\varphi_{j}(b))\to F_{j}(b)$ .
3.

On 2-cells, it takes a family of identities of bundle maps to an identity of their sums via function extensionality: $\Sigma_{2}(\operatorname{\mathsf{refl}}_{u},\lambda j\mathpunct{.}(r_{j},\bar{% r}_{j}))\mathrel{:=}\operatorname{\mathsf{funext}}\lambda(j,b)\mathpunct{.}% \operatorname{\mathsf{cong}}_{uj,{\shortminus}b}(r_{j}),\bar{r}_{j}(b)$ . $\lrcorner$

The construction turning action containers into symmetric ones now factors as follows:

\mathsf{ActCont}\xrightarrow{=}\operatorname{Fam}(\operatorname{\mathsf{Action% }})\xrightarrow{\operatorname{Fam}(\mathbf{\bar{B}}{})}\operatorname{Fam}(% \operatorname{\mathsf{SetBundle}})\xrightarrow{\Sigma}\operatorname{\mathsf{% SetBundle}}\xrightarrow{=}\mathsf{SymmCont}

In general, we do not know whether $\Sigma$ is locally fully faithful or not. We can however consider its restriction to objects in the image of $\operatorname{Fam}(\mathbf{\bar{B}}{})$ , and deduce fully-faithfulness for some of its local functors:

Lemma 50.

Let $X,Y:\operatorname{Fam}_{0}(\operatorname{\mathsf{SetBundle}})$ . If all bundles in $X$ have connected bases, then the local functor $\Sigma_{1}:\operatorname{Fam}_{1}(X,Y)\to\operatorname{\mathsf{SetBundle}}(% \Sigma_{0}(X),\Sigma_{0}(Y))$ is fully faithful.

Proof.

The proof proceeds by showing that there is an equivalence of 2-cells. The assumption on connectedness is used as follows: Recall that $X\mathrel{\doteq}(J,\lambda j\mathpunct{.}(B_{j},F_{j}))$ has connected bases if all $B_{j}$ are connected groupoids. The base of the bundle $\Sigma_{0}(X)$ is $\sum_{j}B_{j}$ , and maps between such bases are typed $\sum_{j}B_{j}\to\sum_{k}B^{\prime}_{k}$ . To characterize identifications of these maps, it is necessary show, given morphisms $u,v:J\to K$ , that the function $u(j)=v(j)\to(B_{j}\to u(j)=v(j))$ constant in $B_{j}$ is an equivalence. But this follows from connectedness of $B_{j}$ and the fact that $u(j)=v(j)$ is a proposition [20, 7.5.9]. $\hfill\blacktriangleleft$

Theorem 51.

The composite $\Sigma\circ\operatorname{Fam}(\mathbf{\bar{B}}{}):\mathsf{ActCont}\to\mathsf{SymmCont}$ is locally fully faithful.

5 Conclusions

We introduced action containers for studying data types with symmetries. This class of containers is inspired by quotient containers, but are different from the latter in two key aspects: First, symmetries are encoded by arbitrary groups acting on positions, allowing for more freedom in presenting permutations of positions. Second, morphisms are required to respect symmetries in a coherent way, and are additionally not equivalence classes of an ad-hoc relation. Instead, the category of action containers is presented universally as a free coproduct completion of a category of groups and actions, from which limits and colimits of action containers are easy to read off. We reintroduce the relation between morphisms in terms of a 2-categorical structure, and show that the 2-category of action containers embeds into that of symmetric containers.

A missing piece in our analysis is the relationship between quotient and action containers. The latter subsume the former, but morphisms of action containers are more constrained than those of quotient containers. Finding a functorial connection is not straightforward: Each action container $(S\mathbin{\triangleright}P\mathbin{\triangleleft^{\sigma}}G)$ can be mapped to a quotient container with the same set of shapes and positions, but for each $s : S$ changing the group to $\operatorname{\mathsf{Im}}(\sigma_{s})$ , which is a subgroup of $\operatorname{\mathfrak{S}}(P_{s})$ . Unfortunately this operation does not act on morphism $(u\mathbin{\triangleright}f\mathbin{\triangleleft}\varphi):(S\mathbin{% \triangleright}P\mathbin{\triangleleft^{\sigma}}G)\to(T\mathbin{\triangleright% }Q\mathbin{\triangleleft^{\tau}}H)$ , since group homomorphisms $\varphi_{s}:G_{s}\mathrel{\vbox{\offinterlineskip\halign{\hfil#\hfil\cr% \scalebox{1.2}{\kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}}}H_{us}$ do not generally restrict to the image of the actions $\operatorname{\mathsf{Im}}(\sigma_{s})\mathrel{\vbox{\offinterlineskip\halign{% \hfil#\hfil\cr\scalebox{1.2}{\kern-1.07639pt{.}}\cr\kern 0.43057pt\cr$\to$\cr}% }}\operatorname{\mathsf{Im}}(\tau_{us})$ . When restricted to a 1-subcategory of action containers with faithful actions, this construction at least yields an isomorphism-on-objects functor $\mathsf{ActCont}_{\mathsf{faith}}\to\mathsf{QuotCont}$ . In the opposite direction, one could search for a functor between the category $\mathsf{QuotCont}$ and the homotopy category of $\mathsf{ActCont}$ , i.e. the category with the same objects but with sets of morphisms obtained by set quotienting 1-cells by 2-cells. We have a candidate if we modify Definition 5 of premorphism by turning the existential quantifier in the preservation of symmetries into a dependent sum: send a quotient container $(S\mathbin{\triangleright}P\mathord{/}G)$ to the action container with the same set of shapes and positions, but for each $s : S$ changing the group to the free group generated by $G_{s}$ , which also acts on $P_{s}$ , though not in a faithful way. This modification shows at least the existence of an action of morphisms. We postpone a deeper investigation in this direction to future work.

In Section 3.1 we analyzed some properties of the category of action containers. Ordinary containers enjoy further properties that make them suitable as a model of data types: Altenkirch et al. [8] show that the category of ordinary containers is cartesian closed, and Abbott et al. [3] construct initial algebras and final coalgebras of containers in one parameter. In the future, we plan to investigate whether action containers also enjoy these properties as well. From previous investigations [14], we know that direct construction of final coalgebras for quotient containers fails constructively. In [5] however, Ahrens et al. show that for any $\mathcal{U}$ -valued container (with no restriction on truncation level of shapes or positions), its extension as a polynomial in $\mathcal{U}$ admits a final coalgebra. Since extensions of symmetric containers are $\mathcal{U}$ -polynomials as well, we would like to internalize this construction: first, find a symmetric container representing this coalgebra, then investigate if this restricts to the inclusion of action containers. This in particular requires studying the composition-monoidal structure of action containers. Similarly, it should be possible to lift the closure properties of Section 3.1 from the underlying 1-category to proper 2-(co)limits in $\operatorname{\mathsf{Action}}$ .

In another direction we are interested to see if the heavy machinery of 2-categories can be avoided, or at least be postponed. This is guided by the following insight: The image on objects of the 2-functor $\mathbf{B}{}$ is not only groupoids, but pointed, connected groupoids. The 2-category of such groupoids and pointed maps, displayed over $\operatorname{\mathsf{hGpd}}$ is, surprisingly, locally thin [9, Lemma 4.4.12]. In other words, pointed, connected groupoids and pointed maps form a 1-category $\mathsf{hGroup}$ . A slight modification of the proof of Proposition 36 shows that the 1-category of ordinary groups is equivalent to $\mathsf{hGroup}$ , and that this equivalence extends to categories of actions. The same argument shows that the 2-category of skeletal groupoids²²2Those that come with a choice of basepoint $\operatorname{\mathsf{pt}}:\prod_{x:\lVert B\rVert_{0}}\operatorname{\mathsf{% fiber}}_{\lvert-\rvert_{0}}(x)$ for each connected component. and skeleton-preserving maps is locally thin. We believe that this extends to an equivalence between the 1-categories of action containers (without additional relation between morphisms) and skeletal symmetric containers, i.e. those whose shapes are skeletal groupoids, and whose morphisms preserve such skeleta. This would identify a structure on symmetric containers such that equality of morphisms becomes propositional, giving rise to a convenient 1-category of containers with symmetries.

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. doi: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. doi: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. doi: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. doi: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. doi: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. doi:10.1017/s0960129522000032.
[7] Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. Logical Methods in Computer Science, 15(1), March 2019. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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. doi: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.
[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.

[bib.bib1] [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. doi:10.1007/3-540-36576-1_2.

[bib.bib2] [2] Michael Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3–27, 2005. doi:10.1016/j.tcs.2005.06.002.

[bib.bib3] [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. doi:10.1007/978-3-540-27764-4_2.

[bib.bib4] [4] Jiří Adámek and Jiří Rosický. How nice are free completions of categories? Topology and its Applications, 273:106972, 2020. doi:10.1016/j.topol.2019.106972.

[bib.bib5] [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. doi:10.4230/LIPICS.TLCA.2015.17.

[bib.bib6] [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. doi:10.1017/s0960129522000032.

[bib.bib7] [7] Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed Categories. Logical Methods in Computer Science, 15(1), March 2019. doi:10.23638/lmcs-15(1:20)2019.

[bib.bib8] [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. doi:10.1007/978-3-642-13962-8_2.

[bib.bib9] [9] Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry. https://github.com/UniMath/SymmetryBook. Commit: 8546527.

[bib.bib10] [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.

[bib.bib11] [11] Ryu Hasegawa. Two applications of analytic functors. Theoretical Computer Science, 272(1–2):113–175, February 2002. doi:10.1016/s0304-3975(00)00349-2.

[bib.bib12] [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.

[bib.bib13] [13] Niles Johnson and Donald Yau. 2-Dimensional Categories. Oxford University Press, January 2021. doi:10.1093/oso/9780198871378.001.0001.

[bib.bib14] [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. doi:10.4230/LIPICS.ITP.2023.20.

[bib.bib15] [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. doi:10.1007/bfb0072514.

[bib.bib16] [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. doi:10.1145/2603088.2603153.

[bib.bib17] [17] Max New, Steven Shaefer, and contributors. cubical-categorical-logic, 2024. URL: https://github.com/maxsnew/cubical-categorical-logic.

[bib.bib18] [18] Andrew M. Pitts. Nominal sets. Number 57 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013.

[bib.bib19] [19] The agda/cubical development team. The agda/cubical library, 2018. URL: https://github.com/agda/cubical/.

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

	$\displaystyle\operatorname{\mathsf{suc}}$	$\displaystyle:\operatorname{\mathsf{Fin}}(n)\simeq\operatorname{\mathsf{Fin}}(n)$
	$\displaystyle\operatorname{\mathsf{suc}}(k)$	$\displaystyle\mathrel{:=}(k+1)\mod n$

Data Types with Symmetries via Action Containers

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Supplementary Material:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

1.1 Notation and Background

1.2 2-Categories

2 Quotient and Symmetric Containers

2.1 Quotient Containers

Definition 1.

Example 2.

Definition 3 (extension of quotient containers).

Example 4 (unordered n-tuples).

Definition 5.

Definition 6.

Definition 7.

2.2 Symmetric Containers

Definition 8.

Definition 9.

Definition 10.

Definition 11.

Example 12.

2.3 Lifting Quotient Containers

Proposition 13.

Definition 14.

Definition 15 (associated bundle).

Proposition 16.

Proof.

Definition 17.

Proposition 18.

Proof.

Theorem 19.

Proof.

Lemma 20.

Proof.

Example 21.

3 Action Containers

Definition 22.

Example 23 (cyclic lists as an action container).

Definition 24.

Definition 25.

3.1 Algebra of Action Containers

Definition 26.

Theorem 27.

▶ Remark (univalence of 𝖠𝖼𝗍𝖢𝗈𝗇𝗍).

Proposition 28.

Corollary 29.

Proof.

Proposition 30 (constant containers are exponentiable).

▶ Remark (composition of action containers).

4 The 2-Category of Action Containers

Proposition 31.

Proof.

4.1 A 2-Category of Groups

Definition 32.

Lemma 33.

Proof.

Theorem 34.

Proposition 35.

Proof.

Proposition 36.

Proof.

4.2 A 2-Category of Group Actions

Definition 37 (2-category of actions).

Definition 38 (set bundles).

Definition 39.

Definition 40.

Lemma 41.

Theorem 42.

Proof.

4.3 A 2-Categorical Fam-Construction

Definition 43 (2-category of families).

Example 4 (unordered $n$ -tuples).

$\blacktriangleright$ Remark (univalence of $\mathsf{ActCont}$ ).

$\blacktriangleright$ Remark (composition of action containers).

4.3 A 2-Categorical $\operatorname{Fam}$ -Construction