管理・配布のメカニズムと論理構成素 - (保存用) 檜山正幸のキマイラ飼育記メモ編

リポジトリからパッケージをストレージに持ってくることをインストールと呼ぶ。インストールされたパッケージの集合体を（ストレージ化された）ライブラリと呼ぶ。ライブラリに対応する配布形式をディストリビューションと呼ぶ。

モジュール、パッケージ、ディストリビューションそれぞれに作成者や著作権がある。

プリミティブ〈原始、基本〉と絶対〈absolute〉という形容詞を付けることができる（無意味なこともある）。

最近のフェイク情報問題は、命題と定理の区別が付いてないことが原因。

非絶対定理を条件付き定理〈conditional theorem〉とも呼ぶ。条件付き定理を絶対定理に書き換えられることを主張するのが演繹定理。

基本命題、基本定理、基本手続きはコンピュータッドを定義するので、2-圏が生成される。その2-圏を論理圏と呼ぶ。

用語法：基本定理はなんか誤解されそうだから、原始命題、原始定理、原始手続きがいいかも。命題、論理式、論理文は区別しない。

僕は「型クラスないと死んじゃう」病なので、当然に型クラスは入る。

指標：型、関数、関係を表す変数の集まり。型理論の型文脈と同様なものだと思ってよい。指標の上に項〈term〉の集合と論理式〈命題〉の集合が定義できる。
項は指標射を定義する材料に使う。論理式は、論理圏の対象となる。
論理圏は、最初は最小の両付点デカルト閉圏または両デカルト閉圏として与えられる。
公理（原始射＝生成射）の追加で、最小のデカルト閉圏を膨らますことができる。
公理の追加で、対応するモデル圏は縮退して小さな部分圏に制限される。
型クラスは、指標と、その指標上の論理圏の対象のペアなので、グロタンディーク平坦化の対象となる。
型クラスにより、指標のモデル圏（＝マグマ圏）の部分圏が決まり、それが型クラスのモデル圏となる。
型クラスのモデル圏の対象を、その型クラスのインスタンスと呼ぶ。インスタンスを構造〈structure〉とも呼ぶ。
論理圏をインデックス付き圏とみなした場合のグロタンディーク平坦化の射をトランスレーション〈翻訳〉と呼ぶ。トランスレーションは型クラスと型クラスを繋ぐもの。

簡素化したいので、

新しい論理構成素は：

管理・配布と論理は直交しているので、お互いに干渉することはない。モジュールには何を書いてもよい。