by Nicolai Kraus on December 12, 2012.
Tagged as: Lunches.
Last Friday (07/12/12), I have talked about the difficulties of quotients in Homotopy Type Theory.
Traditionally, the quotient \(A/\sim\) of a set \(A\) by some equivalence relation \(\sim : A \to A \to \textbf{Prop}\) is a set \(Q\) (or, by abuse of notation, just \(A/\sim\) , think of the set of equivalence classes), together with a function \([\_] : A \to Q\) (mapping every element on its equivalence class) and an eliminator. The latter says, more or less, whenever a function \(f : A \to C\) does not distinguish between elements that are \(\sim\)-equivalent, it can be lifted to a function \(\overline f : Q \to C\). For the details, I would recommend Definable Quotients in Type Theory by Nuo, Thomas and Thorsten.
This is a very natural concept and, in some cases, it is necessary. For example, the real numbers cannot be defined without quotients (this statement refers only to Type Theory, but even in classical mathematics, notions as the Cauchy Reals make usage of quotients). However, the concept becomes much more involved as soon as the principle UIP (uniqueness of identity proofs) is dropped. It would make sense to generalise the notion of an equivalence relation, but even if we don't, it is not clear at all what it means for a function to "not distinguish between elements that are equivalent". Without UIP, the actual proofs and their behaviours matter, while we did not have to care about that issue before.
I talked about the example of the possibly simplest equivalence relation, which is constantly \(\textbf{True}\). In that case, the quotient should be the h-propositional reflection (also known as "squash-type" or "bracket-type"), but it is already very hard to formalise the conditions under which a function \(f : A \to C\) can be lifted to \(Q \to C\). Informally, for any finite number of points in \(A\), we can, by induction on the number of points, define the corresponding simplex in \(Q\), and the condition on \(f\) is that these simplices can be built out of coherence proofs. This leads to one of the standard constructions when it comes to \(\omega\)-category theory, and possibly to concepts that are well-known in Homology. Of course, the first goal is the formalisation of the informally described idea.