Whenever editing is allowed on the nLab again, this article should be ported over there.
Definition
In set theory
Let be a set and let be an equivalence relation on . Let us define a quotient set algebra of and to be a set with a function such that
A quotient set algebra homomorphism of and is a function between two quotient set algebras and such that
The category of quotient set algebras of and is the category whose objects are quotient set algebras of and and whose morphisms are quotient set algebra homomorphisms of and . The quotient set of and , denoted , is defined as the initial object in the category of quotient set algebras of and .
In homotopy type theory
Let be a type, and let be an equivalence relation on .
The quotient set is inductively generated by the following: