Predicativity

超討厭 = =。看來真的沒辦法把 sets 的層級壓下來。那…全部提上去如何？Coq 裡面好像已經有 universe polymorphism，那乾脆把 AoPA 移植到 Coq 算了 XD。

--
顯然我的潛意識認為寧可把 AoPA 整個翻修一遍也不要再造那麼多版本的 arrows XD。

---

看來目前還是 scm 老師說的 "specialised versions" 比較可行一點點。不如就寫得很醜很醜，然後當作支持 universe polymorphism 的好理由 XD。

--
前途一片黯淡啊 XD。