Homotopy Type Theory and Univalent FoundationsHomotopy Type Theory and the Univalent Foundations of Mathematics Homotopy type theory refers to a new interpretation of Martin-Löf's constructive type theory into homotopy theory. Propositional equality between intensionally distinct terms is interpreted as homotopy. The interpretation makes use of methods from abstract homotopy theory such as Quillen model categories, as well as related methods
