We refer to reviewers #13A and #13C respectively by rA and rC.
The review #13B has two authors.
We refer to the "main" author as rB and the subreviewer as rSB.

We have made the following improvements in response to the ICFP 2017 reviews:

1. In response to rA and rB, we have now done the proof of the abstraction theorem
   for the IsoRel translation. The detailed proof is in Appendix B. The intuition is
   briefly explained in Section 5.1.1 (Correctness).

2. In response to rA, for the examples in Section 6 (Applications), we now include the statements of the IsoRel abstraction theorems produced by our translations.
   These can be found in Appendix A.7 (Abstraction theorems for obseq)

3. In response to rB, rSB, rC, we produce an example where the two assumptions
   (total and one to one) are necessary. This is now in Section 3.3 (Necessity of our Assumptions)

4. We thank rSB again for the detailed section-by-section feedback on improving the presentation and the structure of the paper. We have addressed most of those suggestions. Hopefully, this also addresses the concerns rB and rA had about the presentation and the structure of the paper.
   For example, we liberally use the Theorem/Lemma environments to state the main claims and their proofs. Also, we now liberally give names to concepts that we refer to again and again (e.g. strong IsoRel translation and weak IsoRel translation). In proofs, we try to use the traditional mathematical language, instead of the Coq-like
   language that we think in (Most proofs in this paper were originally done in Coq).
   We choose more intuitive names in our examples.

5. In response to rB, we have expanded our related work section to mention and compare with the papers that study semantic models. Also, we have made our comparison with
   HoTT (Homotopy Type Theory) more precise.

6. Use of Axioms/JMeq (rC, rB):
   In Section 1, in summary of contributions, we now explicitly say that our
   AnyRel translation does NOT use any axiom (and that our IsoRel translation uses 2 axioms).
   Thus, it would be a disadvantage to use JMeq-related axioms in the AnyRel translation.
   Furthermore, we now explain the difference w.r.t. JMeq in Section 2.3.