The Royal Swedish Academy of Sciences(9)

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,

The rstconditionstatesthatinaregularcategorywecanformquo-tientsbyequationallyde nedequivalencerelations,andthesecondconditionrequiressuchquotientstobehavewellwithrespectto nitelimits.

Letus rstrecallhowtointerpretdependenttypetheorywithdependent sumsandstrongextensionalequalityEqinacategorywith nitelimits.Weusethesemanticbracket[[X]]todenotetheinterpretationofX,whereXcouldbeatype,aterm,acontext,orajudgment.Whennoconfusioncanarise,weomitthesemanticbrackets,especiallyindiagrams,inordertoimprovereadability.Weusuallydenotetheinterpretationofacontextx1:A1,...,xn:Anas(A1,...,An)insteadof[[x1:A1,...,xn:An]].

Theemptycontextisinterpretedastheterminalobject1.Theinter-pretationofatypeinacontext

Γ Atype

isgivenintheslicecategoryC/[[Γ]]byanarrow,calledadisplaymap,

[[Γ,x:A]]

[[Γ A]]

[[Γ]]

wherewehereabbreviatedthenameofthearrow.Itsdomainistheinter-pretationofthecontextΓ,x:A.

Aterminacontext

Γ t:A

isinterpretedbyapointof(Γ,A)inthesliceC/[[Γ]]

(Γ)[[Γ t:A]]BBBBBB=B

(Γ)(Γ,A)xxxxxxΓ Axx

Inotherwords,atermΓ t:Aisinterpretedasasectionoftheinterpre-tationofΓ Atype.Normally,wewritejust[[t]]ortinsteadof[[Γ t:A]].

Weinterpretsubstitutionsofatermaforavariablex,

Γ a:AΓ,x:A Btype

Γ B{a/x}typeΓ a:AΓ,x:A t:BΓ t{a/x}:B{a/x}

7

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