Coqで圏論の会

Masahiro Sakai @masahiro_sakai

Hom_Equality.v を読んでいる。 #concat

Takashi Miyamoto @tmiya_

@masahiro_sakai CategoryというStructureを定義すると自動で作られるコンストラクタです。＞この Build_Category というのは

Masahiro Sakai @masahiro_sakai

@chiguri @tmiya_ ありがとうございます〜 #concat

[1..100]＞＞=pen @1to100pen

新宿に向かって出発。

ω･`)にべべb @2bbb

さっきから全く圏に関係無く代数やってます. #concat?

Yoichi Hirai @pirapira

#concat の合成は、みためが◯なのに、順番が;みたいな順番。

hiratara @hiratara

RT @pirapira: #concat の合成は、みためが◯なのに、順番が;みたいな順番。

Masahiro Sakai @masahiro_sakai

とりあえず、空の圏を定義してみよう。 #concat

kikx @kikx

konnさんの彼女の圏をCoqで定義するぞ #concat

スマートコン @mr_konn

@kikx ごくり……

ω･`)にべべb @2bbb

Structure使って代数構造を定義出来る雰囲気は出て来たし, 準同型も定義出来て来た気がするけど, こっちの方からやってってそれを圏の対象として扱えるのだろうか. 群が成す圏とか, 群を忘却関手でモノイドに移すとかどうやって考えるんだろう. #concat

ω･`)にべべb @2bbb

ということでやっぱConCaT読めって話なんですかね.

ω･`)にべべb @2bbb

個別の群を定義してそれから忘却させてモノイドに落とす関数とかは取り敢えず定義したんだけど意味が無さげ.

kikx @kikx

よしkonnさんの彼女の圏はONE.vをちょっといじったらできた #concat

ω･`)にべべb @2bbb

@kikx 坂井さんがやってる空の圏の中にkonn君の彼女が（ry

kikx @kikx

ONE.v の中の複雑なreturnは最新のCoqだとさすがにいらないレベルだなあ

Masahiro Sakai @masahiro_sakai

.@mr_konn @kikx やったー！ 空の圏(@mr_konn さんの彼女の圏らしい)を定義できた〜！！ #concat

スマートコン @mr_konn

@masahiro_sakai @kikx (´・ω・｀)……

ω･`)にべべb @2bbb

@mr_konn 彼女出来て良かったね！

スマートコン @mr_konn

@2bbb 空の圏じゃ仕方ないです><

Masahiro Sakai @masahiro_sakai

次は、関手と自然変換の定義でも見て行こう。 #concat

ω･`)にべべb @2bbb

@mr_konn 空とは言え空集合だって立派な集合だ！

ω･`)にべべb @2bbb

準同型と準同型の合成は準同型っていうことが証明出来たぞ！

スマートコン @mr_konn

@2bbb 集合じゃなくて圏ですし！

ω･`)にべべb @2bbb

@mr_konn 確かに. でもまあ, 空の圏だって確かにそこに存在するわけですし！