Derivatives for Containers in Univalent Foundations
Philipp Joram
Tallinn University of Technology
Abstract:
Containers are a convenient type-theoretic representation of a wide
class of inductive data types. Derivatives of containers compute
representations of types of "one-hole contexts", useful for implementing
tree-traversal algorithms. We know that we can take the derivative of a
container whenever its positions have decidable equality.
In a univalent setting, types represent ∞-groupoids, and containers let
us model inductive types with interesting symmetries, such as finite
multisets. However, Hedberg's Theorem prevents us from taking
derivatives of containers whose positions are higher types: types with
decidable equality have trivial higher structure.
In this talk, I will show how to circumvent this apparent restriction,
and extend derivatives to arbitrary, untruncated containers. These
derivatives satisfy the expected basic laws with respect to constants,
sums, and products. I derive the chain rule and show that it is in
general non-invertible. For traditional (set-valued) containers, the
existence of an invertible chain rule is equivalent to a classical
principle. If time permits, I will sketch the derivation of a rule for
derivatives of smallest fixed points from the chain rule and
characterize its invertibility.
More details can be found in the following preprint:
https://arxiv.org/abs/2512.17484
All results are formalized in Cubical Agda, and can be browsed
interactively online:
https://phijor.me/derivatives/