てか誰かも言ってたが、トートロジー的閉ループを構成する証明ってたぶんLEANは向いてないよな
キュービカルAgdaとかでHoTT使わないと計算できないってLEANやってるとわりと色々なAIが言う話だ
俺の独自物理理論もそれだし、IUTもどうやらそれだと今回はっきりしたろ
問題はキュービカルAgdaにはmathlibがないことだろうけどね

LEANにHoTT導入するならunivalenceはどう足掻いても公理化するしかないからその部分は計算不可だし
LEANをcubical Agdaに変換するAIが求められるな