agda

ちんたら、進んでます

細かくって良くわからん

って自分で書いてるわけなんだが

Cubical compatible にしてるんだが、最初からそうしておけば良かった