haskell-jp / math #11 at 2021-11-14 17:24:16 +0900

「ziplist monad proof」でググったら Ziplist アプリカティブがモナドにならないことの証明と思われる Coqコードを見つけた。
https://gist.github.com/viercc/38853067c893f7ad9e0894abb543178b （こちらは日本の人のだ）
https://gist.github.com/Lysxia/b105bcb2f2ba835012476ab7fe37ae87

このツイートでやってたらしい。 https://twitter.com/lysxia/status/1451202791796584454