Datatypes with Symmetries in Homotopy Type Theory

Abstract

We study datatypes with symmetries in homotopy type theory by representing them as containers.

We show that definitions of such containers based on set-truncated types (h-sets) are insufficient to constructively model non-wellfounded datatypes: Typically, non-wellfounded datatypes are interpreted as final coalgebras of endofunctors of sets. Classically, the type of non-wellfounded trees with finite and unordered branching is the final coalgebra of the finite multiset functor. We prove that this coalgebra is final if and only if the constructively non-derivable lesser limited principle of omniscience holds.

Gylterud’s symmetric containers are based on groupoid-truncated types, and are known to induce final coalgebras in a suitable 2-categorical way. Finite multisets are represented both by a quotient container (in the sense of Abbot et al.) as well as a symmetric container. We make this translation from quotient- to symmetric containers precise. To this end we introduce action containers, a variation of the quotient containers satisfying additional coherence conditions. We construct a locally fully-faithful functor from the 2-category of action containers into that of symmetric containers. This 2-functor restricts to an equivalence between a 1-category of action containers and symmetric containers whose groupoids of shapes carry additional structure. From this 1-categorical semantics we derive a partial substitution operation for action containers, previously left undefined for quotient containers.

Lastly, we define a derivative operation for containers whose shapes and positions are arbitrary, untruncated types. It satisfies a universal property with respect to all containers and cartesian morphisms. We derive a chain rule and prove that is an embedding of containers. For groupoid-truncated containers, the chain rule may fail to be an equivalence. For set-truncated containers, it is an equivalence if and only if arbitrary h-sets have decidable equality. To prove these results, we establish properties of the isolated points of arbitrary types, and how isolatedness distributes over various type formers. In particular, we characterize the isolated points of dependent sums in terms of non-constructive axioms.