Homotopy Type Theory
homotopy (Rev #2)



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


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


Revision on October 11, 2018 at 08:58:44 by Ali Caglayan. See the history of this page for a list of all contributions to it.