Extensible Effectsという、大変有名なモナドの合成方法があって、まぁこれはいいんだけど、関連する話でFreer monads, more extensible effectsという論文があり、これまた界隈では有名なんだけどなんやねんって話。 とりあえずext effはモナドを直和してい…

Category TheoryのFormalizationがらみの話。 Category TheoryのFormalizationをするときは、基本的にSetoid-enrichedでやるのが筋がよいということはこの業界(？)では有名な話だし、少し前のブログ記事にも書いたのでそのことを前提として次のようなことを…

最近Coqをかいていて、まぁ自分は基本姿勢として「CoqにはProof Assistantの方向性として共感できないのでもっとよいものが出てきて早く駆逐してほしい」だったのだけれど、 たくさん書いてると多少偏見もなおって考えを改めたりした部分があるのでまとめる…

最近書いてるCoqの話。 主にこれの解説をします: Yoneda.v · GitHub Setoidをベースにすることについて 多分圏論formalize業界(狭そう)では有名な話。 Coqの場合はSetoidのequalityに対してもrewrite tacticが使えるのでそれでやる。 Proper Setoid morphism…

Coq 8.6をインストールしたときのあれこれ Coqのインストール Coq/SSReflect/MathCompの設定 これの通りにやるだけ aptのパッケージは古いからだめってあったので言われたとおりにopamでいれた それと~/.opam/4.04.0/binにパスを通すのもやった. どうもopam…