続・型の意味

背景圏としては、Posetoidを使うが、次のような組 (X, p)を考える。

1. Xはposetoid
2. pはXからΩ={true, false, ⊥}への射

スライス圏を考えるわけではない。射はPosetoidと同じ。ただし、次のような演算を考えることができる。

1. (X, p) | (Y, q) = (X+Y, [p, q])
2. (X, p) * (Y, q) = (X×Y, p(*)q)
3. (X, p) & (X, q) = (X, p∧q)

[p, q]は余デカルトペア、(*)は∧（かつ）を使ったテンソル積、∧は単にブール演算。inclusion structureがあれば、& の定義はもう少し拡張できて：

1. (X, p) & (Y, q) = (X∩Y, p∧q)

∩の定義は、XとYの共通アンビエント領域への埋め込みを使って定義する。