Map a function f : α → β such that ra x y implies rb (f x) (f y) to a map quot ra → quot rb.

If ra is a subrelation of ra', then we have a natural map quot ra → quot ra'.

Map a function f : α → β that sends equivalent elements to equivalent elements to a function quotient sa → quotient sb. Useful to define unary operations on quotients.

Map a function f : α → β → γ that sends equivalent elements to equivalent elements to a function f : quotient sa → quotient sb → quotient sc. Useful to define binary operations on quotients.

A version of quotient.map₂ using curly braces and unification.

Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.

Unwrap the VM representation of a quotient to obtain an element of the equivalence class. Computable but unsound.

Choose an element of the equivalence class using the axiom of choice. Sound but noncomputable.

trunc α is the quotient of α by the always-true relation. This is related to the propositional truncation in HoTT, and is similar in effect to nonempty α, but unlike nonempty α, trunc α is data, so the VM representation is the same as α, and so this can be used to maintain computability.

Constructor for trunc α

Any constant function lifts to a function out of the truncation

Noncomputably extract a representative of trunc α (using the axiom of choice).