T. Wilkinson/Electronic Notes in Theoretical Computer Science 286
(
2012
)
323
从
X
到
Y
的函数,
f R
[
(X
,
R
X
)
,
(Y
,
R
Y
)
]
g惠<$x∈X f(x)R
Y
g(x)
此外,我们可以定义附加的单位
η
(X
,
R
X
)
:(
X
,
R
X
)→[(
Y
,
R
Y
)
,
(
X
,
R
X
)×(
Y
,
R
Y
)]
由η
(X
,
RX
)
(x)=
fx
:(Y
,
RY
)→(X
,
RX
)×(Y
,
RY
),其中
fx
(y)=
(
x
,
y
),以及伴随函数的计数
ε
(Z
,
R
Z
)
:[(Y
,
R
Y
)
,
(Z
,
R
Z
)]
×
(Y
,
R
Y
)→(Z
,
R
Z
)
通过
ε
(
Z
,
RZ
)
(
g
,
y
)
=g
(
y
)
.
因此,我们有以下命题。
命题3.2
范畴
集合
R
是闭范畴。
在本文的其余部分,我们做了以下假设。
假设1
范畴
A
和
X
对于某个固定的关系
类型
R
在集合
R
上是丰富的。此外,范畴
A
和
X
是具
体范畴,即 对象是具有某种附加结构的集合,并且携带
R
类型的关系,并且
态射具有潜
在的
R-
保持函数。
我们这样做有两个原因。首先,在
集合
R
上丰富是
[6
,
7]
方法的明显推广,其
次,为了研究表达性,我们需要访问
X
中对象的各个状态
例
3.3在R是类型等式的情况下,则
集合
R
上的扩充只是普通的范畴论,因此我们
从文献中得到了所有逻辑连接的例子,例如参见
[5]
。
下面的例子是我们的主要例子,当我们讨论表达性时,它将突出显示。
例3.4在集合
R
上,在MSL(与
top
相交的半格)和集合
R
本身之间有一个丰富
的逻辑连接。要看到这一点,我们需要观察MSL的对象带有两个内置的前
序。第一个是众所周知的偏序,定义为
x
≤
y
惠
x=xy
,第二个是等式。在下文
中,如果类型
R
表示前序或偏序,那么
MSL
的对象应该被认为具有标准偏
序,如果
R
表示等价关系或相等,那么它们应该被认为携带相等关系。函子
P
:
Set
R
→
MSL
将对象(
X
,
RX
)发送到其右
R
-
闭子集的交半格。一个子集
U
<$
X
是右
R-
闭的,如果
x
∈
U
且
xRXy
蕴涵
y
∈
U.P
(
X
,
R
X
)是按包含或相等
排序的,这取决于类型
R
。函子
S
:
MSL
→
Set
R
将交半格
A
发送给它的过滤器
集合,也是根据类型
R
按包含或相等排序。