HoTT/book — pull request #686 by mikeshulman (2014-06-20 04:45:13+00:00)
Title: an exercise relating embeddings to left-cancellable maps

from a discussion with Martin Escardo