## 伴隨函子

``` Hom (L A, B) ≅ Hom (A, R B) ```

``` L A → B ≅ A → R B ```

``` (A × S) → B ≅ A → (S → B) ```

`Set` 中的解釋只是（對我來說較好理解的）特例。各種範疇中，伴隨函子的例子相當多。例如，當考慮的範疇是偏序集合（partially ordered set 或 POSet，以偏序為態射），伴隨函子的意思便是 `L``R` 形成一組 Galois connection.

「同構」意指存在一組函數：`ϕ : Hom (L A, B) → Hom (A, R B)``θ : Hom (A , R B) → Hom (L A, B)`, 滿足 ` ϕ ∘ θ = id`` θ ∘ ϕ = id`，如同前述的 `curry``uncurry`。「自然同構」要求 `ϕ``θ` 對於 `A``B` 必須是自然變換 (natural transformation). 它們的自然轉換性質複雜但重要，我們後面會解釋並用到。

## 單子與餘單子

``` η : A → R (L A) η = ϕ id -- id 的 type 為 L A → L A ε : L (R B) → B ε = θ id -- id 的 type 為 R B → R B ```

``` μ : R (L (R (L A))) → R (L A) μ = R ε -- ε 的 type 中，B := L A δ : L (R B) → L (R (L (R B))) δ = L η -- η 的 type 中，A := R B ```

1. `M id = id`
2. `M f ∘ M g = M (f ∘ g)`
3. `η ∘ f = M f ∘ η`
4. `M f ∘ μ = μ ∘ M (M f)`
5. `μ ∘ η = id = μ ∘ M η`
6. `μ ∘ μ = μ ∘ M μ`

## 態射集合與態射函子

``` F id = id F f ∘ F g = F (f ∘ g) ```

``` Hom : (A₂ → A₁ × B₁ → B₂) → Hom(A₁,B₁) → Hom(A₂, B₂) Hom (f,g) h = g ∘ h ∘ f ```

（此處的型別寫法並不很嚴謹，但希望能幫助理解。）

``` h ∘ F f = G f ∘ h ```

``` ϕ ∘ Hom (L f, g) = Hom (f, R g) ∘ ϕ θ ∘ Hom (f, R g) = Hom (L f, g) ∘ θ ```

``` ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f ```

## 單子規則

3. `η ∘ f = M f ∘ η`:

``` R (L f) ∘ ϕ id = { ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f, [g, h, f := L f, id, id] } ϕ (L f ∘ id ∘ L id) = ϕ (L f) = ϕ (id ∘ id ∘ L f) = { ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f, [g, h := id, id]} ϕ id ∘ f ```

4. `M f ∘ μ = μ ∘ M (M f)`

``` R (θ id) ∘ (R (L (R (L f))) = R (θ id ∘ L (R (L f))) = { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := id, id, R (L f)] } R (θ (R id ∘ id, R (L f))) = R (θ (R (L f))) { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := L f, id, id] } = R (L f ∘ θ id ∘ id) = R (L f) ∘ R (θ id) ```

5.1 `μ ∘ η = id`

``` R (θ id) ∘ ϕ id = { ϕ (g ∘ h ∘ L f) = R g ∘ ϕ h ∘ f, [g, h, f := θ id, id, id] } ϕ (θ id ∘ id ∘ id) = ϕ (θ id) = { ϕ ∘ θ = id } id ```

5.2 `μ ∘ M η = id`

``` R (θ id) ∘ R (L (ϕ id)) = R (θ id ∘ L (ϕ id)) = { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := id, id, ϕ id] } R (θ (R id ∘ id ∘ ϕ id)) = R (θ (ϕ id)) = { θ ∘ ϕ = id } R id = id . ```

6. `μ ∘ μ = μ ∘ M μ`

``` R (θ id) ∘ R (L (R (θ id))) = R (θ id ∘ L (R (θ id))) = { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := id, id, R (θ id)] } R (θ (R id ∘ id ∘ R (θ id))) = R (θ (R (θ id))) = { θ (R g ∘ k ∘ f) = g ∘ θ k ∘ L f, [g, k, f := θ id, id, id]} R (θ id ∘ θ id) = R (θ id) ∘ R (θ id) ```