口頭での説明が不十分だったので、誤解をまねくかも知れない。若干比喩も混じえてテレスコープ構成を説明する。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\hyp}{\text{－} }
\newcommand{\In}{\text{ in }}
\newcommand{\A}[1]{\langle{#1}\rangle } % Angular
`$

• イテレーション
• 混乱ポイント
• 長さ2の具体例
  • イテレーション1：
  • イテレーション2（不完全）
• 代数からの例
  • イテレーション1
  • イテレーション2（完全）

イテレーション

「イテレーションを繰り返す」は日本語として奇妙だが、繰り返す作業の1回分を（ソフトウェア開発の習慣に従い）イテレーションと呼ぶ。イテレーションの通し番号は 1 からにする。

• イテレーション1
• イテレーション2
• イテレーション3
• ‥‥

イテレーション内部での手順をサイクルと呼ぶ。サイクルは堂々巡りでなくて、1イテレーションで1段階の進捗があるので、全体として螺旋状に作業が進行していく。

テレスコープ構成のイテレーション内のサイクルは：

1. 入力（2つの圏）を受け取る。
2. 前層をひとつ作る（あるいは選ぶ）。
3. その前層にグロタンディーク構成を施す。
4. できた圏（ファイブレーションのトータル圏）を成果物とする。

ここでの前層は“広義の前層”で、ターゲット圏は集合圏でなくてもいいし、共変関手でもいい。

イテレーションへの入力は2つの圏であり、イテレーションの出力（成果物）も圏である。入出力も明示してサイクル手順を再度書くと：

1. ソース圏 $`\cat{C}`$ とターゲット圏 $`\mathbb{V}`$ が与えられる。
2. 前層 $`P : \cat{C}^\op \to \mathbb{V}`$ を作る。
3. グロタンディーク構成により、$`\int P`$ を作る。
4. 圏 $`\cat{C'} := \int P`$ を成果物とする。

次のイテレーションでは、圏 $`\cat{C'}`$ が入力となる。それとは別に、ターゲット圏 $`\mathbb{V'}`$ も与えて次のイテレーションを開始する。

上記の（サイクルの）手順がすべて揃ったイテレーションを仮に完全イテレーションと呼ぶことにして、グロタンディーク構成をせずに、前層を成果物とするときは不完全イテレーション。最後のイテレーションだけは不完全イテレーションが許されるが、最後のイテレーションが完全イテレーションでもかまわない。

つまり、テレスコープ構成全体の成果物は、前層でも圏でもOK。型理論では、最後は不完全イテレーション、代数では最後も完全イテレーションが多い。

混乱ポイント

次の二点が混乱の原因になるだろう。

1. すべてのイテレーション（のサイクル内で）、関手圏から対象を選ぶ（関手を作る）操作がある。
2. 最後のイテレーション（第nイテレーション）では、グロタンディーク構成はしなくてもよい。そのときは、関手を成果物とする。

特に n = 2 のとき、第2イテレーションでグロタンディーク構成はしないなら、関手を選んで（作って）終わり。

依存型理論では、シグマ型を繰り返し適用するのは普通なので、任意の長さのテレスコープ前層が自然に出てくるが、組み合わせ幾何の文脈では、「(1)組み合わせ構造の定義 (2)幾何構造や線形代数的構造の付加」の二段階で終わってしまう場合がほとんどのようで、脚注より：

長さ 2 だけなら、テレスコープ前層を持ち出すのはオーバーキルだったかも知れません。

長さ2の具体例

次を仮定する。$`\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
`$

1. $`M \subseteq \mbf{R}`$
2. $`M\ne \emptyset`$
3. $`M`$ は有界
4. $`\alpha\in \mbf{R}`$ は $`M`$ の上界

以上すべての仮定のもとで（使わない仮定もあるが）、以下の2つの命題が同値であることを示す。混乱を避けるために、異なるスコープにある束縛変数は別な名前にしておく。共通する自由変数は $`M, \alpha`$

• [A] $`\forall \beta\in \mbf{R}.\, \beta \lt \alpha \Imp M\cap (\beta, \alpha] \ne \emptyset`$
• [B] $`\forall \gamma\in \mbf{R}.\, \gamma \lt \alpha \Imp M\cap [\gamma, \alpha] \ne \emptyset`$

命題に参照用ラベルを貼りたい場合／参照したい場合は、上記のようにブラケット内にラベルを入れる。

[A] から [B] は容易に示せるから割愛する。[B] から [A] を示す。[B] を前提する。

[A] を示すには、[1] $`\beta \lt \alpha`$ を仮定して、[2] $`M\cap (\beta, \alpha]\ne \emptyset`$ を導けばよい。

仮定 [1] と前提している（暫定的に公理扱いの）命題 [B] から次が言える。

• [3] $`M\cap [\beta, \alpha] \ne \emptyset`$

[3] は、[4] $`\beta \le x \le \alpha`$ である $`x\in M`$ の存在を主張している。$`x`$ は次の2つの場合がありえる。

• [5] $`\beta \lt x \le \alpha`$
• [6] $`\beta = x`$

[5] であれば、そこから結論 [2] が言えるので、オシマイ。[6] $`\beta = x`$ の場合を考える。

もし、[7] $`x \lt x'`$ となる $`x'\in M`$ が取れる（存在する）なら、$`x`$ を $`x'`$ に取り直して [5'] $`\beta \lt x' \le \alpha`$ が言える。その場合は [5'] から結論 [2] が言えるので、オシマイ。

残る場合は、[7] $`x \lt x'`$ となる $`x'\in M`$ が取れない（存在しない）場合。この場合は結論 [2] は言えない。しかし、そんな場合が起こるのか？

今 $`\beta' := (\beta + \alpha)/2 = (x + \alpha)/2`$ と取ると、$`x \lt \beta' \lt \alpha`$ となる。前提して（暫定的に公理扱いして）いる [B] から、[8] $`M\cap [\beta', \alpha] \ne \emptyset`$ となる。これは、[7] $`\beta = x \lt x' \le \alpha`$ となる $`x'\in M`$ が取れる（存在している）ことを意味する。

つまり、$`\beta = x`$ である場合でも、$`x \lt x' \le \alpha`$ となる $`x'\in M`$ を取リ直して、その $`x'`$ に関して $`\beta \lt x' \le \alpha`$ が言える。これで結論 [2] が導けたので [A] が示せた。

結局、上限の定義に閉区間を使うか半開区間を使うかは、定義の論理的内容には影響しない。どちらを使うかは恣意的な選択となる。

述語論理は型理論のなかで展開できる。このとき、通常の（常識的な）論理の概念を型理論的概念に翻訳する。この翻訳に多くの人が戸惑う。$`
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\In}{ \text{ in } }
\newcommand{\incto}{ \hookrightarrow }
`$

まず最初の作業として、真偽値の集合 $`\mbf{Bool} = \{\mrm{true}, \mrm{false}\}`$ を（最下層の）型宇宙 $`\mbf{Type} = |\mbf{Set}|`$ に埋め込む。埋め込み関数を $`\mrm{Emb}`$ とすると：

$`\mrm{Emb} : \mbf{Bool} \to \mbf{Type} \In \mbf{SET}`$
$`\quad \mrm{Emb}(\mrm{true}) := \mbf{1} = \{\top\}`$
$`\quad \mrm{Emb}(\mrm{false}) := \mbf{0} = \emptyset`$

$`\mrm{Emb}`$ を $`\mrm{If}`$ と書いたりする。気にしないのがよいが、気持ち悪いかも知れないから、いちおうの由来を説明する。

$`p`$ を普通の意味の述語、$`f`$ を普通の意味の関数として、else部がないif文を考える。

$`\quad \text{if }p \text{ then }f \text{ end}`$

このif文をひとつの関数だと思うと：

$`\quad \mrm{if}(p, f)`$

引数 $`x\in X`$ を渡すと：

• $`p(x) = \mrm{true}`$ のとき、値は $`f(x)`$
• $`p(x) = \mrm{false}`$ のとき、値はエラー値、仮に便宜上 $`0`$ としておく。（「$`0`$ だと正常値と区別できないことがある」とか余計なことは言わない。）

関数を集合族〈indexed family of sets〉のレベルに引き上げる。

• 集合 $`X`$ 上の関数は $`F:X \to \mbf{Type}`$ だとする。

述語は従来の述語（値が $`\mbf{Bool}`$）だとして $`\mrm{If}(p)\times F`$ を考える。

引数 $`x\in X`$ を渡すと：

• $`p(x) = \mrm{true}`$ のとき、$`\mrm{If}(p(x)) = \mrm{If}(\mrm{true}) = \mbf{1}`$ となり、値は $`\mbf{1}\times F(x)\cong F(x)`$
• $`P(x) = \mrm{false}`$ のとき、$`\mrm{If}(p(x)) = \mrm{If}(\mrm{false}) = \mbf{0}`$ となり、値は $`\mbf{0}\times F(x) = \mbf{0}`$ 、$`\mbf{0}`$ はエラー値とみなす。

述語も集合族〈indexed family of sets〉のレベルに引き上げる。

• 集合 $`X`$ 上の述語は $`P:X \to \{\mbf{1}, \mbf{0}\}\subset \mbf{Type}`$ だとする。

引き上げたif文は次のようになる。

$`\quad \mrm{IF}(P)\times F`$

$`\mrm{IF}`$ は実際は id でダミー。

引数 $`x\in X`$ を渡すと：

• $`P(x) = \mbf{1}`$ のとき、値は $`\mbf{1}\times F(x)\cong F(x)`$
• $`P(x) = \mbf{0}`$ のとき、値は $`\mbf{0}\times F(x) = \mbf{0}`$ 、$`\mbf{0}`$ はエラー値とみなす。

集合族 $`F:X \to \mbf{Type}`$ を“次のレベルの型”とみなす。つまり、types-as-sets から types-as-families に引き上げる。命題（述語）も集合族とみなすなら、引き上げたレベルでは propositions(predicates)-as-types が成立する。

レベルの引き上げはいくらでも出来るので、型宇宙の系列を作れる。型概念はいくらでも高階化できる。

$`\quad \mbf{Type} = \mbf{Type}_0 \incto \mbf{Type}_1 \incto \mbf{Type}_2 \incto \cdots`$

十分高いレベルの型宇宙のなかでは何でもできる。したがって、型理論のなかで何でもできる -- というのが型理論万能主義の原理（あるいは教義）。

---

型システムの型だけを使ってプログラミングが出来ることになる。通常のプログラミング言語の型システムはそこまで強力ではないが、無理すれば出来ないこともない。

• TypeScriptで超絶変態型計算

ブール値や自然数値を、型システムの型として埋め込み、フィボナッチ数列の計算を型システム内でコンパイル時に行う例。

「型の世界のブーリアンと自然数」の最初に出てくる定義が $`\mrm{If}`$ の定義に相当するが、諸般の事情で $`\mrm{true}`$ を空集合に、$`\mrm{false}`$ を単元集合にマップしている。

$`\newcommand{\mbf}[1]{\mathbf{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
`$

小中学校・高校で習った、正比例関数、ベキ関数〈累乗関数〉、指数関数、対数関数は、いずれも群の準同型写像／同型写像である。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
`$

• 群と準同型写像
• 定義の簡略化：練習問題
• 大事な2つの群
• 大事な群準同型写像／群同型写像
  • 正比例関数
  • ベキ関数
  • 指数関数
  • 対数関数
• まとめとやるべきこと

群と準同型写像

一般に、群は次のように書ける。

$`\quad (A, *, e, i)`$

群の構成素は：

1. 台集合 $`A`$
2. 二項演算 $`(*):A\times A \to A`$
3. 単位元（特定の要素） $`e \in A`$
4. 逆元（特定の要素ではなくて写像） $`i: A \to A`$

群の法則〈公理〉は割愛する。

$`(A_1, *_1, e_1, i_1)`$ と $`(A_2, *_2, e_2, i_2)`$ が2つの群のとき、写像 $`f:A_1 \to A_2`$ が群の準同型写像であるとは：

1. 二項演算を保つ $`f(x *_1 y) = f(x) *_2 f(y)`$
2. 単位元を保つ $`f(e_1) = e_2`$
3. 逆元を保つ $`f(i_1(x)) = i_2(f(x))`$

写像 $`f:A_1 \to A_2`$ と $`g:A_2 \to A_1`$ が両方とも群準同型写像であり、次を満たすとき、互いに逆〈mutually inverse〉な群準同型写像という。

1. $`g\circ f = \mrm{id}_{A_1}`$
2. $`f\circ g = \mrm{id}_{A_2}`$

この状況で、以下の言い回しはすべて同じ意味。注意すべきは、単なる写像について語っているのではなくて、群準同型写像について語っていること。括弧内は通常省略されるが、群・群準同型写像について語っていることを明示するなら省略しないほうがよい。

1. $`f`$ と $`g`$ は互いに逆（な群準同型写像）
2. $`f`$ は $`g`$ の逆（群準同型写像）
3. $`g`$ は $`f`$ の逆（群準同型写像）
4. $`f`$ は可逆（群準同型写像）である。（$`g`$ の存在を仮定している。）
5. $`g`$ は可逆（群準同型写像）である。（$`f`$ の存在を仮定している。）

群の準同型写像が可逆であるとき、群の同型写像という。

定義の簡略化：練習問題

• 群の準同型写像の定義で、「逆元を保つ」は不要。二項演算と単位元の保存から出る。練習問題。
• 群の同型写像の定義で、逆写像が群の準同型写像であることは不要。群の準同型写像が逆写像を持つなら、逆写像が準同型写像であることは出る。練習問題。

群の準同型写像 -- 簡略化した定義：

1. 二項演算を保つ $`f(x *_1 y) = f(x) *_2 f(y)`$
2. 単位元を保つ $`f(e_1) = e_2`$

群の同型写像 -- 簡略化した定義：

1. $`f`$ は群の準同型写像である。
2. $`f`$ は逆写像を持つ。（逆写像が準同型写像だとは言ってない。）

大事な2つの群

大事な群その1： 実数加法群

1. 台集合 $`\mbf{R}`$
2. 二項演算 $`(+):\mbf{R}\times \mbf{R} \to \mbf{R}`$
3. 単位元 $`0 \in \mbf{R}`$
4. 逆元 $`(-): \mbf{R} \to \mbf{R}`$ （引き算ではなくて、単項演算のマイナス）

大事な群その2： 正実数乗法群

1. 台集合 $`\mbf{R}_{\gt 0}`$
2. 二項演算 $`(\times):\mbf{R}_{\gt 0}\times \mbf{R}_{\gt 0} \to \mbf{R}_{\gt 0}`$ （演算子記号が省略されることが多い）
3. 単位元 $`1 \in \mbf{R}_{\gt 0}`$
4. 逆元 $`(^{-1}): \mbf{R}_{\gt 0} \to \mbf{R}_{\gt 0}`$

大事な群準同型写像／群同型写像

実数加法群と正実数乗法群のあいだの群準同型写像は小中学校・高校で習う。