型付きラムダ計算に対する“デカルト閉圏による意味論”、あるいは“カリー／ハワード対応”においては、型付きラムダ項の計算（書き換え、変換）だけではなくて、シーケント計算が必要になります。型理論では、シーケントを型判断（type judgement）と呼ぶこと…