HoTT/HoTT — pull request #554 by JasonGross (2014-10-06 19:38:32+00:00)
Title: Break a loop that shows up with Keyed Unification

Without keyed unification, `rewrite` inferred that a particular endpoint
of a particular path was `((1 ∘ x ∘ 1) x2)`. However, in the goal, this
endpoint was passed as (the judgmentally equivalent) `x2`. So after
`rewrite` finished filling in its holes, it couldn't find the subterm
anymore, breaking the loop. With keyed unification, it can find the
subterm, so the rewrite loops.

Perhaps we want to factor this bit of logic out into a separate tactic with the spec "replace all `transport P p` with `transport idmap (ap P p)` for non-`idmap` `P`"? (Would this go in HoTT.Tactics? Basics.PathGroupoids?)