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