#
Homotopy Type Theory

homotopy

## 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

## References