確認しよう、指標とモデル

• 指標の圏はだいたいこれでOKだろう - 檜山正幸のキマイラ飼育記 メモ編
• 昔から言っていたことだった - 檜山正幸のキマイラ飼育記 メモ編
• 形式言語系の定義 - 檜山正幸のキマイラ飼育記 メモ編
• 指標について色々 - 檜山正幸のキマイラ飼育記 メモ編
• 観測可能論理と隠蔽論理 - 檜山正幸のキマイラ飼育記 メモ編
• プログラミング言語概念の定義 - 檜山正幸のキマイラ飼育記 メモ編
• 指標と枠 - 檜山正幸のキマイラ飼育記 メモ編

インスティチューションの枠内で、具体的な指標から具体的にモデルを作る話。

1. 指標はグラフ、またはプレ圏。
2. グラフから自由生成された圏（道の圏）の合同がセオリーになる。
3. 指標が前もってプレ圏（圏でもよい）なら、セオリーは一般化合同。
4. グラフに境界概念を入れると、隠蔽ソート＝内部ノードができる。
5. 指標の圏には、直和、直積、境界でのグルーイングが入る。
6. グラフのファイバー和（貼り合わせ）が必要。上江州アタッチメントも貼り合わせ。
7. 指標の圏に、構文生成モナドが働いている。
8. 指標の圏をKleisli拡張できる。
9. モデルの圏は関手圏である。モデル射は自然変換。
10. 圏Cごとに、C-モデルが考えられる。ただし、Cは指標圏のセオリーと整合するとき。
11. モデルを作るとき値となる圏Cをアンビアント〈アンビエント〉圏（または背景圏）と呼ぶ。
12. 指標Σから自由生成した圏Σ^~をセオリー（一般化合同）で割った圏は、アンビアント圏と同じ種類の圏である。

圏的セオリー（categorical theory）とは、一般化合同のことだとすると、セオリーのモデルは、商圏からの関手となる。モデルの全体は圏の圏であり、セオリーのモデル圏と呼ぶべきものとなる。「デカルト圏のセオリー」「双デカルト圏のセオリー」「CCCのセオリー」「コンパクト閉圏のセオリー」などが考えられる。