Identity crisis

[marcbezem]

I rephrased in the style guide the points below in accordance to our discussions, and assign to myself carrying the first point out. That means inspecting 187 lines in which "identity" occurs, and keep "identity type/function/map", add "map" in cases where the map is meant, and change the remaining occurrences of "identity" to "identification" or "path".

• Identity types are denoted in general using the macro \eqto, which produces an arrow with an = on top. An element of an identity type is called an identification, and otherwise a path. We may say that it shows how to identify two elements. If the type is a set, we may denote its identity types by a = b and call them equations. When a = b has an element we say that a and b are equal.
• Types similar to identity types, like the type of eqivalences from A to B, are also denoted with a macro ending in "to", like \equivto, producing an arrow with an equivalence sign on top.

[marcbezem]

2.5 starts by a sentence stating: [...] identity type, which implements the intuitive notion of equality. Is the intuitive really what we mean, or is it even true? I would prefer a notion of equality.

I changed the next sentence to: Identity types are formed of a type and two elements of that type; we shall have no need to compare elements of different types.

Later on we have Equality is symmetric [....]. I would prefer something like: _Equality relations are symmetric [....]. Here we have .... And similarly for transitivity.

We desperately need a paragraph on proof relevance, otherwise we also get an equality crisis!

[DanGrayson]

Maybe add a warning to the effect that the notion of equality implemented here keeps track of the way two things are identified, and there can be multiple ways. For example, two triangles can be congruent in multiple ways.

[marcbezem]

Most cases of "identity" in Ch. 2 have been resolved in commit fbbda70.

There are still some issues with "equal".

1. The following use cases should be fine: "equal in a set", "equal by definition", and "definitionally equal". Should we enforce "by definition" and "definitionally" if that is meant?
2. If none of the three above applied, I replaced "equal to" a couple of times by "can be identified with" (l. 3633, 3667).
3. There are still some = lingering around that mean the truncation of the identity type (Exc. 2.16.9). Will try to find all of them.

I attach an annotated copy of Ch. 2 for discussion tomorrow. AnnotCh2.pdf