diff --git a/docs/reference/values-types-variables/mental-model-of-types.md b/docs/reference/values-types-variables/mental-model-of-types.md
new file mode 100644
index 00000000..2f6faa7b
--- /dev/null
+++ b/docs/reference/values-types-variables/mental-model-of-types.md
@@ -0,0 +1,232 @@
+---
+sidebar_label: 型のメンタルモデル
+---
+
+# 型のメンタルモデル
+
+## 型システムの背景理論
+
+プログラミング言語の型システムにはそれぞれ固有の世界観があり、言語ごとに型の機能が異なります。
+
+その一方で複数の言語で共通している機能もあり、それらのさまざまな型の機能は唐突にどこからともなく出現してきたわけではありません。背景として大きくは**型理論**(type theory)と呼ばれる数学的な研究分野があり、各言語の型システムは型理論に基づいて実装されています。
+
+たとえば、TypeScriptの`unknown`型や`never`型のような一見何のためにあるか分からないような型であっても、型理論においてはその役割や機能を一般的に説明することができます。これらの型はトップ型やボトム型と呼ばれる型の種類に分類され、部分型関係が作る階層構造の両端点に位置する型として振る舞います。
+
+部分型階層の両端点に位置する型
+
+
+
+型理論的な観点からの知識を持つことで似たような型システムを持つ他の言語においても型の機能について自然に推論することが可能になります。たとえばScalaというプログラミング言語では`Nothing`と呼ばれる型が型階層のボトムに位置することから`never`型と同じ働きをすることが推論できます。このように型について一般化された知識を使うことで、ログラミング言語をスイッチするような場合でもスムーズに機能の類推や学習を行うことができるようになります。
+
+型理論は非常に奥深く難解な分野でもありますが、その一方で比較的簡単に理解できて実用的にも役立つ概念も非常に多くあります。このドキュメントではそういった知識からTypeScriptの型の世界観、いわば**メンタルモデル**を構築するための知識の一部を紹介します。
+
+:::info より深く学ぶには
+この章の内容を読んでみて型システムや型理論について興味が湧いたら、著名な入門書である『[型システム入門 プログラミング言語と型の理論](https://www.ohmsha.co.jp/book/9784274069116/)』の単純型や部分型付けの章などを読んでみることをオススメします。
+
+論理学的な知識があると推論規則などが比較的読みやすくなるので、東京大学出版会から出版されている『[論理学](https://www.utp.or.jp/book/b298898.html)』などの書籍を合わせて読むとよいかもしれません。また、型システム入門の読み方としては定理を隅々検証して読むというよりかは、知識や概念を入手する目的で面白そうなところを拾って読んでいくと意外と読みやすくなるのでぜひ挑戦してみてください。
+:::
+
+## 集合論的なデザイン
+
+型のメンタルモデル、つまり「型をどのように解釈するか」を考える上で非常に有用でありなが身近な数学的なツールがあります。それが集合論(set thoery)であり、この章では「型=集合」として考えることにします。
+
+一般に型(type)は集合(set)は異なる概念ですが、型理論と集合論の間には[密接な関連](https://ja.wikipedia.org/wiki/%E3%83%A9%E3%83%83%E3%82%BB%E3%83%AB%E3%81%AE%E3%83%91%E3%83%A9%E3%83%89%E3%83%83%E3%82%AF%E3%82%B9)があります。
+
+特にTypeScriptにおいては、型を集合論的に扱えるようなデザインが意図的になされており、型を「**値の集合**」として捉えることで直感的に型を理解することができるようになっています。この見方は決して偏ったものではなく、[公式ドキュメント](https://www.typescriptlang.org/docs/handbook/typescript-in-5-minutes-oop.html#types-as-sets)でも推奨されている型の考え方です。
+
+本章ではこのような集合論的な見方に立って型を考えることで、型の振る舞いについての自然な推論を行えるようなメンタルモデルを構築します。
+
+## 和集合と共通部分
+
+型を集合論的に扱えるお陰で、TypeScriptの型は集合が持つような演算の一部を利用することができます。
+
+集合の演算は集合から新しい集合を作り出すような操作であり、そのような演算にはいくつも種類があります。TypeScriptではそのような演算の中で和集合と共通部分を演算に相当する[ユニオン型](./union.md)と[インターセクション型](./intersection.md)が備わっています。
+
+```ts twoslash twoslash
+type A = { a: string };
+type B = { b: number };
+
+// AとBの和集合を表現する型
+type Union = A | B;
+
+// AとBの共通部分を表現する型
+type Intersection = A & B;
+```
+
+和集合と共通部分に相当する型表現
+
+
+
+直感的にはユニオン型はふたつの集合の和集合を表現する型であり、インターセクション型はふたつの型の共通部分を表現する型です。ユニオン型は特に型の絞り込み(narrowing)において特に重要な役割を果たし、型の和集合から選択的に型の候補を削っていくことができます。
+
+```ts twoslash title="型の絞り込みは和集合から集合を削っていく"
+type StrOrNum = string | number;
+
+function narrowUnion(param: StrOrNum) {
+ if (typeof param === "string") {
+ // stringとnumberの和集合からstringを削る
+ console.log(param.toUpperCase());
+ } else {
+ // 残された集合はnumber
+ console.log(param * 3);
+ }
+}
+```
+
+このふたつの型は複数の型から新しい型を合成できるという点で演算として重要ですが、特定の型そのものが集合としてどのように解釈できるかを次に紹介する３つの型で解説していきます。
+
+## ユニット型
+
+ここからは、TypeScriptにおいて型は値の集合として扱えることができることを具体例を交えて説明していきます。
+
+まずは単に型を「値の集合」であると考えてください。たとえば、`number`型という数値を表す型ですが、この型が集合であるとすると、その要素は具体的な`number`型の値である数値です。たとえば`1`や`3.14`などの数値がこの集合の要素となります。[number型](../values-types-variables/number/README.md)のページで述べているようにnumber型で表現可能な範囲は有限であり、それらの範囲の要素に`NaN`と`Infinity`などの特殊な定数を加えた集合が`number`型の集合ということになります。
+
+さて、重要な型の概念として**ユニット型**(unit type)という型の種類があります。ユニット型とは文字通りの単位的な型であり、型の要素として値をひとつしか持たないような型です。集合論においては単一の要素からなる集合は単位集合(unit set)や単集合(singleton set)など呼ばれます。
+
+型の世界での単位集合に相当するものがユニット型であり、たとえば、PHPでは`null`という単一の値を持つ`null`型がユニット型に相当し、KotlinやScalaでは分かりやすく`Unit`型という名前の型がユニット型です。
+
+TypeScriptでは`null`という単一の値を持つ`null`型と、`undefined`という単一の値を持つ`undefined`型がユニット型に相当します。
+
+```ts twoslash title="nullとundefinedはユニット型"
+type N = null;
+const n: N = null;
+
+type U = undefined;
+const u: U = undefined;
+```
+
+他にもTypeScriptには[リテラル型](../values-types-variables/literal-types.md)という型がありましたが、このリテラル型もユニット型に相当します。
+
+```ts twoslash title="リテラル型はユニット型"
+type Unit = 1;
+const one: Unit = 1;
+```
+
+リテラル型は値リテラルをそのまま型として表現できる型であり、`number`や`string`などのプリミティブ型にはそれぞれ具体的な値のリテラルによって作成されるリテラル型が存在します。
+
+- 文字列リテラル型 : `"st"`, `"@"`, ...
+- 数値リテラル型 : `1`, `3.14`, `-2`, ...
+- 真偽値リテラル型 : `ture`, `false` のふたつのみ
+
+型は値の集合でしたが、具体的な値はそのリテラル型と一対一で対応します。
+
+集合の要素の個数は「濃度(cardinality)」と呼ばれる概念によって一般化され、基数という数によって表記されます。たとえば、要素がひとつしかない単位集合の濃度は１です。つまり、型を集合としてみなしたときのユニット型の濃度は１ということになります。
+
+それでは濃度が２、つまり要素の個数が二個からなるシンプルな型について考えてみましょう。たとえば、真偽値を表す `boolean` という型の要素(値)は`true`と`false`のみであり、`boolean`型の変数にはそれら以外の値を割り当てることはできません。したがって`boolean`型は濃度2の集合としてみなせます。
+
+```ts twoslash
+const b1: boolean = true;
+const b2: boolean = false;
+// @errors: 2322
+const b3: boolean = 1;
+```
+
+リテラル型について思い出すと真偽値についてもそれぞれリテラル型`true`と`false`が存在しました。これらの型はそれぞれがひとつの値だけを持つユニット型でした。
+
+リテラル型は具体的な値と一対一の他対応となります。型の集まりには集合演算が備わっていたので、リテラル型を要素として新しい集合を作ってみると考えてもよいでしょう。ふたつの単集合`true`と`false`を合成してふたつの型(あるいは値)から和集合を作成すると濃度2の型を得ることができます。
+
+```ts twoslash title="true と false の和集合"
+type Bool = true | false;
+```
+
+このようにユニオン型で合成した型`Bool`は`boolean`型と同一の型となります。
+
+## ボトム型
+
+ユニット型は値をひとつしか持たない型ですが、値をまったく持たないような型も存在しています。そのような型を**ボトム型**(bottom type)と呼びます。型が集合であるとするとき、ボトム型は空集合(empty set)に相当し、空型(empty type)とも呼ばれることがあります。
+
+ボトム型は値をまったく持たない型として、例外が発生する関数の返り値の型として利用されますが、TypeScriptでのボトム型は部分型階層の一番下、つまりボトムの位置に存在している`never`型となります。
+
+```ts twoslash
+function neverReturn(): never {
+ throw new Error("決して返ってこない関数");
+}
+```
+
+`never`型は集合としては空集合であり、値をひとつも持たないため、その型の変数にはどのような要素も割り当てることができません。
+
+```ts twoslash
+// @errors: 1206 2322
+const n: never = 42;
+```
+
+## トップ型
+
+ボトム型が値をまったく持たない型なら、それとは逆にすべての値を持つような型も存在しています。そのような型を**トップ型**(top type)と呼びます。
+
+トップ型はすべての値を持っており、その型の変数にはあらゆる値を割り当てることができます。オブジェクト指向言語であれば大抵は型階層のルート位置、つまりトップ位置に存在している型であり、TypeScriptでは`unknown`型がトップ型に相当します。
+
+```ts twoslash
+const u1: unknown = 42;
+const u2: unknown = "st";
+const u3: unknown = { p: 1 };
+const u4: unknown = null;
+const u5: unknown = () => 2;
+```
+
+ボトム型が空集合に相当するなら、トップ型は全体集合に相当すると言えるでしょう。なおTypeScriptでは`{} | null | undefind`という特殊なユニオン型を`unknown`型相当として扱い、相互に割当可能としています。
+
+```ts twoslash twoslash title="unknown型相当の特殊なユニオン型"
+declare const u: unknown;
+const t: {} | null | undefined = u;
+```
+
+`{}`はプロパティを持たないオブジェクトを表現する空のobject型であり、この型はあらゆるオブジェクトの型と`null`と`undefined`を除くすべてのプリミティブ型を包含しています。したがって、`unknown`という全体集合は上記のような３つの集合に分割できると考えることもできます。
+
+TypeScriptには`unknwon`型以外にもうひとつ特殊なトップ型があります。それが`any`型です。`any`型には`unknown`型と同様にあらゆる型の値を割当可能です。
+
+```ts twoslash
+const a1: any = 42;
+const a2: any = "st";
+const a3: any = { p: 1 };
+const a4: any = null;
+const a5: any = () => 2;
+```
+
+`any`型の特殊性はトップ型としてあらゆる型からの割当が可能だけでなく、`never`型を除くあらゆる型へも割当可能な点です。
+
+```ts twoslash
+declare const a: any;
+
+const n1: unknown = a;
+const n2: {} = a;
+const n3: number = a;
+const n4: 1 = a;
+// @errors: 2322
+const n5: never = a;
+```
+
+`any`型は`never`型を除けばあらゆる型へも割当可能なため一見するとボトム型のように振る舞っているように見えますが、実際にはボトム型ではありません。
+
+TypeScriptは元来、JavaScriptに対して**オプショナルに型付けを行う**という言語であり、型注釈を省略して型推論ができない場合には未知の型を暗黙的に`any`型として推論します。このような状況において`any`型はあらゆる型からの割当が可能であるだけでなく、あらゆる型への割当が可能であることが必要であり、それによって型注釈がないJavaScriptに対して漸進的に型を付けていくことが可能になります。
+
+実は`any`型は`unknown`型がTypeScriptに導入されるまで唯一のトップ型として機能していましたが、純粋にあらゆる型の上位型になる部分型関係のトップ位置の型として機能する`unknown`型が導入されたことで部分型関係の概念が明瞭になりました。
+
+## 部分型関係の解釈
+
+部分型関係とはそもそも「型Aが型Bの部分型であるとき、Bの型の値が求められる際にAの型の値を指定できる」という型同士の互換性に関わる関係です。関数型を除く通常の型については、ここまで見てきた通り型を集合として解釈すれば部分型関係は**集合の包含関係**に相当します。
+
+[部分型関係の説明](./structural-subtyping.md)において、型と型の関係性は**階層構造**で捉えることができると述べましたが、集合の包含関係は階層構造について少し見方を変えた構造であると言えます。
+
+集合的と見方と階層的な見方
+
+
+
+トップ型である`unknown`型はあらゆる型の基本型、つまり上位型として振る舞い、あらゆる型は`unknown`型の部分型となります。したがって、型を集合として解釈したとき、`unknown`型はTypeScriptにおけるあらゆる値を含む集合となります。つまり全体集合であり、あらゆる型は`unknown`型の部分集合とみなすことができます。
+
+それとは逆に、ボトム型である`never`型はあらゆる型の部分型となります。したがって、型を集合として解釈したとき、`never`型はTypeScriptにおけるどのような値も含まない集合、つまり空集合としてみなすことができます。
+
+このように部分型関係を集合の包含関係として捉えることで、より直感的に型の互換性についての推論が可能となります。
+
+たとえばふたつの集合の和集合はその共通部分を包含します。ユニオン型とインターセクション型は和集合と共通部分に相当していたので、包含関係からインターセクション型がユニオン型の部分型となることが推論されます。実際に検証してみると、ユニオン型の変数にインターセクション型の変数を割りあてることが可能です。
+
+```ts twoslash
+type A = { a: string };
+type B = { b: number };
+
+type Union = A | B;
+type Intersection = A & B;
+
+const a_and_b: Intersection = { a: "st", b: 42 };
+const a_or_b: Union = a_and_b;
+```
diff --git a/sidebars.js b/sidebars.js
index 4263a2a0..9e971c2c 100644
--- a/sidebars.js
+++ b/sidebars.js
@@ -171,6 +171,7 @@ module.exports = {
"reference/values-types-variables/typeof-operator",
"reference/values-types-variables/equality",
"reference/values-types-variables/truthy-falsy-values",
+ "reference/values-types-variables/mental-model-of-types",
],
},
{
diff --git a/static/reference/values-types-variables/mental-model-of-types/2way-views-types.svg b/static/reference/values-types-variables/mental-model-of-types/2way-views-types.svg
new file mode 100644
index 00000000..307f4087
--- /dev/null
+++ b/static/reference/values-types-variables/mental-model-of-types/2way-views-types.svg
@@ -0,0 +1,40 @@
+
diff --git a/static/reference/values-types-variables/mental-model-of-types/subtyping-end-points.svg b/static/reference/values-types-variables/mental-model-of-types/subtyping-end-points.svg
new file mode 100644
index 00000000..8bcfcd0d
--- /dev/null
+++ b/static/reference/values-types-variables/mental-model-of-types/subtyping-end-points.svg
@@ -0,0 +1,42 @@
+
diff --git a/static/reference/values-types-variables/mental-model-of-types/union-intersection-inclusion.svg b/static/reference/values-types-variables/mental-model-of-types/union-intersection-inclusion.svg
new file mode 100644
index 00000000..9c8e1392
--- /dev/null
+++ b/static/reference/values-types-variables/mental-model-of-types/union-intersection-inclusion.svg
@@ -0,0 +1,24 @@
+