Transport via Partial Galois Connections and Equivalences

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.