Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees. Similarly, subtypes and quotients are commonly used to construct new type abstractions in formal verification. In such cases, one often wishes to reuse operations on the representation type for the new type abstraction, but to no avail: the types are not the same. To address these problems, we present a new framework that transports programs via equivalences. Existing transport frameworks are either designed for dependently typed, constructive proof assistants, use univalence, or are restricted to partial quotient types. Our framework (1) is designed for simple type theory, (2) generalises previous approaches working on partial quotient types, and (3) is based on standard mathematical concepts, particularly Galois connections and equivalences. We introduce the notion of partial Galois connections and equivalences and prove their closure properties under (dependent) function relators, (co)datatypes, and compositions. We formalised the framework in Isabelle/HOL and provide a prototype.

翻译：多种类型可以表示同一概念。例如，列表和树都可以表示集合。但这一情况容易导致库的不完备性：某些集合操作可能仅对列表可用，而另一些仅对树可用。类似地，在形式化验证中，子类型和商类型常被用于构造新的类型抽象。此时，人们往往希望将表示类型上的运算复用于新的类型抽象，却因类型不同而难以实现。为解决这些问题，我们提出了一种通过等价关系传递程序的新框架。现有的传递框架要么专为依赖类型、构造性证明助手设计，要么利用单值性公理，或局限于部分商类型。我们的框架(1)专为简单类型理论设计，(2)推广了先前基于部分商类型的方法，(3)基于标准数学概念，特别是伽罗瓦连接与等价关系。我们引入了部分伽罗瓦连接与等价关系的概念，并证明了它们在（依赖）函数关联子、（共）数据类型及复合操作下的封闭性质。我们在Isabelle/HOL中形式化了该框架，并提供了原型实现。