Introduction – from type theory and homotopy theory to univalent foundations

摘要

We give an overview of the main ideas involved in the development of homotopy typerntheory and the univalent foundations of Mathematics programme. This serves as arnbackground for the research papers published in the special issue.