Skip to main content

Homotopy type theory is a flavor of type theory – specifically of intensional (Martin-Löf-) dependent type theory – which takes seriously the natural interpretation of identity types as formalizing path space objects in homotopy theory. (from nLab)

References:
nLab