Applicative Functor の続き

Applivative → Monoidal もできたので一通り終わりました。Applicative Law の使い方がさっぱりわからなかったんですが、

　　pure f <*> x = fmap f x

と、Haskelll の Applicative に書いてあって。これは、さらに関手の uniqueness から出ると。でも、Agda で書いた奴だと、そんな uniqueness なんか証明できそうにないんですが... でも、数字のリストとか、文字のリストとか確かに一意に決まる。

さらにググると、Free Theorem からでるとか書いてある。関手 fmap, fmap' に対して、

g o h ≈ k o f → fmap g o fmap' h ≈ fmap' k o fmap f

で、まさに関手の一意性なんんですが、そんな便利なものがあるのか? と思ったら、

　Agda では証明できないらしい
https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities

個々の具体的な関手では証明できるけど、可能な関手全部とかを取り扱うことはできないとかそんな理由らしいです。

でも、それがわかれば、あとは展開してまとめると同じ形になるって感じでした。