Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant

Théo Zimmermann, Hugo Herbelin

In mathematics, it is common practice to have several constructions for the same objects. Mathematicians will identify them modulo isomorphism and will not worry later on which con…