>>610 追加
書棚の”こやし”Steve Awodey 圏論 前原 和壽訳
訳者あとがきで Homotopy type theory、Voevodsky の話がある
ここらは、2009とか2012–13という年代が挙げられているので
望月氏は、Homotopy type theoryは 殆どご存知ない気がします　（＾＾；

(参考)
https://www.kyoritsu-pub.co.jp/book/b10003662.html
圏論 原著第2版 Steve Awodey 著・ 前原 和壽 訳 2015/09/20
圏論が多分野に普及して30年を経た現在、誰もが読める圏論の本が必要だ――本書はこのモチベーションで執筆された。予備知識がほとんどない読者のために、例として半順序集合と半群がゼロから説明され、最後までそれらを用いて話が展開されている。これらのほかにも例が豊富に取り上げられている。なお、予備知識がほとんど必要ないとはいえ、数学的な厳密性は損なわれていない。すべての重要な命題と定理には完全な証明が付されている。本書は情報科学や論理学など、さまざまな分野へ役立てられるであろう。
https://www.kyoritsu-pub.co.jp/book/b10003662.html
序文pdf 詳細目次pdf

https://en.wikipedia.org/wiki/Homotopy_type_theory
homotopy type theory (HoTT) includes various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory applies.
History
Early history: model categories and higher groupoids
These results were first presented in public at the conference FMCS 2006[5] at which Warren gave a talk titled "Homotopy models of intensional type theory", which also served as his thesis prospectus (the dissertation committee present were Awodey, Nicola Gambino and Alex Simpson).
The univalence axiom, synthetic homotopy theory, and higher inductive types
Also in 2009, Voevodsky worked out more of the details of a model of type theory in Kan complexes, and observed that the existence of a universal Kan fibration could be used to resolve the coherence problems for categorical models of type theory.
The next pivotal event was a mini-workshop at the Mathematical Research Institute of Oberwolfach in March 2011 organized by Steve Awodey, Richard Garner, Per Martin-Löf, and Vladimir Voevodsky, titled "The homotopy interpretation of constructive type theory".
Soon after the Oberwolfach workshop, the Homotopy Type Theory website and blog[26] was established, and the subject began to be popularized under that name. An idea of some of the important progress during this period can be obtained from the blog history.
Special Year on Univalent Foundations of Mathematics
In 2012–13 researchers at the Institute for Advanced Study held "A Special Year on Univalent Foundations of Mathematics".[31] The special year brought together researchers in topology, computer science, category theory, and mathematical logic. The program was organized by Steve Awodey, Thierry Coquand and Vladimir Voevodsky