Higher Type Arithmetic (HA$^w$) is a first-order many-sorted theory. It is a conservative extension of Heyting Arithmetic obtained by extending the syntax of terms to all of System T: the objects of interest here are the functionals of higher types. While equality between natural numbers is specified by the axioms of Peano, how can equality between functionals be defined? From this question, different versions of HA$^w$ arise, such as an extensional version (E-HA$^w$) and an intentional version (I-HA$^w$). In this work, we will see how the study of partial equivalence relations leads us to design a translation by parametricity from E-HA$^w$ to HA$^w$.

翻译：高阶类型算术（HA$^w$）是一种一阶多类理论，它是通过将项语法扩展至全部系统T而获得的Heyting算术的保守扩展，其中研究的核心对象是高阶类型泛函。自然数之间的等式由Peano公理指定，但泛函之间的等式应如何定义？由此问题衍生出HA$^w$的不同版本，如外延版本（E-HA$^w$）和内涵版本（I-HA$^w$）。本文将通过研究部分等价关系，揭示如何借助参数化方法设计从E-HA$^w$到HA$^w$的翻译。