Bringing this thread back to David's original announcement of his new
result, one thing that intrigues me about it is that proceeds by
constructing successive approximations to the desired path space and then
taking a sequential colimit.  This reminds me of some other sequential
constructions that also achieved surprising (to me) things, like Egbert's
join construction for building propositional truncation out of nonrecursive
HITs, and the splitting of a quasi-idempotent by a sequential (co)limit
that Lurie used in higher category theory and I then adapted to HoTT.  I
wonder if there are other surprising applications of this principle.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CADYavpzinvAW_PgLUPbp4NyykJxhEbmBsQSC6rQroZWCcFg9xw%40mail.gmail.com.