System I is a recently introduced simply-typed lambda calculus with pairs where isomorphic types are considered equal. In this work we propose a variant of System I with the type Top, and present a complete formalization of this calculus in Agda, which includes the proofs of progress and strong normalization.

翻译：System I 是近期提出的一种带配对结构的简单类型 lambda 演算，其中同构类型被视为相等。本文提出了一种带有 Top 类型的 System I 变体，并在 Agda 中给出了该演算的完整形式化实现，包括进度定理和强正规化定理的证明。