The very dependent recursive structure of iterated parametricity in indexed form

TL;DR

This paper analyzes the complex dependency structure of iterated parametricity in indexed types, replacing equational reasoning with definitional reasoning, and provides a detailed, machine-checked formalisation of the construction.

Contribution

It introduces a highly dependent inductive construction for iterated parametricity, simplifying previous equational approaches and enabling detailed formal verification.

Findings

The new construction is highly dependent and inductive.

It replaces equational reasoning with definitional reasoning.

The formalisation is machine-checked and closely follows the construction.

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.