Relを関係圏（the category of relations）とします。R:A→B in Rel のとき、RはAとBのあいだの関係なので R⊆A×B ですね。(x, y)∈R であることを xRy とも書くことにします。また、x∈A に対して R(x) := {y∈B | xRy} と定義します。
Aが基点付き集合（pointed set）だとは、Aは集合で、Aの要素が1つ特定されていることです。記号を乱用して、基点付き集合を A = (A, ⊥A) のように書くことにします。⊥AはAの基点です。
圏PtRelを次のように定義します。（well-definedであることは示す必要があります。）
- PtRelの対象は基点付き集合である。
- A = (A, ⊥A) から B = (B, ⊥B) への射は、AからBへの関係Rである。
- ただし、R(⊥A) = {⊥B} を満たす。
- 射の結合は関係の結合、恒等射は対角で与えられる。
圏PtRelは、射が R(⊥A) = {⊥B} を満たす以外はRelとほとんど同じです。対象が基点付き集合なので、空集合はこの圏の対象になりません（基点を持てないので）。
ホムセット PtRel(A, B) の部分集合 PtReltotal(A, B) を、全域（total）な関係の集合として定義します。関係 R:A→B が全域とは、次が成立することです。
- ∀x∈A.∃y∈B. xRy
全域な関係だけを集めるとまた圏ができるので、それをTotPtRelとします。TotPtRel(A, B) = PtReltotal(A, B) 。TotPtRelは、PtRelの広い部分圏（|TotPtRel| = |PtRel|）です。単なる集合Aに対して A⊥ = (A + {⊥A}, ⊥A) を対応させて、関係の未定義部分の値を{⊥}で補充すると、RelをTotPtRelに埋め込むことができます。
この圏TotPtRelは、必要があって作ったのですが、なんだか奇妙なところがあります。以下で、関係 R, S に対して R∪S は、関係を集合とみなしての合併です。「+」と「×」は、通常の集合の直和と直積とします。また、A○ := A - {⊥A} （基点付き集合から基点を除いた集合）とします。
- A # B := A○ + B○ + {⊥} とすると、A # B は直和になる。
- しかし、直積は存在しないようだ（たぶん）。Relでは（圏としての）直和と直積が一致するのとは事情が違う。
- A×B はモノイド積になるが（圏としての）直積ではない。直和に対して分配的にもならない。
- A*B := A○×B○ + {⊥} とすると、これもモノイド積になるが、直積ではない。直和に対して分配的となる。
- 自然な（と思える）射 A×B→(A # B) と A*B→(A # B) があるが、この2つは別物だ（2つを関係付ける可換図式がない）と思える*1。
- 自然な（と思える）射 (A # B)→A×B があるが、(A # B)→A*B はないようだ。
- ホムセットごとに演算∪があり、可換で結合的だが、単位元（中立元）がない。空集合は関係として認めてないので。
- 単元集合が零対象であり、ホムセットごとに零射があるが、零射が合併の単位元（中立元）にはならない。
- 射の転置はうまくいかない。関係圏Relでは常に転置を取れる。Relに比べて対称性が弱い。
TotPtRelは、SetともRelとも似てないのです。全然似てないかというと、そうではないのですが、期待した法則性が微妙に食い違ってしまい、SetやRelとの類推に頼ると落とし穴があるという感じ。
圏TotPtRelは、単に「変な例」として構成したわけではなくて、無限走行と非決定性を持つ計算のモデルのつもりです。演算「#」「×」「*」「∪」はどれも必要そうです。それぞれ、「どちらか一方の選択」「待ち合わせをしないタプリング」「待ち合わせをするタプリング」「非決定性の重ねあわせ」を意味します。TotPtRelが奇妙なのは、モデルとして不適切なのか、なにか間違いを犯しているのか、それとも現象がソンナモノなのか？ よくワカリマセン*2。もっといじくり回していると分かるかも知れませんが。
