『プログラマのための圏論:上級編(上)』はこれまで、プログラマのための圏論(上級編)で説明してきたことをまとめました。圏論での重要な概念である、極限、米田の補題、随伴関手についてまとめてあります。
Haskellで下記のデータ型を定義した時にBinat -> Nat型の単射な関数が思いつかず、タイトルの仮説が浮かんだ次第。 なんでそう思ったかの概略 証明する気はないが、なんで実数(とBinat型のすべての値の集合の濃度が同じ)と思ったか、概略を述べておく。 まず、LSuccとRSuccをBizeroに有限回適用して得られる値の集合$B_0$は可算無限集合。 次に、RSuccは有限回、LSuccは可算無限回Bizeroに適用して得られる値の集合$B_1$も可算無限集合。 最後に、LSuccとRSuccをBizeroに可算無限回適用して得られる値の集合を$B_2$として、差集合$B_2 \setminus B_1$を考える。LSuccを0、RSuccを1と読み替えれば、半開区間$(0, 1]$の各実数を二進数の無限小数で一意1に表したものと一対一に対応するので、$B_2 \setminu
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く