Add exercise: all identity type families are equal

[jeanas]

Rendered:

[jeanas]

The first commit fixes a typo in my previous PR #1171, sorry for that.

The anecdote behind this is that I was trying convince a mathematician that HoTT's equality type is not “a misnamed equality that should be called something else and live together with an actual equality that behaves like you expect”. (Though he now believes HoTT is just incapable of correctly handling equality 🙂)

[mikeshulman]

I think the exercise is fine, but there's a bit of redundancy with section 5.8. So from an abstract perspective, the exercise might make more sense in chapter 5. Although I get your point that from a pedagogical perspective there's some value to mentioning it in chapter 2 though. Maybe the exercise in chapter 2 can just refer forwards to section 5.8, and likewise 5.8 can refer back to the exercise?

Anyone else have thoughts?