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