<div dir="ltr">Hi,<div>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 <a href="http://hott.github.io/HoTT/coqdoc-html/HoTT.Modality.html#ismodality_notnot" target="_blank">here</a>.</div>


<div><br></div><div>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.</div><div><br></div>


<div>-Jason</div></div>