![](https://csdnimg.cn/release/download_crawler_static/88749188/bg5.jpg)
法医
Maietti/Electronic Notes in Theoretical Computer Science 122
(
2005
)
105
其中Cat(G)是由图G生成的自由范畴,图G定义为[10],δ
0
,
δ
1
:Cat
(G)
1
→Cat(G)
0
是
定义域和上定义域映射;
(iv)
由Con
FP
(V
,
ν
,
con
FP
)描述的一组终端锥和产品锥,其中V是产品锥和
终端锥的顶点集,ν 是态射
V
:V G
0
将锥顶点映射到图的对象,并且任何v
∈
V上的锥由下式描述:
con
FP
(
v
)
∈
(
<$
f
1
∈
G
1
<$
f
2
∈
G
1
δ
0
(
f
1
)
=
G
0
ν
(
v
)
×
δ
0
(
f
2
)
=
G
0
ν
(
v
))
<$T
注2.7在下文中,为简单起见,我们假设V P
与
con
F P
(
in
l(
p
))
<
$in
r
(
p
)
con
F P
(
in
r
(
p
))
<
$in
l(
π
a
(
p
)
,
π
b
(
p
)
,
eq
,
eq
>>
)
其中
a
(
p
)
=δ
1
(
π
a
(
p
)
)且
b
(
p
)
=δ
1
(
π
b
(
p
)
)。我们还将使用以下缩写:
v
t
inl
()和
v
p
inr
(
p
)。
我们可以通过S的图上的内部图来考虑从内部草图S到算术论域U本身的底层草
图的图态射(参见[1,5]):
定义2.8
U
中有限可判定
FP-
草图
S
(
G
,
Diag
,
Con
FP
)上的图态射,用F:
S →
U表示,是U中内部图G上的内部图(关于范畴定义,例如参见[10]),也就是
说,在
U
的内部语言中,我们可以导出依赖类型F
0
(x)
[
x
∈
G
0
]
和类型化项
F1
(
f
)(
z
)
∈
F0
(
y
)
[
f∈
G1
,
x∈
G0
,
z∈
F0
(
x
)
,
y∈
G0
,
ZJ
∈x
=
G0
δ
0
(
f
)
,
ZJJ
∈y
=
G0
δ
1
(
f
)
]
描述从草图的底层图到算术宇宙的图的图态射,以保持它们的域和余域的方式
将对象发送到对象,将箭头发送到箭头。
定义
2.9
给定
U
中的有限可判定
FP-
草图
S
(
G
,
Diag
,
Con
FP
),从图态射
F
:
S → U
到
U
中的图态射
H
:
S →
U
的自然变换
α
:
F
→
H
由项给出
α
x
(
z
)
∈
H0
(
x
)
[
x
∈
G0
,
z
∈
F0
(
x
)
]
使得我们可以证明
H1
(
f
)(
α
x
(
z
))
=
H0
(
y
)
α
y
(
F1
(
f
)(
z
))
[
x∈
G0
,
y∈
G0
,
f∈
G1
,
z∈
F0
(
x
)
,
ZJ
∈x
=
G0
δ
0
(
f
)
,
ZJJ
∈y
=
G0
δ
1
(
f
)
]
现在,我们引入算术论域U中FP-草图的模型的概念。