We write that In the submission, we relegated much of the HoTT background and notation to the technical appendix. If the paper is accepted it would be worth purchasing a couple of additional pages to streamline the presentation.
In particular:
[x] We will move the explanation of n-types from the appendix to the main text.
[x] It is true that, (f = g) ≃ (f ~ g) by funext/happly (in appendix) - move definition of homotopy and funext/happly to the main text.
[x] Yes, q is the point constructor for the set quotient which we define in the appendix - move to text.
[x] (nonessential) Move the image im(f) to the main text.
We write that
In the submission, we relegated much of the HoTT background and notation to the technical appendix. If the paper is accepted it would be worth purchasing a couple of additional pages to streamline the presentation.In particular:
We will move the explanation of n-types from the appendix to the main text.It is true that, (f = g) ≃ (f ~ g) by funext/happly (in appendix) - move definition of homotopy and funext/happly to the main text.Yes, q is the point constructor for the set quotient which we define in the appendix - move to text.im(f)to the main text.