[[!redirects homotopic]] ## 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 $$(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]] ## See also ## * [[univalence]] * [[function extensionality]] ## References ## * [[HoTT book]]