[HoTT-reading-group] Monday 4/14; 4/21

[Jason Gross]

Hi,
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 Vladimir's proposal for a Homotopy Type
System<http://ncatlab.org/homotopytypetheory/show/Homotopy+Type+System>;
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.

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

For next week (or the week after, if we end up not meeting next week),
we'll continue talking about chapter 8.

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