The Royal Swedish Academy of Sciences(10)

Image factorizations in regular categories are stable under pullbacks, so they model a natural modal operator in dependent type theory. This unary type constructor [A] has turned up previously in a syntactic form as a way of erasing computational content,

asindicatedinthefollowingpullbackdiagram:

(Γ)(Γ,x:A)MMMIIIIMMMII[[t{a/x}]]MMMtIIMMMIIIIMMMIIMMM(Γ,x:A,B)[[Γ,B{a/x}]]_=

[[Γ B{a/x}]]Γ,x:A Ba(Γ)(Γ,A)

Theinterpretationofadependentsumformedas

Γ,x:A BtypeΓ x:ABtype

isthecompositionofthearrows

(Γ,A,B)

Γ,A B

(Γ,A)

Γ AΓ AB

(Γ)

Thisgivesusaconnectionbetweentheinterpretationofcontexts andde-pendentsums,becauseitmustbethecasethat[[Γ,A,B]]=[[Γ,x:AB]].

Theinterpretationofanequalitytypeformedas

Γ s:AΓ t:A

Γ EqA(s,t)type

istheequalizerofsandt,asinthefollowingdiagram:

(Γ,EqA(s,t))[[Γ EqA(s,t)]](Γ)s

t(Γ,A)

Whensandtarethesameterm,theequalizeristrivialandwehave

[[Γ,EqA(t,t)]]=[[Γ]]

Fromthisweobtaintheinterpretationofa‘re exivity’term

Γ t:A

Γ r(t):EqA(t,t)

8

搜索“diyifanwen.net”或“第一范文网”即可找到本站免费阅读全部范文。收藏本站方便下次阅读，第一范文网，提供最新人文社科The Royal Swedish Academy of Sciences(10)全文阅读和word下载服务。