[HoTT-reading-group] Today; Next Monday

[Jason Gross]

Next week, I plan for us to do what was actually on the schedule for this
week, namely covering questions on chapters 3 and 4 and reviewing exercises
3.13, 3.14, and 4.5; please come in with the exercises completed or with
questions about how to do them.

I also welcome advice and feedback on the reading group (now or in the
future, in person, or by private email), whether that's "I want to get
*foo* out
of the group, and I'm not getting it" or "keep doing what you're doing" or
"more/fewer exercises" or something else.

Finally, today in the HoTT reading group, we talked about how chapter 4
seems dry to those with no prior knowledge of how the various definitions
of equivalence are used in math, but interesting to those who can connect
them up to various other bits of math; we talked about various notions of
contractibility (inhabited hprop; equivalent to unit; filling of
spheres/holes); a bit about truncation; and I brought up the fact that The
Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly
Invertible<http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-%E2%84%95-%E2%80%96%E2%84%95%E2%80%96-is-nearly-invertible/>,
which was perhaps a mistake, given that I botched the presentation.  I will
leave it up to those interested to read the blog
post<http://homotopytypetheory.org/2013/10/28/the-truncation-map-_-%E2%84%95-%E2%80%96%E2%84%95%E2%80%96-is-nearly-invertible/>,
Nicolai's Agda code<http://red.cs.nott.ac.uk/~ngk/html-trunc-inverse/trunc-inverse.html>,
or my own Coq version of it <https://gist.github.com/JasonGross/9064514>.
 I think the essence of it is that you can extract information even from
contractible types, which I show in a much shorter Coq
example<https://gist.github.com/JasonGross/9064636> involving
Bool, and two values [x] and [y] where we have [x = y] but we have a
(dependent) function [f] with [f x ≠ f y].  (I believe this is related to
the difference between having a path between two points in a fiber, and a
path between those points which lies over the constant path, and how you
can have the former without the latter.)

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