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

...olable proof terms. As discussed in #454.
I think we agreed not to use smoke and mirrors.

On Mon, Sep 8, 2014 at 7:02 PM, Jason Gross <notifications@github.com>
wrote:

> In contrib/HoTTBook.v:
>
> > @@ -69,7 +69,7 @@ Definition Book_2_1_1 := @HoTT.Overture.inverse.
> >  (* ================================================== lem:concat *)
> >  (** Lemma 2.1.2 *)
> >
> > -Definition Book_2_1_2 := @HoTT.Overture.concat.
> > +Definition Book_2_1_2 := (fun A => (@transitivity _ (@paths A))).
> >
>
> @spitters <https://github.com/spitters>, if you include the Notations I
> gave for @concat, @Overture.concat, and @HoTT.Overture.concat, then
> reverting this line is possible. Of course, then the line is somewhat of a
> deception, and you have to trace the usage of the notation.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/459/files#r17251265>.
>