monadからeffectへ

追記 もう少しまともなeffect入門記事を書きました

myuon-myon.hatenablog.com

この文章は今から5-10年後に万が一effect systemが流行り始め、今のHaskellのような立ち位置になった場合に備えて書いています。

---

effect systemについて

Haskellはモナドを用いて純粋・非純粋を切り分けることができる言語で、computational effectを扱うために導入されたものだった。

かつては関数 A -> B で一緒くたにしていたcomputationは、 A -> T B と、文脈 T をもった関数として表現できるようになった。ところでこのようなcomputational effectとしてのモナドを言語機能に組み込むには2つの方法があって、

• Meta Language方式 (Haskell)
• Programming Language方式 (MLなど)

(ここでは便宜上MetaLanguageとProgrammingLanguageと呼んでいて混乱しやすい名前なことは重々承知しているのだけれど他になんと呼べばいいのかわからないのでとりあえずこうしておく。MLはProgrammingLanguage方式なので注意)

前者はそのままモナドを言語の中に組み込む方法で、Haskellのようにユーザーがモナドを直接操作することになる。一方後者はKleisli categoryで考えましょうという方式で、言語に対して1つの巨大な(IO)モナド T を固定しておいて、 A -> B とプログラム言語の中でかいたら A -> T B だと解釈されるというもの。

さて、Haskellはモナドを直接ユーザーに見せることで、複数のモナドを切り替えてプログラムがかけるようにしたのだけれど、このせいで通常の関数とモナド付きの関数では互換性がなくなってしまった。

例えば 1 + 2 はよいけれど、 return 1 + return 2 は許されない。

さて、effect systemはいわば添字付きのモナドであり、プログラム A -> B を文脈 T とそこでのエフェクト e があって A -> Te B として表現するものである。effect systemも上に述べたようにそのモナドをユーザーに見せるかどうかを区別することが出来る。

表にまとめてみよう:

-	Programming Language	Meta Language
ベースの言語	`A -> B`	`A -> B`
monad system	`A -> B`	`A -> T B` …(2)
effect system	`A -> {e}B` …(3)	`A -> Te B` …(4)

effect systemを使うと同じモナドに対してどういう操作が起こる可能性があるかを調べることができる。詳しい話は省くけれど(2)から(3)に移ることは自然に出来て、effect systemは詳細に「起こりうる副作用」を分類することができる。

さて、(3)はProgramming Language方式なので実際にユーザーがモナドを意識する必要はないし、なによりpure functionとの互換性があるのが嬉しい。a : {e}Int と b : {e'}Int にたいして自然に a+b : {e | e'}Int などとできる。(これは厳密にはeffectの扱い方による)

おそらくHaskellよりももっと自然に副作用の分離ができるようになるはず。

ところで、(4)の用にエフェクトもモナドも記述するという方法があって、果たしてこれがどういうパラダイムになり、何ができるようになるのかは今の自分にはあまり想像できない。(便利なことがあるのだろうか？)

実装について

いくつか実装はあるけれど、例えばHaskellによく似たsyntaxを採用している Frank というのがある。この言語では A -> [e]B とかくと自然に forall eff. A -> {eff + e}B と解釈されてpolymorphic effectの計算が行われる。

少なくともよくあるeffect systemの定義ではcoerce rule(e < e' ~> {e}A -> {e'}A みたいなやつ)を入れずにこれを自然に計算する仕組みを考えてあって、個人的にはcoerce ruleをユーザーが手動で挿入するのはアホらしいのでこれがいいと思う。なので、そういうことをしようとすると既存のHaskellみたいな言語にそのまま組み込むわけには行かないので、個人的にはそろそろHaskell捨てたいな〜〜って言っている。

よい実装とライブラリがちゃんと揃ってくれないとどうしようもないのだけれど、いずれHaskellが捨てられる日がくるのだろうか。

はてさて

ゲームを作る機運が高まってきた

個人のゲーム制作といえばRPGがなんとなく花形感がありますが(多分ツクールのせいや)
じゃあ作ろうって思って完成まで行くのは結構大変ですよねみたいな

以下言い訳が並びます

グラフィック

多分一番問題になるのはここで、スキルはないが人間はいる(人間を雇うお金がある)なら
最近のコンシューマーゲームに倣って3D一択なんだろうけど
残念ながら個人制作で3Dを採用するのは敷居が高すぎるわけです

というわけでRPG素材をググることになるわけですが
するとジャンルやらストーリーに大幅に制限がかかります
(素材として配布されているようなものはジャンルが結構偏ってる)

というわけでグラフィックでジャンルとかキャラクターが決められてしまうというのは
もったいないことではあります

ただしドット絵を素人が描くのはかなり厳しいので
困ったねぇみたいな

フレームワーク的な

これに関してはツクールその他の開発環境を選べば全く問題がないのだけれど
プログラミングするマン的にはエンジンもどうせなら自作したいという邪悪な心が芽生えて
めでたくエターナるわけです(素直にツクール使え)

ただしエンジン自作のメリットとして
例えばブラウザで動かしたいみたいな欲求にも比較的答えやすいというのがあり
今時PCでダウンロードしてフリーゲームを遊ぶ人はかなり減ってることを思えば
そういう手もあるにはある(完成しない可能性も飛躍的に上がるけど)

音楽

音楽は多分問題がなくて山ほど素材があるし
多少のお金が出せるのならばそれはそれは素晴らしい音楽を作ってくれる人はネットに意外といるので
ここが問題になることはあんまりないと思う

ただ素材の選定がめんどくさいことこの上ない
欲しいBGM素材を探す行為ほど時間が削られることもない

ストーリー・演出

いや面白いストーリーが思いつかないならゲームなんて作らないでしょって感じなので
ストーリーは多分みんなそれなりにちゃんと考えるのだろうけれど
それがプレイヤーに伝わるレベルで細かく演出やらなんやらを入れるのは実はかなり大変なので
結果としてそこで妥協してしまい、
その流れでストーリーも予定より縮小されかねない

まぁ最初から大きすぎるものを作ろうとするのをやめよう、という話ではある

終わりに

以上がゲーム作りたい作りたいって言いながら結局何もしない人間の言い訳集なんだけど
本当に作りたい人は例えば以下のような心得的なものをちゃんと頭に入れて
真面目にプロジェクトマネジメントをするべきなんだろう

シルバーセカンド開発日誌 ゲームを完成させる作り方

個人制作ゲームが空中分解しやすいのは、十中八九「プロジェクトマネジメントができてない」なので
そこさえできれば技術もなにもなくても完成まではこぎつけられるんじゃないかな

さてゲーム作る機運が高まってきたのだけれど
自分はどうしたらいいのかな

美少女と学ぶ圏論(2)

本来ならば図式を交えて説明するべきところを図式を用意していないので非常に分かりにくいです(特に証明の部分など). 自分で可換図式を書きながら議論を追って読まれることをおすすめします.

1.2 SpecialなObjectたち

　レポートをやるというのは話を切り上げるための口実で, 実際ほとんどできていたので仕上げには全然時間がかかなかった.
　ゼミのために買ったホモロジー代数の本をパラパラめくっていると, 導来関手という文字が度々目に入った. そういえば, 千景に渡されたpdfには"関手と自然変換"というセクションがあった. 僕はカバンから紙の束を取り出して机にのせる.
　1.1は圏の定義と例で, 今日話したようなことが載っているだけだった. 1.2に進もう.

Definition 射\(f : A \to B \)に対し射\(g : B \to A \)が存在して\(f \circ g =1_B, g \circ f = 1_A\)を満たす時, \(f\)を同型射(isomorphism)という. またこのとき\(A,B\)は同型ともいう.

　同型はよく見る定義だ. 写像が全単射であることと写像が上の意味で同型であることは同値だから, 上の定義は理解しやすくて良い.
　ただ, 全単射の定義とは違ってdomainやcodomainの元がどうなるかについては触れていない. これが千景の言っていた"元の取れない圏論"なのだろうか. 確かに元に触れずに同型射を定義しているので, なんとなく抽象的な感じはする.

Definition 射\(f : A \to B \)がepimorphism(epi)であるとは, 任意の\(g \circ f = h \circ f \)を満たす射\(g,h : B \to C \)に対して\(g = h\)が成り立つ.
　このとき\(f : A \twoheadrightarrow B \)とかく.
Definition 射\(f : A \to B \)がmonomorphism(mono, monic)であるとは, 任意の\(f \circ g = f \circ h \)を満たす射\(g,h : C \to A \)に対して\(g = h\)が成り立つ.
　このとき\(f : A \rightarrowtail B \)とかく.

　epimorphismとmonomorphismはどうやら逆の概念であるらしい. そう, よく見れば上の定義にある\(f,g,h\)の射の"向きを反転"させれば下の定義に一致する. これが千景の言っていた双対に違いない.
　ネットによると, それぞれの射にはエピ射, モノ射という訳が当てられるらしい.　千景は, 双対には"余"という漢字が当てられると言っていたが必ずしもそういうわけでもないのか.

　ところでepiやmonoが何を表しているかをもうちょっとよく考えよう.
　分かりやすいところで写像, つまりSet圏を考えることにする. \(f\)がepiなら, \(g(f(x)) = h(f(x)) \;\; (\forall x \in A)\)のとき\(g = h\)が言える. \(g,h\)が\(Im f\)上で一致するなら\(B\)上全体で一致するということで, これが成り立つということは\(f\)が全射ということに違いない.
　同じく, \(f\)がmonoなら, \(f(g(x)) = f(h(x)) \;\; (x \in C)\)のとき\(g = h\)だから\(f\)は単射になる.
　なるほど, どうやらepiとmonoは全射, 単射に対応するらしい.

　僕は手を止めて紅茶を一口飲んだ. ハーブティーは心を落ち着けてくれる. 温かい紅茶が心に染み入るように, epiとmonoの定義は僕の脳内に染みこんでくるようだ.
　ここに千景がいたら, きっとこんな風に語りかけてくるだろう.
『さぁ, 次はisoについても考えてみよう. 集合では全射かつ単射と同型は同値. ではepiかつmonoとisoは同値？』
　そんな僕の考えを予想しているかのように, 次のページには千景が書いたと思われる走り書きがしてあった.

　isoならばmonoかつepi. しかし逆は成り立たない. 反例は？

　isoならばmonoかつepiは定義から明らかだ. さて, 反例は….

---

「それで？ 反例は見つかったの？」
　午後. 僕はまた, 千景と教室の黒板前にいた. 学部生控室というのは便利なもので, 自由に使える黒板や椅子や机がある. こんなに素晴らしい環境の割には人も少ない.
　僕は昨日考えたことを千景に話すことにした. 人に説明すると, 頭の中も整理される.
「意外なところにあったよ. 群とか加群じゃ見つからなかった」

Counterexample \(X\)を2点以上の位相空間とする. さらに\(X_i\)は\(X\)に密着位相を入れたもの, \(X_d\)は\(X\)に離散位相を入れたものとする.
　集合として恒等写像である連続写像\(id : X_d \to X_i; \; x \mapsto x \)は全単射で, 位相空間の圏の射としてepiかつmono. しかしこの逆写像は連続でないから, 位相空間の圏の射にはならない. よって\(id\)は位相空間の圏の中でepiかつmonoだがisoではない.

「よく出来ました. 言ってなかったけど, isoとepiかつmonoが同値になる圏をbalancedという」
「ふむ？」
「一般にAbel圏はbalancedなんだ. だからAbel群や加群では同値になるよ」
「うん, それに気がついてから, 位相空間の圏で探してみたら見つかった」
「他に何か気がついたことはある？」
「そうだな…. posetを圏とみなす, というのをやったよね. この圏では全ての射はepiかつmonoで, isoな対象は等しいことが反対称律から分かる, とか」
「そうだね. それもepiかつmonoだがisoでないような例の一つね」
「あまり面白い反例とは言えないかもしれないけどね」
　千景は満足そうにニヤついて, 僕を見た.
「さて, 先に進もう. 1.2くらいは読んできた？」
「う, うん. でも, 関手と自然変換まではたどり着かなかったよ」
「いや, 別にいいよ. 昨日のアレは言ってみただけ」
　千景は僕にチョークを渡して, 一番前の席についた. 先生ではなく生徒として聞き手に回る, という意思表示. 渡されたチョークはほとんど使ってなくて, 先がほんの少しだけ欠けていた.
「1.2の残りでは圏の特別な対象を定義して, それらの例を見るって感じだね. まずはproduct」

Definition

\(A \xleftarrow{p_A} P \xrightarrow{p_B} B \)が直積(積, product)の図式である, または対象\(P\)がproductであるとは, 以下を満たすことである.

• (UMP) 任意の\(A \xleftarrow{f} Z \xrightarrow{g} B\)なる図式に対し, \(p_A \circ h = f\)かつ\(p_B \circ h = g\)を満たす\(h : Z \to P \)が一意的に存在する. \(f,g\)から定まる射\(h\)のことを, \(h = \langle f,g \rangle\)と書く.

「ここでいう"一意的に存在する"というのは, 存在して, かつ一意的であるってことね. 条件として2つあるってことに注意してね」
「オッケー. じゃあ双対のcoproductも一緒に定義を述べるよ」

Definition

\(A \xrightarrow{i_A} Q \xleftarrow{i_B} B \)が直和(余積, coproduct)の図式である, または対象\(Q\)がcoproductであるとは, 以下を満たすことである.

• (UMP) 任意の\(A \xrightarrow{f} Z \xleftarrow{g} B\)なる図式に対し, \(h \circ i_A = f\)かつ\(h \circ i_B = g\)を満たす\(h : Q \to Z \)が一意的に存在する.

「定義はこれだけなんだけど……UMPってなんのことかな？この条件の名前？」
「うん, UMPの説明は特にしてなかったね. UMPはUniversal Mapping Propertyの略で, 簡単に言えば"ある射が一意的に存在する"っていう性質のこと」
「〜の条件を満たす\(h\)が一意的に存在する, って条件のことだね」
「そう. universalityと言ったりもする. productのuniversalityと言えば, 上の条件のことだと思って」
「了解. じゃあもう少し例を続けるよ」

Definition

対象\(0\)が始対象(initial object)とは, 以下を満たすことである.

• (UMP) 任意の対象\(X\)に対して\(0 \to X \)なる射が一意的に存在する

対象\(1\)が終対象(terminal object)とは, 以下を満たすことである.

• (UMP) 任意の対象\(X\)に対して\(X \to 1 \)なる射が一意的に存在する

「例は挙げられる？」
「うん」
　昨日ノートにまとめたことを, 黒板に書いていく.

圏	initial object	terminal object	product	coproduct
\(\mathbf{Set}\)	空集合 \(\emptyset\)	1点集合\(\{* \}\)	直積	直和(disjoint union)
\(\mathbf{Top}\)	\((\emptyset, \{\emptyset\})\)	\((\{* \}, \{\emptyset, \{* \}\})\)	直積空間	直和
\(\mathrm{R}-\mathbf{Mod}\)	1点加群 \(\{0\}\)	1点群 \(\{0\}\)	直積	直和(=直積)
poset \(P\)	\(P\)の最小元	\(P\)の最大元	sup(最小上界)	inf(最大下界)

「注意としては, 一般に加群の直積と直和は一致しないけど, 今定義した直積と直和が有限(二項)直積/直和しか定義していないからだね. そういえば, 今の定義じゃ二項直積/直和しかないけど, 一般の直積や直和も定義できるのかな…？」
「もちろん. 一般の集合\(I\)上の直積も定義できるよ」

Definition

\(P \xrightarrow{p_i} X_i \; (i \in I)\)または\(P\)が直積とは, 以下の満たすことである.

• (UMP) 任意の\(Z \xrightarrow{f_i} X_i\)なる図式に対し, \(p_i \circ h = f_i \;\; (i \in I)\)を満たす\(h : Z \to P \)が一意的に存在する.

「表をみていて気がついたことはある？」
「terminal objectとinitial objectが一致する圏があるね. 加群の圏とか, Abel群の圏がそうだね」
「terminal objectとinitial objectが一致する時, それをzero objectという. Abel圏にはzero objectをもつことが要請される」
「確か…加群の圏とかAbel群の圏がAbel圏だったね」
「あとはベクトル空間の圏もね」
「他には, posetではterminal objectが最大元でproductがsupになるんだね」
「posetは例として分かりやすくていいよね. うん, 私も好きだよ」
「じゃあ次に進むよ…って言っても, 次はあんまりピッタリ来る例がないんだけど」
「equalizerとpullbackね. こちらは定義だけやろう, とりあえず後で出てくるまで覚えておいてくれればいいよ」

Definition

平行射\(f,g : A \rightrightarrows B \)に対し, \(e : E \to A \)が\(f,g\)のequalizerであるとは, 以下を満たすことである.

• (図式の可換性) \(f \circ e = g \circ e \).
  
• (UMP) 任意の\(z : Z \to A \)で\(f \circ z = g \circ z \)を満たすものに対し, \(z = e \circ h \)を満たす\(h : Z \to E \)が一意的に存在する.

Definition

\(A \xleftarrow{q_A} P \xrightarrow{q_B} B \)が図式\(A \xrightarrow{p_A} C \xleftarrow{p_B} B \)のpullbackとは, 以下を満たすことである.

• (図式の可換性) \(p_A \circ q_A = p_B \circ q_B \).
  
• (UMP) 任意の\(z_A : Z \to A, z_B: Z \to B \)で\(p_A \circ z_A = p_B \circ z_B\)を満たすものに対し, \(q_A \circ h = f, q_B \circ h = g\)を満たす\(h : Z \to P \)が一意的に存在する.

「coequalizer, pushoutがequalizer, pullbackの双対概念として定義されるよ」
「これらの概念に関していくつか性質を確認しておこう」
「うん」
「じゃあ, 次のことを証明して」

Prop terminal object, initial object, product, coproduct, equalizer, coequalizer, pullback, pushoutは同型を除いて一意的である

「同型を除いて一意的」
「つまり, 2つあったとすると同型になるってことね. 同型を同一視すると存在は一意的ということ. もちろん一般の圏がこれらを持つとは限らないけどね」
「とりあえずterminal objectの一意性をやろうか」

証明 \(1, 1'\)をterminal objectとする. \(1\)のterminal objectのUMPから, \(p': 1' \to 1 \)なる存在する. 同様にして\(p : 1 \to 1'\)も存在する.
　\(p,p'\)が同型, すなわち\(p \circ p' = id_{1'}, p' \circ p = id_{1}\)を示せば\(1 \cong 1'\)であることが分かる.

　\(p \circ p', id_{1'}\)はともに\(1' \to 1' \)なる射であるが, \(1'\)のterminal objectのUMPより\(1'\)に向かう射は一意的である. 即ち\(p\circ p', id_{1'}\)は一致するので\(p \circ p' = id_{1'}\)が分かる. 同様にして\(p' \circ p = id_1\)もわかるので, \(1 \cong 1'\)が示された. (QED)

「これでいいかな？ UMPは存在+一意性という2つの条件のことだから, それを上手く使ったよ. 射を作るのに存在を, 射が等しいことを示すのに一意性を使う感じだね」
「うん, オッケー. あとについては大体同じ感じでできるからやっておいて」
「う, うん」
　大体同じ感じ……っていうのはさすがにどうだろう. あとでちゃんとチェックしないと.
「この命題はどうかな？」

Prop \(A \times (B \times C) \cong (A \times B) \times C \)

「直積の結合律だね. 証明は, すぐには思いつかなさそうだなぁ」
「じゃあ, これは私が示そうか. 証明は先と似たような感じでできるよ. ポイントは, UMPを使って射を構成するところと, 一意性から射が等しいことを導くところかな.」

証明 \(A \times (B \times C) \to (A \times B) \times C \)を構成する. \(p^{A \times B}_A : A \times B \to A \)を射影(直積に付随する射)とする.
　\(p^{A \times (B \times C)}_A : A \times (B \times C) \to A \), \(p^{B \times C}_B \circ p^{A \times (B \times C)}_{B \times C} : A \times (B \times C) \to B \)に対し, \(\langle p_A, p_B \circ p_{B \times C} \rangle : A \times (B \times C) \to A \times B \)なる射がある. また, \(p^{B \times C}_C \circ p^{A \times (B \times C)}_{B \times C} : A \times (B \times C) \to C \)と合わせて, \(h_1 = \langle \langle p_A, p_B \circ p_{B \times C} \rangle, p_C \circ p_{B \times C} \rangle : A \times (B \times C) \to (A \times B) \times C \)なる射を得る.

　逆向きの射を作ろう. 上と同じ議論により, \(h_2 = \langle p_A \circ p_{A\times B}, \langle p_B \circ p_{A \times B}, p_C \rangle \rangle : (A \times B) \times C \to A \times (B \times C)\)を得る.

　射が構成できたので, あとはこれらが同型を与えることを見ればよい. すなわち, \(h_1 \circ h_2 = 1, h_2 \circ h_1 = 1\)を示す.

　\(h_2 \circ h_1, 1\)がともに\(f\)に対して\(p_A \circ f = p_A, \; p_{B \times C} \circ f = p_{B \times C}\)という関係式を満たすことを言えば, \((A \times B) \times C　\)の直積のUMPを図式\(A\times B \leftarrow (A \times B) \times C \rightarrow C \)に対して使うことで, 射の一意性より\(\langle p_{A\times B}, p_C \rangle = h_2 \circ h_1 = 1\)が分かる.
　\(p_A \circ 1 = p_A, \; p_{B \times C} \circ 1 = p_{B \times C}\)はよいから, \(p_A \circ (h_2 \circ h_1) = p_A, \; p_{B \times C} \circ (h_2 \circ h_1) = p_{B \times C}\)を示す.

\[ \begin{eqnarray} p_A \circ (h_2 \circ h_1) &=& p_A \circ \langle p_A \circ p_{A\times B}, \langle p_B \circ p_{A \times B}, p_C \rangle \rangle \circ h_1 \\ &=& p_A \circ p_{A \times B} \circ h_1 \\ &=& p_A \circ p_{A \times B} \circ \langle \langle p_A, p_B \circ p_{B \times C} \rangle, p_C \circ p_{B \times C} \rangle \\ &=& p_A \circ \langle p_A, p_B \circ p_{B \times C} \rangle \\ &=& p_A \end{eqnarray} \]

　同様にして\(p_{B \times C} \circ (h_2 \circ h_1) = p_{B \times C}\)および\(h_2 \circ h_1 = 1\)も分かる. よって\(A \times (B \times C) \cong (A \times B) \times C \)である. (QED)

「最後は一気にはしょったね」
「ただのdiagram chaseだからね, 自分で手を動かして確かめるしかないよ」
「まぁそれもそうかもね. しかし, 集合の時は元の対応を見るだけで明らかだったのに, 圏だと大変だなぁ……」
「直積が図式を使って間接的にしか定義されないからだね. 基本的にdiagram chaseは大変面倒くさい. でも圏論はなんでもかんでもエレガントにできるわけじゃない. 泥臭いことも勉強の一つ」
「自分で一度証明を追ってみるよ」
「それがいい. ついでにもう一つ宿題を出しておこう」

Prop(宿題)

\[ \begin{array}{c} \bullet & \rightarrow & \bullet & \rightarrow & \bullet \\ \downarrow & (a) & \downarrow & (b) & \downarrow \\ \bullet & \rightarrow & \bullet & \rightarrow & \bullet \\ \end{array} \]

という図式に対して, 以下を示せ.

• 1. 左右の四角(a),(b)がpullbackのとき, 全体もpullback
     
• 2. 右の四角(b)と全体がpullbackのとき, 左の四角(a)もpullback

「さてとりあえずこれでspecial objectの話は終わり」
「special object？」
「うん. ここでやった概念は覚えておくといいよ. あとでまた出てくるから」
「なるほどね」
　千景はそう言って, 椅子から立ち上がった. ゆっくりとした足取りで黒板の前に立つ. ぼうっとしている僕からチョークをひったくって黒板に向かった.
「私たちは圏とその上のspecial objectを定義した. まだ話していなかったけど, 関手は圏から圏への変換のことね」
「関手と自然変換って概念があるって言ってたね. 自然変換は？」
「自然変換は関手から関手への変換」
「変換ばっかりだね」
「圏論ではこうやって, 色んな物が抽象的に定義されていく. 関手や自然変換がどの意味で"抽象的"なのかはまだ言わないけど, とにかく圏, 関手, 自然変換と進むに連れて, 視点はどんどん広くなるの」
　千景は黒板に不思議な絵を書いた. 一番右下に圏, その上に矢印を引っ張って関手, さらにその上に矢印を引っ張って自然変換と記した.
「けれど, 視点の広さは変えないで, 色んな物をより深く, より精密に見ることもできる」
「どういう意味？」
「例えばspecial objectね. 抽象度は上げないままで, 圏の上で条件をつけたりしながら特別な概念を追求する」
　圏と書かれたところから左に矢印を引っ張って, "special object"と書いた. さらに千景はその下に, "終対象, 直積, equalizer, pullbackなど"と付け足した.
「左に向かうのは理論の緻密さ, 上に向かうのは理論の高さ. 緻密な理論ほど細かい条件に対応できるし, 高い理論ほど抽象的に話が進む」
「ふむ」
　一体彼女は何がいいたいのだろう. いや楽しそうなのはすごく伝わってくるんだけどね.
「じゃあ, 関手くらいの高さで, special objectくらいの緻密さのある概念は何？」
「は？」
「言葉を変えようか. special objectを関手の言葉を使って一般化できるかな. あるいは, 関手の言葉を使ってspecial objectに対応するものは作れるかな」
「えっと, 何を言ってるのかさっぱりわからないんだけど」
「結論から言おう, それにはちゃんと名前がついてる. その説明をする前に……」
　千景はチラッと僕を見た.
「関手と自然変換の定義をしてしまおう. これでようやく, 圏のまともな絵がかける」
「うーん」
　日本語でお願いします. って言いたかったけど, 千景の楽しそうな話に水を差したくなかったので黙っていた.
　攻守交代, 僕は一番前の席に腰掛けて, 千景の話に耳を傾けた. 日暮れ前の空は紫色でなんとも得体の知れない色をしていたけれど, 僕にはそんな空もいつもと同じく綺麗に見えた.

補足

千景が出した"宿題"は, two pullbacks lemmaと呼ばれます. 証明は https://proofwiki.org/wiki/Pullback_Lemma などを参照してください.