上限を適当に決めて，サイズがそれ以下の lambda term の個数はいくつになるか計算してみました。本当に項の個数を数えると変数の名前を変えるだけでいくらでもできるので，自由変数として使える変数の個数を制限します。この条件は都合のいいように設定した…

すっきり証明する方法を考えました。概要。 right adjoint preserves terminals*1 limit is a terminal of a cone category adjoint between categories induces an adjoint between cone categories 証明を厳密に全部書き下したら結局すっきりしてないんで…