[HoTT-reading-group] Meeting on 3/10

[Jason Gross]

Today we talked about higher inductive types.  We discussed the various
restrictions and open problems of higher inductive types (e.g., higher
induction-recursion is not known to be consistent; we don't have systematic
rules for which paths are allowed (though experts will generally agree on
what's safe); we don't know how to write all of the recursion rules).  We
tried and failed to understand a comment by Mike
Shulman<http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/comment-page-1/#comment-29129>
on
which functors can be (higher) inductive types.

We explored an alternate definition of something that looks like the circle
at a first glance, but might not be.  Here's the partial Coq code on
exploring an alternate "circle".<https://gist.github.com/JasonGross/9473619>
(For HoTT/coq; Bruno Barras's partial
implementation<https://github.com/barras/coq/tree/hit> would
reject S1'.)

Next week, we'll continue discussing higher inductive types.  As a
reminder, the suggested exercises from last week are 6.2, 6.5, and 6.9.
 I've realized that 6.5 requires 6.4 to do formally, so feel free to do 6.4
instead of or in addition to 6.5.

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