HoTT/HoTT — pull request #635 by mikeshulman (2014-12-08 06:56:53+00:00)
Title: Splitting of coherent idempotents

An answer to a question of Martin Escardo.