Emphasise that the homotopies being discussed are all endpoint-preserving

[Rotsor]

Chapter 2 -- Homotopy type theory -- defines homotopy between paths p and q as a continuous map f from [0, 1] × [0, 1] to a space X such that f(0,-) = p and f(1,-) = q.

This definition misses the very important point that homotopies being discussed later in the chapter are endpoint-preserving homotopies -- such that f(-,0) = const x and f(-,1) = const y.

The only point where I could find a similar notion discussed is the mention of based homotopy inside brackets in the discussion of loops.

The distinction is especially important because for any p and q : x = y there exists a homotopy between them, but there is often no endpoint-preserving homotopy.

[mikeshulman]

You confused me for a moment, because most topologists I know would call those endpoint-preserving homotopies (a "based" homotopy meaning the domain and codomain are spaces equipped with basepoints and the homotopy is constant on the basepoint). But I think you're right, that should be clarified. The notion of endpoint-preserving homotopy is mentioned a bit later in the context of fundamental groups, but it also applies of course to all homotopies between paths.

[awodey]

we don't define homotopies in terms of continuous functions from the interval at all. that's just for conventional intuition -- homotopies are actually defined in terms of identity types, which are primitive.

On Jul 19, 2013, at 4:04 AM, Rotsor notifications@github.com wrote:

Chapter 2 -- Homotopy type theory -- defines homotopy between paths p and q as a continuous map f from [0, 1] × [0, 1] to a space X such that f(0,-) = p and f(1,-) = q.

This definition misses the very important point that homotopies being discussed later in the chapter are based homotopies -- such that f(-,0) = const x and f(-,1) = const y.

The only point where I could find the notion of based homotopy mentioned is inside brackets in the discussion of loops.

The distinction is especially important because for any p and q : x = y there exists a homotopy between them, but there is often no based homotopy.

— Reply to this email directly or view it on GitHub.

[Rotsor]

mikeshulman, sorry, I'm very new to topology. I've updated the text to reflect your comment.

awodey, indeed that topological definition (on the first page of Chapter 2) is only there to form intuition. As a person first learning about homotopies from this book, I can tell that the definition being imprecise only causes confusion instead.

[mikeshulman]

(or homotopies "rel endpoints", but I've never really liked that)