A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl).

Yannick Forster, Felix Jahn, Gert Smolka

Browse the full CPP paper archive.