HoTT/book — pull request #748 by Pierre-Yves-Gaillard (2014-12-19 06:19:52+00:00)
Title: Last rule of Section A.2.2, lines 591 and 592

In the last rule of Section A.2.2 I put

* A : \UU_i instead of A \equiv A' : \UU_i in the first hypothesis, and

* B : \UU_i instead of B \equiv B' : \UU_i in the second hypothesis.

(See lines 591 and 592 of https://github.com/HoTT/book/blob/master/formal.tex#L591.)

I think this corrects a typo, but I am far from being sure I am right.