Homotopy Type Theory
homotopy

Idea

Definition

Let f,g: (x:A)P(x)f,g : \prod_{(x:A)}P(x) be two sections of a type family P:A𝒰P: A \to \mathcal{U}. A homotopy from ff to gg is a dependent function? of type

(fg) x:A(f(x)=g(x))(f \sim g) \equiv \prod_{x : A} (f(x) = g(x))

Properties

Note that a homotopy is not the same as an identification f=gf = g. However this can be made so if one assumes function extensionality

See also

References