While reasoning modulo equivalences is standard for mathematicians, replacing structures in formal proofs by equivalent ones often bears considerable porting effort. Similarly, computer scientists like to write programs and proofs in terms of representation types but prefer to provide libraries in terms of different, though related, abstract types; again, replacing these representation types by their abstract counterparts is often not for free. Existing solutions facilitating the transport of terms along such equivalences are either based on univalence -- and hence not applicable to most proof assistants -- or restricted to partial quotient types. We present a framework that (1) does not require univalence, (2) is richer than previous approaches working on partial quotient types, and (3) is based on standard mathematical notions, particularly Galois connections and order equivalences. For this, we introduce the idea of partial Galois connections and Galois equivalences. We prove their closure properties under (dependent) function relators, (co)datatypes, and compositions. We formalised the framework in Isabelle/HOL and provide a simple prototype.

翻译：在模等价关系下进行推理是数学家的常规做法，但将形式化证明中的结构替换为等价结构往往需要大量的移植工作。同样，计算机科学家倾向于使用表示类型编写程序与证明，却更希望以不同但相关的抽象类型形式提供库函数；而将这类表示类型替换为对应的抽象类型通常并非无成本。现有的便于沿此类等价关系迁移术语的解决方案，要么基于单值性——故不适用于多数证明助手，要么局限于部分商类型。我们提出一个框架，该框架(1)不依赖单值性，(2)比先前基于部分商类型的方法更丰富，(3)基于标准数学概念，特别是伽罗瓦连接与序等价。为此，我们引入偏伽罗瓦连接与伽罗瓦等价的概念。我们证明了它们在（依赖）函数关系子、(共)数据类型及复合下的封闭性质。该框架已在Isabelle/HOL中形式化，并提供了简易原型。