部分トレース付き圏（Partially Traced Category）
「一様性を持つ圏」において、部分的に定義されたトレースの概念を導入したが、僕よりずっと気が利いた定義が、"Towards a Typed Geometry of Interaction" by Esfandiar Haghverdi, Phillip J. Scott （http://www.site.uottawa.ca/~phil/papers/HS-APAL-05.pdf）にあった。
これは、ジラールのGoIの拡張であるMGoI（Multiobject GoI）を提唱している論文。部分トレース付き圏の定義はけっこう複雑。C = (C, ×, I, σ)が対称モノイド圏として、Cをベースとしてその上に構造を載せていく。
X, Y, U∈|C|ごとに、3パラメータの集合族T(X, Y; U)⊆C(X×U, Y×U)が指定される。Tが全体として部分圏となることは要求しない。トレースの各公理に対応して、Tに要求される条件を決めていく。
- タイトニング（自然性）g:X'→X, h:Y→Y' のとき、 f∈T(X, Y; U), ⇒ (g×U);f;(h×U)∈T(X, Y;U)
- スライディング（対角自然性） f:X×U→Y×U', g:U'→U のとき、f;(Y×g)∈T(X, Y; U) ⇔ (X×g);f ∈T(X, Y; U7)
- バニッシング I T(X, Y; I) = C(X×I, Y×I)
- バニッシング II g∈T(X×U, Y×U; V) のとき、g∈T(X, Y; U×V) ⇔ TrX×U, Y×UV(g)∈T(X, Y; U)
- スーパーポージング f∈T(X, Y; U), g:W→X ⇒ g×f∈T(W×X, Z×Y; U)
- ヤンキング σU, U∈T(U, U; U)
定義域に関する条件を上のようにして、後は通常のトレース公理群をかんがえる。
トレースの定義域であるT⊆Morph(C)をトレースクラスと呼ぶ。トレースクラスに属する射はトレーサブル射、または（用語の濫用で）トレースクラス射と呼ぶ。トレースクラス上で定義された部分トレースも含めてトレースクラス構造と呼ぶこともある。
トレースクラス構造(T, Tr)を備えた対称モノイド圏が部分トレース付き圏である。
印象的な例は、有限次元ベクトル空間と直和の圏で、X(+)U→Y(+)U を行列表示したときの2-2成分をd:U→Uとして、U - d:U→Uが可逆であるモノをT(X, Y; U)として、言語理論と同様に(U - d)-1 = d* = 1 + d + d2 + ... を使ってトレースを定義した圏。
もうひとつの例は、完備距離空間の非拡張的（non-expansive）連続写像からなる圏にトレースクラス構造を定義したもの。fがトレースクラスであるのは、f:X×U→Y×U として、x∈Xごとに決まるπ2・λu.f(x, u):U→U が一意不動点を持つとき。
注意すべきは、π2・λu.f(x, u) が、どんなxに対しても縮小写像という定義では整合性に欠けること。スライディングとバニッシングIIが成立しない。
トレースクラス、部分トレース付き圏の定義はけっこう面倒だが、アラン・ジェフリーの簡略化されたトレース公理により少し簡略化できるかもしれない→セリンガーの論文 - 檜山正幸のキマイラ飼育記 メモ編。プロトキン、長谷川などの一様性原理を考えるのも部分トレース付き圏がふさわしい気がする。
つまり、トレースクラス構造と厳密クラス（または酵素クラス）構造をもった圏を考えて、そこで一様性原理（ホーン等式で記述される）を導入することになる。→一様性原理 - 檜山正幸のキマイラ飼育記 メモ編、→コゥゼン圏（Kozen圏）とクリーネ圏（Kleene圏） - 檜山正幸のキマイラ飼育記 メモ編。これは、証明論（カット消去）にも関係するらしい。
