JcentricTS, 現状わかったこと
Jcentric型システムの宣言スタイル・スキーマ構文 - 檜山正幸のキマイラ飼育記 (はてなBlog)の意味論のほうの話。
- Posetoidの導入は避けられない。Posetoid自体はデカルト閉っぽい。
- Posetoidの圏の変種は、必ずしもデカルト閉にはならない。
- category with embeddings という概念が必要。
- embedding := projectable（造語）な射として埋め込み概念を定義する。
- アイソトピーが定義できる。
- アイソトピー＝通常のアンビエントアイソトピーかどうかまだ分からない。
- 直和に関するアイソトピー定理を示せる。
- 直積に関するアイソトピー定理を示せる。
- Cを背景圏、Aをアンビエント対象、K⊆|EO(C, A)| として、Kから生成されたCの部分圏は、EO(C, A)にup-to-isotopyで埋め込める。「アイソトピー埋め込み定理」と言っていいだろう。
- あとはinclusion structureを明確に作る。
なんだかんだ考えているうちに、新しい概念／用語をイッパイ作ることになったなー。
- setoidがクリスプ（crips） :⇔ 同値関係がイコール
- posetが平坦 :⇔ (x≦y ならば、x = y または x = ⊥)
- posetが強平坦 :⇔ 平坦で⊥がない
- posetが離散的 ＝ 強平坦
- setoidが離散的 ＝ クリスプ
- posetoidが離散的 ＝ クリスプかつ強平坦
- posetが厳密 :⇔ ⊥を持つ
- 射が厳密 :⇔ ⊥を保存する
- f, g:X→←Y が劣同型ペア :⇔ f;g ≦X, g;y≦Y
- fがプロジェクタブル :⇔ (f, p)がEPペアとなるpが存在する
- fが埋め込み ＝ fがプロジェクタブル
- 2つの埋め込みがアイソトピック :⇔ アンビエント対象の劣同型ペアで互いに移れる
