小学生の頃（たぶん）、ササジマさんに教わった天国地獄問題を思い出した。
他に：
などの分析も面白い。本編記事だと：
例題：
もうひとつ
まずテンプレートとテンプレートの変形ルール。意味規則は変形ルールにより定義される。
変形ルール1の適用
別な変形ルール
変形ルールの精密化
適用
「順序圏」はどうなるだろうか？ 「順序集合を対象とする圏」「順序構造を持つ圏」あるいは「ホムセットが順序構造を持つ圏」。
別な変形ルール
別な変形ルール
適用
別な変形ルール
適用
あらゆるリストはラベル付きリストだと考える。ラベルを一緒にした項目をラベル付き項目と呼ぶ。ラベル付き項目は、ラベルとデータのペア（「値」は使わないで、「データ」とする）。
型宣言を $`\in:`$ 、所属関係を $`\in`$ 、ラベルとデータの区切りをコロンとする。
コロンがラベル区切りと型宣言として、同時に使われている。所属記号が宣言の記号に流用されている。
値の多義性
違いと類似性は：
関数値も像の要素を指しているのか、割り当てペアを指しているのかが曖昧。多くの場合、割り当てペア。一般と個別特定の区別も難しい。個別特定から一般への汎化作用がある。
流用も転用もオーバーロードが起きるもとになる現象。
P が生きている人の集合、'親子' が親子関係、'親'と'子'が関係における役割り名（ペアのポジションに付けた名前、成分射影に付けた名前）。'親'と'子'は関係に対応する述語 P✕P → Bool の名前付き引数の名前、引数変数名。
R := 親子関係 と置いて、R は外延だとする。
役割り名（引数変数名、引数ラベル）であった'親'は射影関数の名前に流用（あるいは転用）される。
get_親 : R → P in Set
関係付きペア〈related pair〉（R の要素）の第二成分を取る関数。
ニ項関係から二種類の非決定性関数が得られる。そのうちのひとつは：
親_of_ : P → P in NDet
get_親 の像集合と 親_of_ の像集合は一致する。
The_親_s := Img(get_親) = Img(親_of)
The_親_s ⊆ P
'親'は、関係における単なる関係ラベル（タブルを関数とみての引数）。get_親 はラベル '親' のゲルファント変換。親_of はワイヤーストレッチング。The_親_s は像集合。one_親 ∈ The_親_s は要素。
まとめると：
集合の所属関係と、そこでの役割り名 '要素', '集合' に同じ議論を適用すると：
The_集合_s に空集合が入らなくなる。これは、空集合が定義上アトムだから。
依存型理論の「インスタンス」に次の形容詞を付ける。
各形容詞に、さらに修飾できる形容詞
形容詞を Is_形容詞 で述語化したとき、他の形容詞が付けられるかは、コンテキスト拡張の問題になる。
否定辞は non-, un-, 非、不 など。形容詞に否定辞を付けられる。
一般名詞に形容詞をつける、否定辞付き形容詞をつける場合に、意味がどう変わるか？
例：
根本的誤解 補遺： 誤認・誤解の原因 - 檜山正幸のキマイラ飼育記 (はてなBlog) で、
を述べたが、
もある。「名前が同じだから同じモノだ」「名前が違うから違うモノだ」という信念、それに伴う誤認・誤解。
文脈を忘れてしまう症状は、文脈健忘症。
$`f:X \to Y`$ があるとき、$`(X, f)`$ を何と呼ぶか？
rank, label, grade, sort, type, color, tag, role などを属性名とする attributed set で統一的に記述できる。いずれも single-attributed set になる。
attributed set は：
$`\quad f : X \to \sum_{a\in A}Y_a`$
single-attributed set でも multi-attributed set = attributed set でも、バンドル-ファミリー対応でファミリーとみなすことができる。
基底
派生
なぜやばいのか：
去年の11月、12月あたりの知見だが：
Lean と AI に関してわかったこと：
AIは、十分に物知りで優秀だが、虚言癖があって“知ったか”するヤツと思って付き合えばよい。
