#
Homotopy Type Theory

homotopy (Rev #1, changes)

Showing changes from revision #0 to #1:
Added | ~~Removed~~ | ~~Chan~~ged

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

Revision on October 10, 2018 at 19:57:50 by
Ali Caglayan.
See the history of this page for a list of all contributions to it.