簡易インスティチューションのすごく簡単な例

多項式インスティチューションは簡易インスティチューションの簡単な例だと思う。似たような例に命題論理のインスティチューションがある。が、もっと簡単な例がある。

Pow_*、Pow^*をそれぞれ、共変と反変のベキ関手だとする。Pow_*(f)をf_*、Pow^*(f)をf^*と略記する。集合Xに対するPow_*(X)とPow^*(X)は同じものだから、Pow(X)とも書く。

X∈|Set|だとして、Pow^*(X)×Pow_*(X) = Pow(X)²の関係|=_X を次のように定義する。

• A, B∈Pow(X)に対して、A |= B とは B⊆A のことだと定義する。

以上の状況で、(Set, Pow_*, Pow^*, |=)は、指標圏Set、文関手Pow_*、モデル関手Pow^*、充足関係族 |= から成る簡易インスティチューションになる -- 次の充足条件が成り立てばよい。

• f:X→Y、A∈Pow(X)、B∈Pow(Y)に対して、f^*(B) |= A ⇔ B |= f_*(A)。

=の定義によれば、これは次のことを意味する。

• A⊆f^-1(B) ⇔ f(A)⊆B 。

上の命題が成り立つことは練習問題だろう。