Documentation nit: use `[epi_surj]` and `[hProp]` and `[hSet]` so that coqdoc will make links for you.