Coqで圏論の会

Coq

議題

名前空間を完全に分離したいときは、ファイルを分けるのが無難。
Coq内でのLoad Pathの設定方法
Add LoadPath "~/src/coq/ConCaT" as ConCaT.
Print LoadPath.
Require Export ConCaT.SETOID.Map2.
structureをlocalにできるのか？
ConCaTのインストール

makeの動作がおかしい。直接contribフォルダにConCaTをコピーして解決した。
coqmakefileを使ってみる?

Constructorの使い方は？

Definition x:int := 3.
CategoryTheoryのONEにいろいろ例がある。

Proof中のセミコロンとピリオドの違い

セミコロンにすると、サブゴール全部に以下を適用する。

Hint Resolveってなに？
Build_Equivarenceって何？

これがコンストラクタ。

Coqで2つゴールが出たときに変更する方法は？
trivialはちょっとだけ自動化してくれる。
redはreduction。何かをreductionしてくれる。
GoalにTrueが出たときは？

auto.で終わり。apply I. IがTrueの定義。

Canonical Structureって何？
中間成果物

- http://ideone.com/Nt7n6
- http://gist.github.com/954854

@を使うと型を明示できる（Implicitが無効になる）
AxiomとDefinitionの違い

Definitionは実体がないとダメ。
Axiomは型だけでよい。

Category Theoryの証明コード

Coq8.2用ですが。
http://mattam.org/repos/coq/cat/

おひらき
Inductive One_ob : Type :=
    Obone : One_ob.

Check One_ob.

なんでこうすると、One_obの型が、Propになるの？

  • 代数の圏が圏になることの証明(酒井さん)
    • ConCaTでは独自のSetoid使ってるので、いちいちapplyをしていった。
    • 簡約するのに必要なだけunfoldしておくと、いっきにsimplできる。
  • Allegories(たけをさん)
    • SetとRelationの一般化
    • CategoryにOrderとConverseを付け足す
    • これを使って任意のAllegoryからCategoryに落とすのをやりたい。
    • AllegoryのStructureを新たに定義すればいいはず。
    • Converseの途中で終了。
  • Heyting AlgebraがCCCであることの証明
    • latticeのStructureの定義だけで大変。
  • 練習問題的なもの
    • Zero圏
      • Proof.contradiction.Qed.
    • 合成がmonicだったら、とか
      • rewriteができなくて苦戦。
      • epicとmonicを定義してあるCat.Property。Monic_low,Epic_lowの引数定義順が逆になってた。