Proof and Program Transfer Modulo Equivalence

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Opening obstruction

An efficient representation may be equivalent to one that is easier to reason about, yet raw rewriting, parametricity alone and univalence alone do not provide coherent automated transport of programs and dependent proofs.

Development contract

Use a Trocq-style heterogeneous transfer calculus with the relation $R_n(xs,v):=(xs=\mathsf{toList}(v))$ between lists of length $n$ and vectors. Prove its abstraction theorem, transfer append and its length theorem, calculate the generated transports, and identify exactly which relation enrichments use univalence before auditing the kernel proof terms.