Equality diagram

Here's an attempt at a diagram illustrating some of the conceptual structure of equality types.  Latex source is at https://github.com/mobileink/graphics/blob/master/pgf/h-equality.tex.

``In the homotopy interpretation, ... the type of triples (x, y, p), where x and y are the endpoints of the path p (in other words, the Σ-type ∑(x,y:A)(x = y)), is inductively generated by the constant loops at each point x. As we will see in Chapter 2, in homotopy theory the space corresponding to ∑(x,y:A)(x = y) is the free path space — the space of paths in A whose endpoints may vary — and it is in fact the case that any point of this space is homotopic to the constant loop at some point, since we can simply retract one of its endpoints along the given path.'' (HoTT p. 51)

``[T]he space of paths starting at some chosen point (the based path space at that point, which type-theoretically is ∑(y:A)(a = y)) is contractible to the constant loop on the chosen point.'' (HoTT p. 51)

``In set theory, the proposition a = a is entirely uninteresting, but in homotopy theory, paths from a point to itself are called loops and carry lots of interesting higher structure. Thus, given a type A with a point a : A, we define its loop space Ω(A, a) to be the type a =A a.'' (HoTT p. 68)

This diagram is intended to convey the idea that point a freely generates its path space, hence b_1 and b_2, that there are multiple "ways of being identical", multiplicity of loops at a, etc.  Suggestions for improvement welcome.