Homotopy Type Theory homotopy

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

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

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