最近書いてる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…