[HoTT]HoTTをこっそり学ぶ その10 さて、すでに終盤に突入している。2.4.1節に取り組もう。ホモトピー解釈からさらに進んで、Martin-Lf型理論をホモトピー理論の論理学としたいのである。 2.4. Higher algebraic structures ホモトピー解釈によって本質的に…

[HoTT]HoTTをこっそり学ぶ その9 2.3節の後半。実際のところモデル圏であることの確認はかなり難しいようであるが、それをいったん認めて、本題である内包的型理論のモデルへと話を進めてみよう。 （2.3. Homotopical models of type theory の続き） 今や型…

[HoTT]HoTTをこっそり学ぶ その8 さて、Steve Awodey "TYPE THEORY AND HOMOTOPY"の勝手に翻訳シリーズもいよいよ佳境である。2.3節ははっきり言って急に難しくなっている。今までは何だったんだ。まずは2.3節の前半。 2.3. Homotopical models of type theo…

[HoTT]HoTTをこっそり学ぶ その7 さて、Steve Awodey "TYPE THEORY AND HOMOTOPY"の勝手に翻訳の続きである。もちろん翻訳そのものが目的ではなく中身の解読がメインである。今回は第2章 The homotopy interpretationの2.2節まで、いろいろ調べ物をしながら…

[HoTT]HoTTをこっそり学ぶ その6 いろいろぐぐっているうちに次のAwodey氏のレビューペーパーを見つけた。Steve Awodey "TYPE THEORY AND HOMOTOPY" 2010これもarXiv.orgで無料で手に入る。こんないいのがあるなら早く教えてよって感じである。全部20ページ…

[HoTT]HoTTをこっそり学ぶ その5 今回はHoTT Bookにもどってみる。このテキストは"HoTT Book"でぐぐれば公式でPDFを無料でゲットできる。さて、まだ１章のFoundationを少しずつ読み進めている段階であるが、Introductionを読み返してみるとちょっとわかった…

[HoTT]HoTTをこっそり学ぶ その3 Martin-Lfのextensional版とintensional版についてもう少し追及してみる。その後の調査では、というようなidentity typeの導入（intensional identity typeと呼ばれるそうな）があるものをintensional版と理解すればよいよう…

[HoTT]HoTTをこっそり学ぶ その2 さて、まずはMartin-Lf依存型理論というのを勉強せんといかんわけだが、調べれば調べるほどなんだかとっ散らかっている感がある。標準的な定式化というのがあるようなないような、バリエーションも多く、表記の違いなのか何…

[HoTT]HoTTをこっそり学ぶ その１ HoTT始めました。HoTTとはHomotopy Type Theoryの略語であり、またその最初のテキスト（？）である『Homotopy Type Theory Univalent Foundations of Mathematics』というタイトルの本（電子本もネットに落ちている）も指し…