Showing changes from revision #4 to #5:
Added | Removed | Changed
Whenever editing is allowed on the nLab again, this article should be ported over there.
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 .
Let be a setoid. The quotient set is inductively generated by the following:
a function
a family of dependent terms
a family of dependent terms
Last revised on June 15, 2022 at 20:37:40. See the history of this page for a list of all contributions to it.