Using the standard (type class based) transitivity tactic for more contr...

...olable proof terms. As discussed in #454.
I think, by convention, this should be `@HoTT.Overture.transitive_paths`, not `@transitive_paths`.