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.

翻译：雷诺兹参数化最初为类型配备了证明无关的二元命题关系。然而，这类关系亦可视为证明相关或一元的，并可通过索引化或纤维化的方式进行描述。参数化可进行迭代，当类型为集合时，在单变量情形下将集合解释为增广单纯集，在双变量情形下则解释为立方集。在先前工作中，我们给出了描述集合的n元迭代参数化索引形式转换的方程组。该构造通过在罗克中归纳一个支持等式推理的大型结构得以形式化。本研究分析了先前工作的依赖结构，提出了一种以定义式推理替代等式推理的构造表述。新构造具有高度依赖性，其基于一种需要交错指定归纳假设与构建归纳步骤的归纳法。同时，该构造还原至其计算本质，可依据新的机器验证形式化进行完整详尽的描述。