Homotopy before type theory

Last Friday, the 18th of October, I talked about homotopy and the fundamental group. As I heard about homotopy type theory, I thought that reviewing what I know of the geometric part could be useful. So I prepared this talk, using Allen Hatcher’s free textbook.

Consider a continuous line on the whiteboard, from point x_0 to point x_1, and another continuous line from point y_0 to point y_1. Think of a bijection between the two lines: Continue reading