[HoTT-reading-group] 4/7 (Chapter 7); 4/14 (Chapter 8)

[Jason Gross]

Hi,
Today we spent most of the time discussing modalities in Chapter 7.  At the
end, we proved that double negation is a modality; the Coq proof is
available here<http://hott.github.io/HoTT/coqdoc-html/HoTT.Modality.html#ismodality_notnot>
.

Next week, we will be moving on to Part II: Mathematics!  Please read
chapter 8, focusing especially on the first few sections.  Please look at
and attempt exercises 8.1, 8.2, and 8.6.

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