Just $ A sandbox

(追記) 解決した: variable-free type theoryの圏論的な解釈について - Just $ A sandbox -- 文献に突然登場して？ってなったので. 調べても情報がヒットしないのでよくわからないけど, simply typed lambda calculusを変数を使わずに定義するものらしい. で, STLCかなんかでうまく解釈できるかと思ったけど思いつかなかっ…