Homotopy Type Theory homotopy > history (changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Idea

Definition

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

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

Properties

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

See also

References

Last revised on June 9, 2022 at 20:31:19. See the history of this page for a list of all contributions to it.