The nCategory Cafe の記事 "Synthetic ∞-Groupoid Theory" 経由で知ったマイク・シュルマン（Mike Shulman）のスライド "Homotopy type theory: towards Grothendieck's dream"。
スライドなので、プラウザ内でスクロールして見るより、ダウロードしてAdobe Readerでページングして見たほうがいいと思います。ページングじゃないと、せっかくのネタが笑えません。
表紙の次のページが"Topos theory"、「群盲象を撫でる*1」の絵ですね。僕は読んだことはないのですが、ジョンストン（Peter T. Johnstone）の "Sketches of an Elephant: A Topos Theory Compendiumm" という二巻本があるようです。この本のタイトルと「群盲象を撫でる」は関係するのでしょう。ちなみに、アウディ（Steve Awodey）による"Sketches of an Elephant"本の書評があります。
さて、スライドの次のページには、Homotopy type theory なら、こんな絵だろう、という象の絵があります。これは笑えます。「群盲象を撫でる」どころの騒ぎではないっ！ てことですね。この象の絵で満足してしまい、表紙入れて3枚しか僕は見てないのです。が、もちろん、それ以降にも有益な情報があると思いますよ。
