Lawvere流セオリー

Lawvere流のセオリーの理論がよくわかってないから、変なことを書くかもしれないが、それもよしとしよう。

指標ΣのLawvere代数セオリーLawvereAlgTh(Σ)とする。これは対象（の集合）がNと同型な圏で、Σの記号が射として追加されていて、最小な圏ということだろう。圏Cから圏Dへの関手の圏（射は自然変換）を[C, D]と書くことにすると、

• [LawvereAlgTh(Σ), C] ≒ Alg_Σ(C) （≒は圏同値）

Alg_Σ(C)は、圏C内のΣ代数の圏。

いまいち曖昧な書き方なのだが、LawvereAlgTh(Σ) = LawvereTh(Cartesian, Σ)と書いてみる。Catesianとは定数記号を持たない、デカルト・モノイダル圏のセオリーとする。ここで出た“セオリー”は古典的等式的セオリーのこと。

U∈Cだとして、Uをgenerating objectとするLawvere流セオリーのモデルは[LawvereTh(Cartesian, Σ), (C, U)]と書く。セオリーのただ１つのソート記号に対応する対象をUにする、ということ。

LawvereTh(Cartesian, Σ)以外に、

• LawvereTh(Cocartesian, Σ)
• LawvereTh(Bicartesian, Σ)
• LawvereTh(SymmetricMonoidal, Σ)
• LawvereTh(CompactClosed, Σ)

とかを考えて（単項生成の最小）モデルを考えると、計算できる小さな圏が作れそうだ。特に、LawvereTh(CompactClosed) = LawvereTh(CompactClosed, Φ)はKelly達が作ったモデルのような気がする。