圏をつくろう(前編) -Why do we use Coq?-圏をつくろう(前編) -Why do we use Coq?- この記事は Theorem Prover Advent Calendar 2013 の 8 日目の記事です． Packaging Mathematical Structures を参考にして 圏をつくってみた というテーマで，当初はコードを載せてダラダラと説明をする予定でしたが，ちょいと変更し，今回は前編としてその動機たる部分をほんわかと書いていこうと思います． 実際にコードを見ていくのは後日載せる予定の後編になります． なお，記事は会話形式です．被ってしまった． 「こんにちは」 「こんにちわー」 「今日は定理証明系と圏論，両方に関わる話をしていきたいと思います」 「はーい」 「具体的には，定理証明系の上で圏をつくってみよう，というお話です」 「なるほどー」 「定理証明系には幾つかありますが，今回は Coq を使って進めていき
