Terminal and intial objects

4.1: Terminal and initial objectsのノート

### Kleisliカテゴリーの構築

1. オブジェクト$a$, $b$を持つカテゴリーCがあったとして、ここからKleisliカテゴリーを作る。
    ![ck1.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/e0fd1554-f065-ed90-3479-84ecec52e1d1.png)

2. 同じオブジェクトとArrowを持つKleisliカテゴリを作る。CとKleisliで、$a \to b$の意味が異なるため、このままでは成立しない。

    ![ck2.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/b3497815-2a23-f5d2-be61-aee32a0cbeb3.png)

3. Cの全てのオブジェクトを、stringとのTupleにマップする。$a \to (a, string)$。これを、$m\; a$と書くことにする。Cの$a \to m\;b$が、Kleisliの$a \to b$に対応するArrowになる。

    ![ck3.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/e1c2734a-f2c7-6a52-2706-de74d0f5f9aa.png)

4. Cの$a \to m\;b$の終点と、$b \to m\;c$の始点が一致しないので、このままではComposeできない。KleisliのCompositionの裏側で、$a \to m\;b$のあとで、$m\;b$から$b$を取り出して、$b \to m\;c$という実装を$C$サイドで行うことにする。（このようなやり方が常にできるわけではない）

    ![ck4.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/39ee113b-c8fe-3917-baa0-13a36d6b677a.png)

5. Kleisliオブジェクトのidentityは、CオブジェクトからCオブジェクトと空文字列とのTupleへのマッピング$a \to (a, "")$になる。

     ![ck5.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/53e40cef-19d7-9803-261a-fd845c1c9c97.png)

6. Associativityを満たすためには、Arrowをどの順序で合成しても問題ないことを証明する必要がある。今回のstringの結合はAssociativeなので問題ない。

CompositionとIdentityが実装されていて、CompositionにはAssociativityがあるので、右の図はKleisliカテゴリーということができる。
また、右の図がKleisliカテゴリーならば、左の図の　$x \to m\;a$はMonadになる。

これはたくさんあるMonadの定義の中の１つ。

### Isomorphism (2.1での説明のRecap)
InvertibleなArrowのこと。

#### 定義
$f$または$g$がIsomorphic：

![isomor.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/681fdedf-6162-e4da-3f44-fa5314c91272.png)

$f \to g = id\;a$
$g \to f = id\;b$

### Setと型 (2.2での説明のRecap)
Setは型のモデルになっている。

#### SetとLogic
セットの要素をマップする関数は、Logicでの証明に対応する。

#### 空のセット
HaskellではVoid型と一致する。（手続＃き型の言語で一致する型はない）
要素がないのでコンストラクタもない。

##### LogicでのVoid
Logicでは、Voidはfalseと一致する。

##### Voidを引数に取る関数
存在する。Haskellではabsurd関数として定義されている。Logicではfalseからなんでも導くことができるので、戻り値は多相になっている。

$absurd :: Void \to a$  

##### VoidのIdentity
VoidのIdentityも存在する。
$id\;Void :: Void \to Void $

#### 1要素のセット
Singletonのセットは、（）と書いてUnitと呼ぶ。HaskellでのUnitの型は（）と書く。

##### LogicでのUnit
Logicでは、Unitはtrueと一致する。

##### Unitが戻り値になる関数
()をポイントするArrowになる。
$unit :: a \to ()$

##### Unitを引数に取る関数
例えば、
$() \to Int$

は、

$one:: () \to Int$
$two:: () \to Int$

の形でいくらでも定義することが出来る。カテゴリーでは、これを使って、オブジェクトに含まれる要素を定義する。この要素を、Generalized elements of an objectという。

#### 2要素のセット
booleanに対応する。

##### ターミナルオブジェクト
Singletonセットには、その他の全ての要素から向かうUniqueなArrowが１つ存在する。

![singleton.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/0ac8ebcc-c28c-881e-a764-601fc5847f7a.png)

自身以外の全てのオブジェクトからのユニークなArrowが存在するオブジェクトをターミナルオブジェクトという。全てのカテゴリに存在するわけではない。

![terminal.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/1b6e3fd1-beed-793e-c30d-c3509a9a67f2.png)

###### 定義
1. $\forall a\, \exists f :: a \to ()$
2. $\forall f :: a \to (), g :: a \to () \implies f = g$

###### 例
Thin categoryでは、Arrowは $\leq$ の意味なので、最大のオブジェクトがターミナルオブジェクトになる。

![thin-term.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/acd24037-5242-9dd0-d2ce-e24e5959a98a.png)

自然数のOrderに最大の数は存在しない等、全てのOrderにターミナルオブジェクトが存在するわけではない。

##### イニシャルオブジェクト
ユニークなOutgoing Arrowを、自身以外の全てのオブジェクトに対して持つ。このような関数は、Haskellではabsurd関数として定義されている。

![initial.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/e129a508-d11c-3224-a3a6-64338dfada4f.png)

###### 定義
1. $\forall a\, \exists f :: Void \to a$
2. $\forall f :: Void \to a, g :: Void \to a \implies f = g$

#### Pathの簡略化
オブジェクトからターミナルオブジェクトへのどのようなPathでも、Compositionを使って、一つのユニークなPathに置き換えることができる。イニシャルオブジェクトからオブジェクトへのPathも同様。

![path-simple.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/bd23f347-0f73-851b-704d-f7f03a780072.png)

#### オブジェクトの比較
カテゴリーの世界では、オブジェクト同士の比較は出来ない、できるのはArrowの比較のみなので、Isomorphismを使う。InvertibleなArrowがIsomorphism。

##### ターミナル・イニシャルオブジェクトとIsomorphism
ターミナル（イニシャルオブジェクト）が複数ある場合、それらをつなぐArrowはユニークでIsomorphicになる。

###### 証明
ターミナルオブジェクトa, bがあるとする。a, bはターミナルオブジェクトなので、a, b自身に向かうユニークなArrow g, fがそれぞれ存在する。

![term1.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/c741078a-a82f-d522-3c8c-f98e1e431198.png)

$a$を始点として、$f$と$g$をコンポーズすると、$a \to a$のArrowができる。あるオブジェクトから$a$に向かうArrowは１つしかなくて、$a$にはid aが存在するので、コンポーズ後のArrowはid aになる。
![term2.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/e1a0f50d-7b73-e3ad-e516-3010f87aaaa4.png)

同様に、$f \circ g = id\;b$になる。

![term3.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/8c83d560-a849-fccb-9696-a2fc9c63a9e7.png)

これはIsomorphismの定義と同じで、fとgはユニークなので、ユニークなIsomorphismになる。

$f \to g = id\;a$
$g \to f = id\;b$

### Universal Construciton
Empty set, singleton setなどを、Setカテゴリーで構築する方法

#### 手順
1. 構築したいものを、オブジェクトとArrowのコンビネーション（パターン）で表す。
2. カテゴリー内で、パターンとマッチする、オブジェクト・Arrowを抽出する。
3. マッチしたもので、比較可能なものをランク付けする。
4. 比較結果で１番になったものを構築結果とする。

#### ターミナル・イニシャルオブジェクトの構築
1. パターンを１つのオブジェクトとする。
2. Partial OrderのOrderとして、オブジェクトとオブジェクトをつなぐユニークなArrowがある場合に、Arrowの終点のオブジェクトは、始点のオブジェクトよりもBetterとしてRankを付ける。ユニークなArrowがない場合には、比較対象にしない。

![unique-better.png](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/499443/eb07405a-bec7-8497-d819-fb7d799ebad9.png)

3. Bestの位置にあるのがターミナルオブジェクトになる。

Arrowの始点のオブジェクトが、終点のオブジェクトよりBetterと定義すると、Bestの位置にイニシャルオブジェクトが来る。

## 動画
Bartosz Milewski / Category Theory 4.1: Terminal and initial objects
https://www.youtube.com/watch?v=zer1aFgj4aU