Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory