Formalising Inductive and Coinductive Containers

TL;DR

This paper formalizes the theory of containers for inductive and coinductive types within intensional type theory using Cubical Agda, avoiding UIP assumptions and leveraging path types for coinductive proofs.

Contribution

It provides a formalization of container fixed points in Cubical Agda, extending previous results to intensional type theory without UIP, and demonstrates the utility of path types for coinductive reasoning.

Findings

Formalization of container fixed points in Cubical Agda

Generalization from Set to the category of types

Use of path types to establish coinductive equality

Abstract

Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of locally cartesian closed categories (LCCCs) with disjoint coproducts and W-types, and uniqueness of identity proofs (UIP) is implicitly assumed throughout. Although it is claimed that these developments can also be interpreted in extensional Martin-L\"of type theory, this interpretation is not made explicit. In this paper, we present a formalisation of the results that 'containers preserve least and greatest fixed points' in Cubical Agda, thereby giving a formulation in intensional type theory. Our proofs do not make use of UIP and thereby generalise the original results from talking about container functors on Set to container functors on the wild category of types. Our main incentive for using Cubical Agda is that its path type restores the equivalence between bisimulation and coinductive equality. Thus, besides developing container theory in a more general setting, we also demonstrate the usefulness of Cubical Agda's path type to coinductive proofs.