<div dir="ltr">Hi,<div>This week, we talked about a variety of things, including how to construct the circle as the homotopy colimit of a diagram containing only the unit type, the difference between homotopy colimits and (regular) colimits, the homotopy groups of spheres, the univalence axiom for categories, simplicial types, and various problems with defining infinity categories in HoTT. (I referenced some posts by Mike Shulman, which are available <a href="http://golem.ph.utexas.edu/category/2012/06/directed_homotopy_type_theory.html">here</a>, <a href="https://golem.ph.utexas.edu/category/2013/03/category_theory_in_homotopy_ty.html">here</a>, and <a href="http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/">here</a>.) We also talked about whether or not one of the axioms for the definition of a modality is redundant, and Chris came up with a counter-example to an idea I had about product-with-the-circle.</div>
<div><br></div><div>For next week, please, again, have read chapter 7 (homotopy n-types). The exercises I suggested last time were 7.1, 7.2, and 7.12. If you're looking for more exercises, feel free to also try 7.5 and 7.14. You can also think about whether or not 7.7.5(iv) is redundant.</div>
<div><br></div><div>-Jason </div></div>