HoTT/HoTT — pull request #453 by JasonGross (2014-09-02 02:56:45+00:00)
Title: Revert "Remove [path_via]"

This reverts commit dd9121da211cdcb3cdb434a0da2cf10b178eee58.

As per @mikeshulman's
https://github.com/HoTT/HoTT/pull/451#issuecomment-54104523:

> I don't understand why we are so cavalier about replacing a tactic
> that's used throughout the library by a tactic that does something
> different. I think we should revert this change and then continue the
> discussion about the advantages and disadvantages of all possible
> options before making a decision.

> My experience suggests that even if we manage to make transitivity
> "pretend" that it is just concat, eventually it will bite someone
> somewhere.

> Also, there's undoubtedly a reason why we added `auto with path_hints`
> to `path_via`. Is the questionable advantage of calling the tactic
> "transitivity" worth having to type that manually every time we need
> it?