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