Showing changes from revision #3 to #4:
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 onequivalence relation . Let on us define aquotient set algebra of and . to Let be us define a setquotient set algebra of and with to be a function 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