In January 1984, Alexander Grothendieck submitted to the French
National Centre for Scientific Research his proposal “Esquisse d’un
Programme.” Soon copies of this text started circulating among
mathematicians. A few months later, as a first-year...
The following text is excerpted from the introduction to the
book Homotopy Type Theory: Univalent Foundations of
Mathematics, written jointly by the participants of the special
year on univalent foundations, which may be obtained at