望月氏の論文の最後の部分は改善の余地がある気がした
最後にグロタンディークの圏論仲間のJoyalの組合わせ論的種の理論を使って
log-theta-lattice周辺の状況がちゃんと定義できてることを有限的に主張してるってところ
種の理論は組み合わせとか置換の母関数の圏で演算を表示する仕組みだけど
離散数学で種の圏が半環になってその演算で組み合わせ構造を簡易化みたいな使い方するものだと思う
（計算機科学とかで使われてHaskellにライブラリがあるらしいけど
そもそもこの理論自体が衒学趣味っぽいし例を見る限り圏でやる理由がよくわからない）
今回望月氏は種の圏の射が自然変換だからフォンノイマン順序数のような状況を起きることを利用して
0の種に集合論的論理式を割り当てて・・・のような議論をしているけど
種の理論のこの仕組みは今じゃ弱２圏とわかっているので、やるんだったらこちらに書き換えて一般化してほしい
Cellとかにすれば2000年代以降の一連のｎ圏ブームによる新しい圏論インフラと合流して一気に汎用化すると思う
（望月氏の圏論の情報源が60〜70年代とかの古典ばかりなので）
あとZFCの部分の議論はやり方が変なので省いてほしい、今のｎ圏の枠組みだと公理的集合論は必須でもないから