[HoTT-reading-group] Bool ≃ (Bool ≃ Bool)

[Jason Gross]

I've put the code at
https://github.com/JasonGross/HoTT/blob/0bbd692f9465364763319368a4c424301fa503a8/theories/types/Bool.v#L113(also
https://github.com/JasonGross/HoTT/blob/0bbd692f9465364763319368a4c424301fa503a8/theories/Misc.v#L93,
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
http://hott.github.io/HoTT/proviola-html/HoTT.types.Bool.html#equiv_bool_equiv_bool_bool_helper

-Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.mit.edu/pipermail/hott-reading-group/attachments/20140127/afae872a/attachment.htm