型理論の人々は「判断形式で書かないと死んでしまう」のでしょうか？ そして、判断形式にターンスタイル（'$`\vdash`$'）とコロン（'$`:`$'）以外使ったら死んでしまう」のでしょうか？ターンスタイルとコロンへの執着は、もはや「好みの問題」の域を超えて…