<div dir="ltr">I've put the code at <a href="https://github.com/JasonGross/HoTT/blob/0bbd692f9465364763319368a4c424301fa503a8/theories/types/Bool.v#L113">https://github.com/JasonGross/HoTT/blob/0bbd692f9465364763319368a4c424301fa503a8/theories/types/Bool.v#L113</a> (also <a href="https://github.com/JasonGross/HoTT/blob/0bbd692f9465364763319368a4c424301fa503a8/theories/Misc.v#L93">https://github.com/JasonGross/HoTT/blob/0bbd692f9465364763319368a4c424301fa503a8/theories/Misc.v#L93</a>, for the version that doesn't depend on an extra hypothesis). If anyone has questions, I'll be happy to elaborate/add more comments. Eventually, when this gets merged, you'll be able to follow the proof interactively at <a href="http://hott.github.io/HoTT/proviola-html/HoTT.types.Bool.html#equiv_bool_equiv_bool_bool_helper">http://hott.github.io/HoTT/proviola-html/HoTT.types.Bool.html#equiv_bool_equiv_bool_bool_helper</a><div>
<br></div><div>-Jason</div></div>