なんというバカバカしさ、なんという無駄、なんという浪費！ ラムダ計算 インスティチューション 型理論 型コンテキスト 指標 型前提（域側） 大きなラムダ式 クライスリ指標射 型判断（シーケント） 大きなラムダ計算 指標圏の計算 型証明計算 レコード（値…