>>266
>>添え字の意味を押えながら このdiagramを言語化・コード化する必要があります
>ならばそれは数式の説明およびコード化の面倒さですね
>それは本文部分には無いものですか？

はい
ですから、図式＝diagram で 軽く 記述しているところの
すべてを Leanの言語に落とさないといけない
正確にね

そして、正確にLeanの言語に落とした 望月IUTのLean化された論文について
Leanの検証プログラムにかける
そうすると、ギャップの有無（エラーの有無）が分る
ギャップ無しならOK

ギャップ有りなら ギャップのカ所が特定されているので
そのギャップを埋められるかどうか？

もし 何かのギャップを簡単に埋められるならば、望月IUTは成立していることになる
逆に、ギャップを埋めらられないならば、望月IUTは不成立です
（ギャップを埋めらられない→根本的に書き直し）