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

...olable proof terms. As discussed in #454.
I guess
@HoTT.Overture.transitive_paths
would be clearer. Would that make you happy?

On Sun, Sep 7, 2014 at 11:45 PM, Andrej Bauer <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))).
>>
>
> What precisely must a person who is familiar with the HoTT book figure out
> about Coq before they can understand this line? How many layers of stuff are
> piled on top of concat? Before it was straightworfward, now it's not.
>
> —
> Reply to this email directly or view it on GitHub.