Homotopy Type Theory
quotient set > history (Rev #1)
Contents
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 . Then the quotient set is a set with a function such that
In homotopy type theory
Let be a type, and let be an equivalence relation on .
The quotient set is inductively generated by the following:
-
a function
-
a family of dependent terms
-
a family of dependent terms
See also
References
Revision on April 13, 2022 at 23:21:43 by
Anonymous?.
See the history of this page for a list of all contributions to it.