The very dependent recursive structure of iterated parametricity in indexed form

TL;DR

In indexed form iterated parametricity is described as dependent sequences $E_0, E_1, \dots$ whose later stages depend on earlier data, yielding interpretations as augmented semi-simplicial or semi-cubical structures for $\nu$-ary iterations. It replaces equational induction from the Rocq formalisation with a definitional, mutually dependent induction that interleaves the specification of the induction hypothesis with the construction step. The authors provide a machine-checked, detailed account of the core components—$\framep$, $\layer$, $\painting$, and the coherence maps $\restrf$, $\restrp$, $\cohf$, $\cohp$—and show how a zipper data structure manages the intricate dependencies. This approach yields a precise interpretation of higher-arity parametricity as dependent indexed structures (ν-sets) and points toward unbounded iterations via streams, linking back to Rocq and to semi-simplicial/semi-cubical models.

Abstract

Reynolds' parametricity originally equips types with proof-irrelevant binary propositional relations over the types. But such relations can also be taken proof-relevant or unary, and described either in an indexed or fibred way. Parametricity can be iterated, and when types are sets, this results in an interpretation of sets as augmented simplicial sets in the unary case, or cubical sets in the binary case. In earlier work, equations were given describing the n-ary iterated parametricity translation of sets in indexed form. The construction was formalised in Rocq by induction on a large structure embedding equational reasoning. The current work analyses the dependency structure of the earlier work leading to a presentation of the construction replacing equational reasoning with definitional reasoning. The new construction is very dependent, based on an induction that requires interleaving the specification of the induction hypothesis and the construction of the induction step. At the same time, the construction reduces to its computational essence and can be described in full detail, closely following the new machine-checked formalisation.