From 02485f8a2f36cd30e38d3334b97bfb69177a9803 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 4 Nov 2024 22:50:05 +0900
Subject: [PATCH 1/2] =?UTF-8?q?Functor=20=EF=BC=88=E9=96=A2=E6=89=8B?=
 =?UTF-8?q?=EF=BC=89=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B=20Fixes?=
 =?UTF-8?q?=20#536?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Reference/TypeClass/Functor.lean          | 30 +++++++++++++++++++
 booksrc/SUMMARY.md                            |  1 +
 2 files changed, 31 insertions(+)
 create mode 100644 LeanByExample/Reference/TypeClass/Functor.lean

diff --git a/LeanByExample/Reference/TypeClass/Functor.lean b/LeanByExample/Reference/TypeClass/Functor.lean
new file mode 100644
index 00000000..b20d55c9
--- /dev/null
+++ b/LeanByExample/Reference/TypeClass/Functor.lean
@@ -0,0 +1,30 @@
+/- # Functor
+
+`Functor` は圏論における関手(functor)という概念からその名がある型クラスで、非常に雑な表現をすると、この型クラスを実装した型は「値を包んでいる」ものとして扱うことができます。
+
+より詳細には、`f : Type u → Type v` に対して `Functor` はおおむね次のように定義されています。(実際の定義とは異なります)
+-/
+namespace Hidden --#
+--#--
+/--
+info: class Functor.{u, v} : (Type u → Type v) → Type (max (u + 1) v)
+number of parameters: 1
+constructor:
+Functor.mk : {f : Type u → Type v} →
+  ({α β : Type u} → (α → β) → f α → f β) → ({α β : Type u} → α → f β → f α) → Functor f
+fields:
+map : {α β : Type u} → (α → β) → f α → f β
+mapConst : {α β : Type u} → α → f β → f α
+-/
+#guard_msgs in #print Functor
+--#--
+
+universe u v
+
+/-- 関手 -/
+class Functor (f : Type u → Type v) : Type (max (u+1) v) where
+  /-- 関数 `g : α → β` を `g* : f α → f β` に変換する -/
+  map : {α β : Type u} → (α → β) → f α → f β
+
+end Hidden --#
+/- つまり、`Functor` のインスタンスは `map` メソッドが使用できます。これは型からわかるように、関数を関数に写す高階関数で、「`f` で包まれる前の関数」から「`f` で包まれた関数」を返します。 -/
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index 7d8235bf..c641a7de 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -84,6 +84,7 @@
   - [CoeFun: 関数型への強制](./Reference/TypeClass/CoeFun.md)
   - [CoeSort: 型宇宙への強制](./Reference/TypeClass/CoeSort.md)
   - [Decidable: 決定可能](./Reference/TypeClass/Decidable.md)
+  - [Functor: 関手](./Reference/TypeClass/Functor.md)
   - [GetElem: n番目の要素を取得](./Reference/TypeClass/GetElem.md)
   - [Inhabited: 有項にする](./Reference/TypeClass/Inhabited.md)
   - [OfNat: 数値リテラルを使用](./Reference/TypeClass/OfNat.md)

From a460cbdba721eb3eb4d780965b0a482c280a2aa8 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 5 Nov 2024 00:49:58 +0900
Subject: [PATCH 2/2] =?UTF-8?q?`Functor`=20=E3=81=AE=E4=BE=8B=E3=82=92?=
 =?UTF-8?q?=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Fixes #536
---
 .../Reference/TypeClass/Functor.lean          | 30 +++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/LeanByExample/Reference/TypeClass/Functor.lean b/LeanByExample/Reference/TypeClass/Functor.lean
index b20d55c9..6cf058d2 100644
--- a/LeanByExample/Reference/TypeClass/Functor.lean
+++ b/LeanByExample/Reference/TypeClass/Functor.lean
@@ -28,3 +28,33 @@ class Functor (f : Type u → Type v) : Type (max (u+1) v) where
 
 end Hidden --#
 /- つまり、`Functor` のインスタンスは `map` メソッドが使用できます。これは型からわかるように、関数を関数に写す高階関数で、「`f` で包まれる前の関数」から「`f` で包まれた関数」を返します。 -/
+
+-- `f` は Functor であると仮定
+variable (f : Type → Type) [Functor f]
+
+-- 関数 `g : α → β` と `x : f α` が与えられたとする
+variable {α β : Type} (g : α → β)
+
+-- 高階関数を返す
+#check (Functor.map (f := f) g : f α → f β)
+
+/- `Functor.map` はよく使われる操作であるため、`<$>` という専用の記法が用意されています。-/
+
+example (x : f α) : Functor.map g x = g <$> x := rfl
+
+/- ## 典型的なインスタンス
+
+### List
+`Functor` 型クラスのインスタンスの典型的な例のひとつが `List` です。
+これにより「リストの各要素に関数を適用する」ための簡単な方法が提供されます。
+-/
+
+#guard [1, 2, 3, 4, 5].map (fun x => x * 2) = [2, 4, 6, 8, 10]
+
+/- ### Option
+`Option` も `Functor` 型クラスのインスタンスになっています。
+これにより「`x? : Option` が `some x` の場合に関数を適用し、`none` なら `none` を返す」という操作のための簡単な方法が提供されます。
+-/
+
+#guard (some 2).map (fun x => x * 2) = some 4
+#guard (none : Option Nat).map (fun x => x * 2) = none