まーた、気が変わった、コロリ（気が変わった音）。あっ、いや、米田の補題はやるつもりですよ、ええ。それはいいんですけどね、第8歩の冒頭で「新年の挨拶なんてのは省略。」と書いたのですが、なんか松の内も過ぎて「新年の挨拶」でもしたくなったよ。
まー、圏の定義とかやせた圏（thin category）の補足説明するついでに、圏論（そのコンピューティング・サイエンスへの適用）プロモーションの方針(?)でも述べるべ。
内容：
- 圏の直感的イメージを作る：孤立から連絡へ
- 論理とやせた圏
- 重い圏から軽い圏へ
- 圏もどきと構造付き圏
- まとめ
●圏の直感的イメージを作る：孤立から連絡へ
この「はじめての圏論」シリーズ、気まぐれで米田の補題に向かって舵を切ってしまったのですが、「はじめての」である点を忘れているわけではない（ホントか？）ので、基礎的概念と共に基礎的イメージ（感覚、気分）についても述べましょう。
Aは単なる集合だとして、その元（element; 要素）は“点”とも呼ぶことにします。集合Aは、無関係な点がパラパラと集まっているだけのシロモノです。集団ではあるけれど、メンバー達は孤立しています。
次に、A = |C| であるような圏Cを考えます（圏の用語法／記号法は、前回にまとめてあります）。Cの射は、Aの点と点のあいだを結ぶものです。射は、点どうしの連絡手段、交通路を与えます。2つの点 a, b∈A に注目すると、ホムセットHomC(a, b) = C(a, b)は、aからbに至る連絡手段、交通路をすべて集めた集合です。感覚としては、対象の集合Aが“点の集合”であるのに対して、ホムセットC(a, b)は“線の集合”（矢印の束）です。
Cが離散圏（discrete category）のときは、単なる集合Aと事情が変わらず、点aごとに、自分自身との連絡手段、しかも「私は私である」という自己確認／自己認識である恒等射idaだけしか射がありません。異なる点のあいだに射はなく、やはり、すべての点は孤立しています。
やせた圏（thin category）は、完全孤立に対する救いです。救いではありますが、最低限の連絡手段／交通路しか許されません。つまり、異なる点a, bのあいだには唯1本の射しか許されないのです。自分自身とのあいだにはidaがあるのでこれ以上自己射（endomorphism; a→aの射）は増やせません。もちろん、すべての点どうしが関連しているとは限らないので、a, bのあいだに射がないこともあります。
C(a, b) ≠ 0（0は空集合）、つまり a→b という射が存在することを「aからbに連絡可能である」と解釈すると、圏の基本的性質は：
- 常にaからa（自分自身）に連絡可能である。（idaがある。）
- aからbに連絡可能、bからcに連絡可能なら、aからcに連絡可能である。
さらに圏では、実際の連絡方法が構成可能（constructive）であることも要請します。
- aからaに連絡するidaは、常に前もって特定（distinguish）されている。
- aからbへの連絡手段f、bからcへの連絡手段gが与えられていれば、aからcへの連絡手段であるf;gが具体的・一意的に構成（あるいは特定）できる。
●論理とやせた圏
圏の2つの基本性質は、次の図で表現できます。
（なにもなし）
--------
a→a
a→b b→c
------------
a→c
横の仕切り線の上側が前提で「…があるなら」と読み、下側が結論（帰結）で、「…がある」と読みます。念のため、読み下すと：
- （前提はなしで常に）a→aがある。
- a→b と b→c があるなら、a→c がある。
これらは、論理における基本的な推論法則に対応してます（このへんのことは「論理とはなにか？」を見てください）。圏論の場合は、a→b などの主張（「a ならば（含意） b」と読んでもいいし、前節のように「aからbに連絡可能」と読んでもいいです）に対して、その証拠（witness）として射があるのです。ですから、証拠としての射を添えて、次のように書いたほうが適切でしょう。
（なにもなし）
-----------
id_a:a→a
f:a→b g:b→c
-----------------
f;g:a→c
普通の論理では、いちいち射を書かないで、「射（主張の証拠）があるかないか」だけを問題にします。射（証拠）があれば、その射がどういうものかまでは問いません。それだったら、射の個性を無視していいので、a→b なる射はたかだか1本しかない世界で考えても同じことです。「a→b なる射はたかだか1本の世界」がやせた圏です。
●重い圏から軽い圏へ
ここで話題を変えます。正月の挨拶っぽいハナシ。
僕は、「はじめての圏論」シリーズをしりとりの圏からはじめました。その後も、行列の圏、圏としてのモノイド、やせた圏（プレ順序集合）、とてもやせた圏（順序集合）、変換キュー（バッファ付きフィルター）など、具体的に手で触れるような素材を選んできました。
これには、それなりの意図と理由があります。従来、圏の事例というと、集合と写像の圏、位相空間と連続写像の圏、アーベル群と加法的（線形）写像の圏などが引き合いに出されていました。これらの例を僕は個人的に“重い圏”と呼んでいます。“重い”理由は：
- 予備知識がないと事例を理解できない。つまり、ヘビーな学習を必要とする。
- 圏の対象、射の全体が、普通の意味の集合ではない。ヘビーに巨大な集まりである。
歴史的には、圏論は代数トポロジー（代数的位相幾何学）やホモロジー代数から生まれたので、これらの事例は典型的ともいえます。しかし、物理学やコンピューティング・サイエンスでも圏が常用されつつあるご時世に、初っぱなにこんな重い例を出すのはイカガナモンでしょうか。
それともうひとつ。こういう例から出発すると、「対象≒集合、射≒写像」という先入観が刷り込まれる危険があります。昨今は、「対象≒集合、射≒写像」では理解できない例が頻出します。例えば、プログラムやプロセス（の数理モデル）の圏では、射は写像とは解釈できません。むしろ、射を写像で近似したり表現したりする方法を模索することになります。
そんな事情で、重い圏は（いずれは導入しますが）当面避けて、“軽い圏”を中心に扱おうと思ったわけです。“軽い”とは：
- 比較的少ない予備知識で導入できる。
- 圏の対象、射の全体が、集合となっている。（小さい圏（small category）と呼ぶ。）
特に有限圏（finite category）なら、紙に点と矢印の絵を描いていじれます。軽い圏は、グラフ理論と抽象代数の延長として理解できるので、代数トポロジーやホモロジー代数は不要です（知っていれば有利だが）。
●圏もどきと構造付き圏
正統な（あるいは純粋な）圏の定義だけを採用しても、圏の例はものすごくたくさんあります。しかし、実際的応用を考えると、圏と似てるがわずかに違う“圏もどき”や、圏にさらに別な構造が乗った“構造付き圏”に慣れておくべきだと思います。
例えば、恒等射の存在が保証されない半圏（semicategory）は第6歩で出しています。結合演算が完全には定義できないプレ圏（precategory）とかもあります。
構造付きの圏で一番重要だと思うのは、結合以外の演算（+、×、これらを丸で囲んだ演算記号を使う）を1つ備えたモノイド圏（monoidal category）です。モノイド圏については、「指を使った足し算と interchange law」でわずかに触れています。他に、アミダの圏は、モノイド圏にできます（アミダクジを“横に並べる”操作がもうひとつの演算です）。
圏を絵に描くとき、対象は点、射は線（矢印）にします。射の線は、対象である点と点のあいだを繋ぎます。では、線と線のあいだを繋ぐ面（あるいは膜）のようなものは考えないのでしょうか？ 考えます！ 点（0次元）、線（1次元）、面（2次元）、もっと高次元の構成素を考え、演算も導入します。そうすると、2-圏（2-category）、双圏（bicategory）、二重圏（double category）、一般のn-圏（n-category）などの高次圏（higher (dimensional) category）が出現します。
高次圏論は建設中で、現状では広く合意された“高次圏の定義”もありません。しかし、コンピューティング・サイエンスで登場するオートマトンやラベル付き遷移系の圏などをチャント調べるには、高次圏として取り扱う必要があります。
●まとめ
まとめておきましょう。以下は、僕の個人的な意見と方針ですが：
