構文 レコード ::= '{' 文並び '}' 文並び ::= 空 | 文並び ';' 文 文 ::= 空文 | 宣言文 | 定義文 宣言文 ::= 種 名前 プロファイル 定義文 ::= 種 名前 ':=' 項種付きレコードは、 種付きレコード ::= 種 レコード種〈区分 | division〉を列挙： type func…

value x:X を function x:->X の略記とするなら、type X:Set を functor X:->Set の略記と考えることが出来るな。 Cat in Doctrines functor F:C->D in Cat functor X:->C 略記⇒ type X:C トランスフォーを使うと： 1Cat in 2Cat(Doctrines) 1transfor F:C->…

ゴグエンが、指標の圏にはインクルージョン構造が必要だといっていた。ΔからΣへのインクルージョンはあってもひとつだから、Δ⊆Σ という記法が意味を持つ。Δ⊆Σのとき、引き算Σ＼Δが意味を持ち（持たせて）、Σ Σ＼Δ # Δ が成立するようにする。そうすれば、変…

最初に与えられるハイパードクトリンとエルブランモデルで作られるインスティチューションをレイヤー0（L0）と言うことにする。L0の上にレイヤー1インスティチューションを構成するのが問題なのだが、結局、レイヤー1はレイヤー0と同型である、という事だと…