Derivatives for Containers in Univalent Foundations

TL;DR

This paper extends the concept of derivatives for containers within Univalent Foundations, providing universal properties, laws, and a chain rule, all formalized in Cubical Agda, to enhance the representation of one-hole contexts in type theory.

Contribution

It introduces derivatives for untruncated containers in Univalent Foundations, establishing their universal properties and laws, and formalizes these results in Cubical Agda.

Findings

Derivatives satisfy a universal property in the category of untruncated containers.

A chain rule exists but is generally non-invertible, with restrictions in set-truncated cases.

Derived rules for fixed points and characterized invertibility of derivatives.

Abstract

Containers conveniently represent a wide class of inductive data types. Their derivatives compute representations of types of one-hole contexts, useful for implementing tree-traversal algorithms. In the category of containers and cartesian morphisms, derivatives of discrete containers (whose positions have decidable equality) satisfy a universal property. Working in Univalent Foundations, we extend the derivative operation to untruncated containers (whose shapes and positions are arbitrary types). We prove that this derivative, defined in terms of a set of isolated positions, satisfies an appropriate universal property in the wild category of untruncated containers and cartesian morphisms, as well as basic laws with respect to constants, sums and products. A chain rule exists, but is in general non-invertible. In fact, a globally invertible chain rule is inconsistent in the presence of non-set types, and equivalent to a classical principle when restricted to set-truncated containers. We derive a rule for derivatives of smallest fixed points from the chain rule, and characterize its invertibility. All of our results are formalized in Cubical Agda.