<div dir="ltr">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 href="http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/comment-page-1/#comment-29129">a comment by Mike Shulman</a> on which functors can be (higher) inductive types.<br>
<div><br></div><div>We explored an alternate definition of something that looks like the circle at a first glance, but might not be. <a href="https://gist.github.com/JasonGross/9473619">Here's the partial Coq code on exploring an alternate "circle".</a> (For HoTT/coq; <span style="font-size:13px;font-family:arial,sans-serif">Bruno Barras's </span><a href="https://github.com/barras/coq/tree/hit" target="_blank" style="font-size:13px;font-family:arial,sans-serif">partial implementation</a> would reject S1'.)</div>
<div><br></div><div>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.</div>
<div><br></div><div>-Jason</div></div>