[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…