ほんとに必要な概念

1. ストラクチャ＝{構造体 | クラス | 型クラス | レコード | 指標 | オブジェクト}
2. トランスフォーマ＝{ファンクタ（SML） | 型クラス・インスタンス | セオリー}
3. プロファイリング ： ストラクチャのメンバーの一部
4. バインディング ： ストラクチャのメンバーの一部
5. 名前＝識別子 ： ストラクチャのメンバーのキー
6. メンバー： 名前、プロファイルは必須で、オプショナルな値からなる。
7. 項： 評価されと、プロファイルまたは値となる式。
8. プロファイル項： 評価されと、プロファイルとなる式。
9. 値項： 評価されと、値となる式。

プロファイル項

1. ドクトリン項 : 圏のプロファイル
2. 圏項 ： 対象のプロファイル
3. 対象項 ： 射のプロファイルの一部
4. ホムセット項 ： 射のプロファイル
5. 圏項 ： コンストラクタのプロファイルの一部
6. コンストラクタ項 ： トランスフォーマーのプロファイルの一部

名前	プロファイル形式
圏名	ドクトリン項
対象名	圏項
射名	対象項 -> 対象項 （ホムセット項）
コンストラクタ名	圏項 -> 圏項
コンビネータ名	コンストラクタ項 -> コンストラクタ項 => (同様)

出てくる名前

1. ドクトリン名 ： CCCなど
2. 圏名 ： Setなど
3. 圏の対象名 : nat など
4. 圏の射名 ： +, 0 など
5. コンストラクタ名 ： DirectProd, Squre など
6. コンビネータ名： diag, comp, terminal

以上の名前は、インデックス付き圏のベース圏と垂直圏に対して使う。ハイパードクトリンのグロタンディーク圏（平坦化した圏をそう呼ぶ）の対象はストラクチャ、射はトランスフォーマー。

圏	その対象	その射
アンビエント圏	型	関数
ベース圏	指標	指標射
垂直圏（ファイバー）	命題	定理
グロタンディーク圏	仕様	セオリー

注意事項：

1. アンビエント圏はドクトリンから選ぶ
2. アンビエント圏は型〈type〉と関数〈function〉の圏である。
3. ハイパードクトリンの余域はドクトリンから選ぶ
4. ベース圏はアンビエント圏と識別子集合〈Name〉から構成する
5. 指標は、プロファイリングのリストである。
6. 指標射は、名前集合のあいだを繋ぐ、forkと関数ノードから構成されるクローンと呼ばれるグラフである。
7. 指標はプロファイリングだけを持つストラクチャ〈structure〉で表現する。
8. 指標射はトランスフォーマー〈transformer〉で表現する。
9. 命題は普通の論理式構文で定義する。
10. 論理結合子はコンストラクタである。
11. 推論規則はコンビネータとして定義する。

圏論	ソフトウェア
ドクトリン	暗黙
アンビエント圏	型の型
対象	型 type
射	関数 function
ベース圏	暗黙
ベース圏の対象	プロファイリングだけの structure
ベース圏の射	関数だけの transformer
垂直圏	proposition の値として暗黙
垂直圏の対象	命題 proposition
垂直圏の射	定理 theorem
グロタンディーク圏	暗黙
グロタンディーク圏の対象	structure
グロタンディーク圏の射	transformer

注意事項

1. 名前空間 ： ストラクチャの用法のひとつ。実体はストラクチャ
2. 名前パス＝完全修飾名
3. 型クラス、クラス、インターフェイス、指標は、ストラクチャの利用法
4. インスタンス、セオリーは、トランスフォーマーの利用法

結果、ソフトウェア的に必要な概念

1. doctrine ほとんど不要
2. category ほとんど不要
3. type 対象名のバインディング
4. function 射名のバインディング
5. proposition 垂直圏の対象名のバインディング
6. theorem 垂直圏の射名のバインディング
7. structure ベース圏とグロタンディーク圏の対象名のバインディング
8. transformer ベース圏とグロタンディーク圏の射名のバインディング
9. constructor 関手と自然変換のバインディング、ほとんど不要
10. combinator 関手と自然変換のバインディング、ほとんど不要

別名

1. doctrine : bland
2. category : kind
3. type : sort
4. function : value
5. proposition : assertion, constraint, condition, hypothesis
6. theorem : axiom, conjecture, fact, confirmation
7. structure : class, typeclass, specification, interface, signature, record
8. transformer : theory, object, instance, implementation, simulation, simulator

型は単純なストラクチャに、関数は単純なトランスフォーマーに埋め込める。

// 自明なストラクチャ テータ
structure Θ = {}

structure S := {
 ...
}

structure T := {
// プロファイル部
  t1 : T1,
  t2 : T2
// 命題バインディング部
 propositons
  q1 := Q1,
  q2 := Q2
}

transformer Foo : S -> T := {
// 変換関数達 transforming functins
 function >t1 := {
 }
 function >t2 := {
 }
// 変換定理達 transforming theorems
 theorem >q1 := {
 }
 theorem >q2 := {
 }
}

簡単な例：

structure T := {
// プロファイル部
  t1 : int,
  t2 : int
// 命題バインディング部
 propositons
  q := t1 ≦ t2,

}

transformer Foo : Θ -> T := {
// 変換関数達 transforming functins
 function >t1 := 1
 function >t2 := 2

// 変換定理達 transforming theorems
 theorem >q := {
  1 ≦ 2 by trivial
 }
}

別名とシュガーを使って書くと：

class T := {
  t1 : int,
  t2 : int
 assertions
  q := t1 ≦ t2,
}

object Foo : ->T := {
 value for t1 := 1
 value for t2 := 2

 confirmation for q := {
  1 ≦ 2 by trivial
 }
}