Pos 

Awodey は和訳が見つからなかったので勝手訳になる:

数学でよく見るものに構造的集合 (structured set)、つまり集合に何らかの「構造」を追加したものと、それを「保存する」関数の圏というものがある。(構造と保存の定義は独自に与えられる)

半順序集合 (partially ordered set)、または略して poset と呼ばれる集合 A は、全ての a, b, c ∈ A に対して以下の条件が成り立つ二項関係 a ≤A b を持つ:

  • 反射律 (reflexivity): a ≤A a
  • 推移律 (transitivity): もし a ≤A b かつ b ≤A c ならば a ≤A c
  • 反対称律 (antisymmetry): もし a ≤A b かつ b ≤A a ならば a = b

poset A から poset B への射は単調 (monotone) な関数 m: A => B で、これは全ての a, a’ ∈ A に対して以下が成り立つという意味だ:

  • a ≤A a’ のとき m(a) ≤A m(a’)

関数が単調 (monotone) であるかぎり対象は圏の中にとどまるため、「構造」が保存されると言える。poset と単調関数の圏は Pos と表記される。Awodey は poset が好きなので、これを理解しておくのは重要。

poset の例としては Int 型があり、 として PartialOrder 型クラスで定義されているように整数の比較である <= を使う。 別の例として、case class LString(value: String) を考えてみる。 としては value の文字列の長さを比較に使う。

scala> :paste
// Entering paste mode (ctrl-D to finish)

case class LString(value: String)
val f: Int => LString = (x: Int) => LString(if (x < 0) "" else x.toString)

// Exiting paste mode, now interpreting.

defined class LString
f: Int => LString = <function1>

scala> f(0)
res0: LString = LString(0)

scala> f(10)
res1: LString = LString(10)

上の f は、f(0) ≤ f(10) および a <= a' を満たす任意の Int において f(a) ≤ f(a') であるため、単調である。

Contents