圏論勉強会第７回

(T,in)がF始代数ならば
(|in|)=1T(反射則)
またh∘f=g∘F(h)　①が成り立つならば
h∘(|f|)=(|g|)　　　②　(融合則)

sum∘filter(even)を一つのfoldrで表せ。

まず
p(a,as)=　　cons(a,as)　(even(a)=trueの時)
　　　　　{　as　(それ以外)
とするとfilter(even)=(|[nil,p]|)となります。
　　このfilter(even)=(|[nil,p]|)が②の(|f|)に対応する

 よってsum∘[nil,p]=[c,g]∘(11+1A×sum)　③　を満たすc,gを見つければ融合則が使えます。
　　　①に対応する式が③　　　また、[nil,p]が①のfに対応している。　sumはｈに対応。

これをpointwiseな等式に書き直すとまずc=sum(nil)=0であり,
　　　　∵③式の左の要素どうしが等しいことから

　　g(a,sum(as))=　sum(cons(a,as))=a+sum(as)　　(even(a)=trueの時)
　　　　　　　　　　{　sum(as)　　　　　　　　　　　　　　(それ以外)
が成り立てば良いので,
　　　　∵③式の右の要素が等しいから　p適用後sum適用つまり、sum(p(a,as))　＝sum適用後ｇ適用つまり　g(a､sum(as))　ということか

g(a,x)=　　　a+x　(even(a)=trueの時）
　　　　　{　　x　　　(それ以外)
とすれば良いです。すなわち(|[0,g]|)=foldr(g,0)が求める関数です。

圏論 P19

Cの対象Cのもとでの余スライス圏C/Cとは、対象としてdom(f)=CをみたすCのすべての射ｆをもち、ｆ：C→Xからｆ’：C→X'への射はｈ・ｆ＝ｆ’となる射ｈ：X→X’である。さて、スライス圏の定義から、余スライス圏の定義の残りの部分を実行してほしい。スライス圏および双対構造の用語により、余スライス圏はどのように定義されるであろうか？
　　　　ｈ
　　X　→　X’
　　ｆ↖　　↗ｆ’
　　　　C

　C/Cでは、ｆ、ｆ’が対象　　ｈが射　？

例１．８　点付き集合の圏Sets*は　与えられた点a∈Aをもつ　集合Aからなり、射ｆ：（A,a）→（B,b)は’点’を保つ。すなわちf(a)＝ｂをみたす写像ｆ：A→Bである。これは、一つの要素からなる任意の集合１＝｛＊｝の’もとで’、集合の余スライス圏と同型である。
　　　　　　　　　　Sets*≅１/Sets

実際、写像ａ：１→Ａは要素a（＊）＝aに一意に対応し、射ｆ：（A,a)→（B,b)はちょうど次の可換三角形に対応する。　　　　　　a
　　　　　　　　　　　　１　→　A
　　　　　　　　　　　　　ｂ↘　↓ｆ
　　　　　　　　　　　　　　　B

わかりやすいサイトです。参考にさせていただきました。