HoTT/book — pull request #472 by mikeshulman (2013-09-14 20:33:41+00:00)
Title: Fix the construction of the Rezk completion as a HIT

close #464