Consider porting ssreflect's "Pragmatic quotient types in Coq"
(Paper link: https://link.springer.com/chapter/10.1007%2F978-3-642-39634-2_17 / https://hal.inria.fr/hal-01966714).
That's part of the motivation in !327 (merged); @robbertkrebbers was interested, so here's an initial summary.
The paper lets you build a quotient given only:
- a decidable equivalence relation
- a choice structure — here, a
Countable
instance.
Usually, one must also write a normalizer to produce a canonical form — but that can be hard to define for arbitrary equivalences, and proving the required properties can be harder.
To avoid that, it's enough to use the choice structure: choose
is enough of a normalizer!