Setoid-based Constructive Category Theory in Coq 概要 Setoid をベースにして圏や関連する概念の定義と証明をしていこうという個人プロジェクトです。 Universe Polymorphism を利用しています。 用法 git clone https://github.com/mathink/Cat_on_Coq.git COC