自由コゥゼン圏（Kozen圏）

コゥゼン圏は、トレースを持つベキ等・双デカルト圏のこと（だとしたが、ベキ等を落としてもいい気もするが）。圏的指標Σがあるとき、Σから自由コゥゼン圏FK(Σ)を作れる。FK(Σ)は、Σの正規表現全体の代数に対応し、FK(Σ)の射は正規表現。

圏的指標Σはグラフと考えてよい（プレ圏だと考えるのが正確）。アンビエント・コゥゼン圏C（意味領域）を適当に固定して、グラフ準同型γ:Σ→C があるとする。γはFK(Σ)→C のコゥゼン関手に拡張できる。コゥゼン関手は“コゥゼン圏の圏”の射、トレース付き双デカルト構造を保つ関手。γの拡張Γによる射の像は「正規表現の意味」を与える。

もちろん、忘却関手U:KozenCat→Graphと自由生成関手FK:Graph→KozenCatは随伴。