「型理論周辺、何で混乱するのか？」において： 型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです 地雷原になってしまう大きな理由に、ターンスタイル記号 '$`\vdash`$'、二重矢印 '$`\R…