付点非空ベキ集合モナドのクライスリ圏を使う

(-)+⊥ を Set→Set の自己関手で付点するモナドだとする。このクライスリ圏は部分写像の圏と圏同値で、アイレンベルグ／ムーア圏は付点集合の圏PtSet。この例では、クライスリ圏とアイレンベルグ／ムーア圏が同値。

付点集合の圏に非空ベキ集合関手を作用させてさらにクライスリ圏を作る。このとき、Set上の複合モナドは Pow₊(- +⊥) と書ける。このモナドのクライスリ圏をNTNDとする。non-terminating non-deterministic から。

クライスリ圏を2回作っているだけなので、対象類は変わらないので、|NTND| = |Set|。この理由から、NTNDの対象も集合として書く。A, B∈|NTND| = |Set| に対して、f:A→B in NTND とは、f:A+⊥→B+⊥ in Rel （ただし全域） と解釈できる。A×B、A+B も意味は単純な直積、直和ではない。Rel内で解釈するなら、(A+⊥)×(B+⊥） と A + B + ⊥ になる。

この圏NTNDが具合がいいのは、A×B→A+B in NTND が「待たないで行け」を表現できること。(A+⊥)×(B+⊥）→ (A + B + ⊥) は、(A×B + A×⊥ + B×⊥ + ⊥×⊥） → A + B + ⊥ となるが、⊥を待たないように定義すれば、直感に一致する。