#CATEGORY THEORY FOR PROGRAMMERS
Bartosz Milewski "Category Theory for Programmers"
https://github.com/hmemcpy/milewski-ctfp-pdf
プログラマーが圏論を学習するときに良く参考にされる文献です。
Milewskiは同じ題材の講義を行っており、動画が公開されています。
https://www.youtube.com/user/DrBartosz/playlists
動画の内容を基に圏論について解説したブログが公開されています。
https://bitterharvest.hatenablog.com/entry/2016/11/24/203021
https://bitterharvest.hatenablog.com/entry/2017/03/09/155935
https://bitterharvest.hatenablog.com/entry/2017/10/12/211149
Milewskiの動画には書籍"Category Theory for Programmers"のPart Threeに関する講義は少ないので、Part Threeに関して詳しく知りたい場合には、書籍を参照してください。
現在、この書籍の翻訳が進められており、基本的な内容は日本語で読むことができます。
https://zenn.dev/taketo1024/books/850b20937af93b
以下、"Category Theory for Programmers"について、インデックス程度の情報ではありますが、サマリを作成しました。
##Part One
###1 Category:The Essence of Composition
合成のエッセンス
対象、射、恒等射、合成（結合律、単位律）の定義。
###2 Types and Function
型、関数
型と関数の必要性、純粋関数、シングルトン、Voidに関する説明。
###3 Category Great and Small
空圏、グラフからの圏、順序からの圏、二項演算子からの圏、モノイド圏
具体的な圏の例をあげながら解説。
###4 Kleisli Categories
クライスリ圏
Writer圏を用いてクライスリ圏を説明している。
###5 Products and Coproducts
積と余積
終対象、始対象、双対、積、余積の定義と簡単な例による説明。
###6 Simple Algebraic Data Types
代数データ型
直積型、直和型、分配律（直積と直和の複合）の説明。
###7 Functors
関手
Maybe、Optional、List、コンテナによる関手
関手の合成
関手を圏から圏への射と見なせば、関手を合成することができる（圏の圏）。
###8 Functoriality
関手性
双関手の定義、双関手としての積と余積、代数データ型の関手性、共変関手と反変関手、プロファンクタ
双関手の定義から始まり、積と余積が双関手であること、余積の関手での表現、クライスリ圏で触れたWriter圏を関手で洗練化を行っている。
共変関手、反変関手、プロファンクタで関手の向きに関する説明をまとめて行っている。
###9 Function Types
関数型
写像対象、カリー化、指数対象、デカルト閉圏、型定理、カリー・ハワード同型対応
###10 Natural Transformation
自然変換
自然変換の定義、ポリモーフィズムによる自然変換の記述、関手圏、2-圏
反変関手の反対自然性についても触れている。
##Part Two
###11 Declarative Programming
宣言的プログラミング
圏論でのアプローチと宣言的プログラミングとの親和性。
###12 Limits and Colimits
極限と余極限
錐を定義し、極限を定義している。
錐と圏の抽象化
インデックス圏から錐を構成する圏への関手を対象、関手間の自然変換を射とする圏との同型についての議論
極限の例
引き戻しについて例をあげて説明
余極限の定義
連続関手の定義
###13 Free Monoids
自由モノイド
自由モノイドの定義
自由モノイドの普遍構成
モノイド圏と集合圏を忘却関手でつないで、普遍構成について説明している。
###14 Representable Functors
表現可能関手
表現可能関手の定義
Hom関手と自然性条件を満たす関手
###15 The Yoneda Lemma
米田の補題
米田の補題に関する説明、証明
余米田の補題
米田の補題を反変Hom関手に変えたもの
###16 Yoneda Embedding
米田の埋め込み
米田の埋め込みの説明
前順序集合への埋め込みの例
自然性
評価関手による自然性の説明
##Part Three
###17 It's All About Morphisms
射を中心に圏論の内容のまとめ
関手、可換図式、自然変換、自然同型、Hom集合）、Hom集合の同型射、射の集合の非対称性
###18 Adjunctions
随伴
随伴とunit/counitのペア
随伴の定義、三角恒等式、随伴から導かれる可換図式
随伴とHom集合
Hom集合による随伴の別定義、先に定義したものと同じであることの証明
随伴から導かれる積、随伴から導かれる指数対象
###19 Free/Forgetful Adjunctions
自由忘却随伴
忘却関手によって無視された付加的な構造を追加する自由関手
###20 Monads: Programmer's Definition
Haskellのモナド
クライスリ圏
クライスリ圏を関手で洗練化したものはWriterモナド
フィッシュ・オペレータ、do記法
###21 Monads and Effects
モナドと副作用
Haskellでの副作用の問題に対して、解決策を説明している。
###22 Monads Categorically
モナド
圏論でのモナドの説明
モノイド圏
モノイドとしてのモナド
随伴から導かれるモナド
###23 Comonads
コモナド
プログラミングでのコモナド
Productコモナド、合成の分解、Streamコモナド
圏論でのコモナド
Storeコモナド
###24 F-Algebras
F-代数
F-代数の定義と例
再帰
多項式の環、不動点
F-代数の圏
F-代数の圏の準同型を射として構成した圏
自然数
F-代数で定義した自然数
カタモルフィズム
F-始代数とF-代数での準同型による数学的帰納法
畳み込み
リストの加算の畳み込みの例
余代数
F-代数の矢印を全て反対にしたもの。定義、事例など。
###23 Algebras for Monads
モナドのための代数
T-代数
クライスリ圏
モナドで構成したクライスリ圏
コモナドの余代数 、レンズ
レンズはStoreコモナドの余代数
###24 Ends and Coends
エンドとコエンド
対角自然変換、エンド
対角自然変換を定義し、ウェッジを経て、エンドを定義する
等化子としてのエンド
プロファンクタのエンドがプロファンクタの対角要素をポリモーフィック関数に写す関数の等価子になること
エンドとしての自然変換
エンドの例：自然変換の集合
コエンド
エンドの双対
忍者米田の補題
米田の補題のエンドを用いた書き換え
プロファンクタの合成
プロファンクタを射とする圏
###25 Kan Extenstions
カン拡張
右カン拡張
右カン拡張の定義、カン拡張の埋め込み
随伴としてのカン拡張
右カン拡張が与える随伴
左カン拡張
右カン拡張の双対が左カン拡張
エンドとしてのカン拡張
自由関手
カン拡張から構成される自由関手
###28 Enriched Categories
豊穣圏
モノイド圏
対称モノイド圏、双閉モノイド圏
豊穣圏
豊穣圏の定義
前順序
豊穣圏の例である前順序集合
距離空間
豊穣圏の例である距離空間（ローヴェア）
豊穣関手
関手を豊穣圏に合わせて一般化
自己豊穣
閉対称モノイド圏はHom集合を内部準同型で置き換えることによる豊穣化
2-圏への関連
2-圏は小さい圏上の豊穣化されあたもの
###29 Topoi
トポス
部分対象分類子
部分対象分類子の定義
トポス
初等トポスの定義
トポスとロジック
Predicate（真偽判定）のロジックとトポスについての説明
###30 Lawvere Theories
ローヴェア理論
普遍代数 、ローヴェア理論 、ローヴェア理論のモデル
普遍代数を圏に広げて、ローヴェア理論へ導く
ローヴェア理論の説明を経て、ローヴェア理論のモデルを定義していく
モノイドの理論
モノイドに対するローヴェア理論のモデルの圏は全てのモノイドの圏と同値
ローヴェア理論とモナド
ローヴェア理論から導かれるモナド、有限積モナドから導かれるローヴェア理論
コエンドとしてのモナド
副作用のローヴェア理論
Maybeの例外をローヴェア理論で考察
###31 Monads, Monoids, and Categories
モナド、モノイド、圏に関するより詳しい話題
双圏
双圏の定義
モナド
双圏によるモナドの一般化