ドクトリンとハイパードクトリン

ドクトリンは、CCCのような、Cat上の具象圏だとする。ハイパードクトリンは拡張されたドクトリンくらいの意味だが、

1. ベース圏（論域の圏）の上のインデックス付き圏であり、余域はCCCのようなドクトリンになる。
2. ベース圏の射に対して、ΣΔΠ随伴性がある。Σは存在限量子、Πは全称限量子に対応する。

抽象化すれば、ハイパードクトリンは、随伴概念を持つ2圏Dへの反変関手であり。ψ:S→T in C に対して F(f): F(T)→F(S) in D が左随伴Σ_fと右随伴Π_fを持つようなもの。

ハイパードクトリンのベースドクトリン（ベース圏が所属するドクトリン）と論理ドクトリン（値が所属するドクトリン）が決まれば、ベース圏と論理ドクトリンに対して、ハイパードクトリンを決めることができる。ベースドクトリンは随伴性を持たなくてもいいが、論理ドクトリンは必ず随伴性を持つ必要がある。そうでないと述語論理ができない。

ただし、ベース圏が単元圏のときは話が別で、単元圏の上のハイパードクトリンは単に論理ドクトリンに所属する論理圏だから、単一の論理圏の話、つまり命題論理となる。

単元圏（＝自明圏）は終対象を持つ。終対象の上の論理圏が真理値圏だから、単元圏上のハイパードクトリンは真理値圏も持つ。

単元圏の次に簡単なベース圏は2元圏で、恒等射以外に単一の射影を持ち、射影の余域が終対象となるような圏。ここでは、論域Xと終対象1だけがあり、標準的な限量子があり、簡単ながらも普通の述語論理が完全に展開できる。

X, Y, X×Y, 1の4元を対象として、恒等射以外に5本の射を持つダイヤモンド形の圏を考える。ここでは2変数の述語論理が展開できる。全称限量子だけ書くと。

1. ∀x. on x, y
2. ∀y. on x, y
3. ∀x. on x
4. ∀y. on y
5. ∀x, y. on x, y

可換性は

• (∀x. on x, y);(∀y. on y) = (∀y. on x, y);(∀x. on x) = (∀x, y. on x, y)

普通に書くと：

• ∀y.∀x.P[x, y] = ∀x.∀y.p[x, y] = ∀x, y.P[x, y]