HoTT/HoTT — pull request #481 by andrejbauer (2014-09-09 16:57:15+00:00)
Title: Various improvements to `Overture`.

Caveat: This branch is not working yet, I am hoping someone can fix the problem with notations, which appears in `categories.Comma.Dual`, line 28. I am making a pull request because it best demonstrates how my understanding of what we should do about `symmetry` and `transitivity`.

1. Updated comments which were out of sync with reality in various places.

2. Removed non-ascii characters (Type subscripted with 0 or 1). No utf8 characters in the core, please.

3. Reverted back to calling concatenation of paths `concat`. Then declared `concat` to be an instance of transitivity. Then tried to define notations so that in `path_scope` both `concat` and `transitivity` applied to `transitive_path` display using `@`. It's a bit ugly because it defines the `@` notation twice, but I think it works.

4. The same for inverses: a notation which displays both `inverse` and `@symmetry _ _ (@symmetric_paths _) _ _ _` using `^`.

For 3. and 4. above I followed the principle that *our* definitions of paths are primary, therefore we have the right to call transitivity of paths by its geometric name `concat`. At the same time, by declaring suitable instances and notations, we get to use `transitivity` as a tactic which essentially inserts `concat`.