This PR removes two unnecessary assumptions from discreteSetQuotients in Cubical.HITs.SetQuotients.Properties. It now simply shows that the quotient A / R is discrete if R is an equivalence relation (not necessarily prop-valued) and R a₀ a₁ is decidable.
This PR removes two unnecessary assumptions from
discreteSetQuotientsinCubical.HITs.SetQuotients.Properties. It now simply shows that the quotientA / Ris discrete ifRis an equivalence relation (not necessarily prop-valued) andR a₀ a₁is decidable.