HoTT/book — pull request #684 by jledent (2014-06-19 13:44:12+00:00)
Title: clash of notations between pairing and union

The \cup notation for the pairing seems strange, and clashes with the \cup in the axiom of infinity next line, which seems to denote the actual union of sets