path concat

[zstone1]

The most technical of all the parts of #1350. This proves that path concatenation has left/right identities, and associates, up to reparameterization. The current proofs are slow, ugly, and ill-named. They are, however, correct.

Checklist

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

• [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels