While reasoning modulo equivalences is standard for mathematicians, replacing structures in formal proofs by equivalent ones often bears considerable porting effort. Similarly, while representation independence tells us that two related implementations of an abstract interface are contextually equivalent, such a replacement is often not for free in proof assistants. Existing solutions facilitating the transport of terms along 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.