[HoTT-reading-group] Chapter 7

[Jason Gross]

Hi,
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
here<http://golem.ph.utexas.edu/category/2012/06/directed_homotopy_type_theory.html>,
here<https://golem.ph.utexas.edu/category/2013/03/category_theory_in_homotopy_ty.html>,
and here <http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/>.)
 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.

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.

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