Cubical Agda の続き

結構、難航してて

まぁ、でも、List Bool と ℕ の対応とかが書きやすくなるらしい

けど、Path とか出てくるので、微妙に一般的でないような

そして、

　　Agda での data の展開との相性がよろしくない

自動的に展開すると、cubical agda の warning をくらう

それでも、一段落したんですけど、赤黒木と Galois の方が、かなり難しい。あと zorn もか

証明の難易度が少し上がることは確か。自動変換とかできないのかな?

まぁ、でも、ゆっくりやるか