introduce quotient sets by means of a higher inductive type

[DanGrayson]

... because the current construction in 2.22 is a bit too slick, and the student will be better able to see what is going on in the higher inductive type.

[UlrikBuchholtz]

Revised proposal: Introduce the HIT version in an exercise in Ch. 2, along with a forward reference to Ex. 6.3.7 (with the variation: set-truncation of graph quotient).

[DanGrayson]

Now the original definition looks pretty good to me.

[DanGrayson]

Well, let's put some motivation for the definition into the text.

[marcbezem]

I liked Dan's example of net worth and I had a go at an introduction. @DanGrayson: feel free to modify it! (NB the raw text uses book-macros like \succ that are interpreted by git in a different way. Pls switch to raw text.)

Net worth can be defined as wealth minus debt. Let's assume wealth $w$ and debt $d$ are natural numbers. The debt can be greater than the wealth, yielding a negative net worth, but at this point in our book we do not have negative numbers at our disposal. However, we do have the binary product, and the pair $(w,d): (\NN\times\NN)$ also completely determines the net worth. However, $(w,d)$ contains more information than necessary: for example, $(\succ(w),\succ(d))$ determines the same net worth as $(w,d)$, and $(\succ(w),\succ(d))\ne(w,d)$. Put differently, the type $\NN\times\NN$ does not capture the notion of net worth, since its identity types don't capture equality of net worth.

Clearly, we need a different type to capture the notion of net worth. Of course, we want a type construction that works not only for the special case of net worth, but also in similar situations. Common for such situations is that we have type $A$ and an equivalence relation\footnote{} $R : A\o A\to \Prop$. In the example of net worth, we would have $A\defeq(\NN\times\NN)$, and the equivalence relation would be $R((w_1,d_1),(w_2,d_2)) \defeq (w_1+d_2 = w_2 + d_1)$, precisely capturing equality of net worth, $w_1 - d_1 = w_2 - d_2$, without using negative numbers!

What we need is a new type, which is like $A$, but with $x\eqto y$ if and only if $R(x,y)$, for all $x,y:A$. Note that the latter requires that the new type is a set. The quotient set $A/R$ that we will define and study in this section fulfills these requirements. In the special case of $A\defeq(\NN\times\NN)$, and $R((w_1,d_1),(w_2,d_2)) \defeq (w_1+d_2 = w_2 + d_1)$, the type $A/R$ could in fact be used as a type of intergers, see \cref{sec:integers} and see \cref{xca:newexercise}.

[marcbezem]

I made the changes as we discussed: equivalence class ---> equivalence predicate. It occurred to me that the motivation for this change also applies to $R: A \to (A\to \Prop)$: in set theory $R$ would be a subset of $A\times A$. All this is now explained in Footnote 69, using colors to distinguish between different occurrences of $a$ n $R(a)(a)$. Please take a look at 0035e25

[UlrikBuchholtz]

Looks good!