In this file we define concrete quotients in the style of Cyril Cohen. The central remark is that for countable types (or, for that matter any type supporting constructive indefinite description and having decidable equality, which is "almost" the same) quotients by decidable equivalence relations can be constructed using only the native equality of Coq. These quotients have the pleasant additional property of being retracts of the original type.

The quotient of A by R maps x to the canonical representative of the equivalence class R x (which is given by definite description). The definition of Quotient R requires that R is reflexive to ensure that R x is non-empty. Of course, the quotient construction is only really useful when R is an equivalence. Indeed, symmetry and transitivity will ensure that R x and R y are equivalent when R x y, which, by extensionality of choose will ensure that the canonical representatives of R x and R y are indeed equal. The use of Canonize in the definition makes it so that extensional equality on Quotient R is Coq's primitive equality.

Universal property of quotients

Extentionality of quotient equality

Quotients are countable