<div dir="ltr">Hi,<div>Yesterday, we began chapter 8.  We talked about covering spaces (specifically of the circle), how univalence comes up in the universal cover of the circle, and how the encode-decode method relates to fibers and universal covers.  We touched briefly on the notion of an identity system.  We talked about <a href="http://ncatlab.org/homotopytypetheory/show/Homotopy+Type+System">Vladimir&#39;s proposal for a Homotopy Type System</a>; Vladimir wants something as strong as possible, so we can found mathematics in it, Mike Shulman wants to have a weaker theory that can be the internal language of more categories.  We also talked about what judgmental rules you can have, and whether strict equality should be interpreted as on-the-nose-equality, or canonical paths, etc.</div>

<div><br></div><div>Next Monday is Patriot&#39;s day, but I&#39;m happy to meet.  Please email me privately by Friday at midnight if you plan to come; I&#39;ll cancel if no-one is interested, but will otherwise show up.</div>

<div><br></div><div>For next week (or the week after, if we end up not meeting next week), we&#39;ll continue talking about chapter 8.</div><div><br></div><div>-Jason</div></div>