インスティチューションでは、指標Φに対してモデル圏Mod[Φ]が決まる。まーこれはいいのだが、指標圏が何であるか、Mod[Φ]をどう作るかは言及しない。公理的フレームワークだから、まー、そんなもんだ。しかし実際に出現するインスティチューションではもっと…

C-c C-n しか憶えてない。http://proofcafe.org/wiki/ProofGeneral より： command action C-c C-n 1ステップ進む C-c C-u 1ステップ戻る C-c C-Enter カーソル位置まで進める C-c C-a C-o SearchPattern C-c C-a C-p Print C-c C-a C-c Check C-c C-a C-s S…