Homotopy Type Theory homotopy > history (Rev #2)

Idea

Definition

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

Properties

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

See also

• univalence
• function extensionality

References

• HoTT book