ちょっと空いた時間にLEANで圏論をやってる． 自然変換の等価性を証明するときに困ったけど，友達に聞いて解決したので備忘録． 結論から言うと， 構造体を要素に分解するときはcases_onを使う． cc tacticは便利． 構造体hogeで説明（？） 次のようにして構…

本業の方の研究が進んだと思った一時間後にダメだったことが判明した。今の方針で進んだ先の反例が分かったという意味は進捗があったが、バックトラックすることになりそう。もー