The Royal Swedish Academy of Sciences(18)

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,

andfromthatthefactorizationofhthroughtheequalizer:

z:C h,r(s{h/x}) :x:AEqB(s,t)

Thisarrowisuniquebecauseanytwotermsofa(strongextensional)Eqtypeareequal.Therefore,Shasall nitelimits.

ItremainstoshowthatShasstablecoequalizersofkernelpairs.Beforeproceedingwith theproof,letusspellouttheinterpretationofdependenttypeswith1,andEqinS.

Dependentcontextsareinterpretedbynesteddependentsums

[[1]]=1 [[x1:A1,...,xn:An]]=x1:A1x2:A2···xn 1:An 1An

Inordertokeepthenotationsimplewedenotesuchanestedsumby(A1,...,An).Atypeinacontext,Γ Atype,isinterpretedbyasuit-abledisplaymap

(Γ,A)

Γ A

(Γ)

Moreprecisely,ifΓisy1:B1,...,yn:Bn,thenthedisplaymapΓ Aistheterm

n 1p:(B1,...,Bn,A) π1(p),π1(π2(p)),...,π1(π2(p)) :(B1,...,Bn).Withthisnotation,wegetagoodmatchbetweenthesyntaxofdependenttypesandtheirinterpretationinS.Forexample,adependentsuminadependentcontext

Γ,x:A BtypeΓ x:AB

isinterpretedessentially“byitself”asthearrow

(Γ, x:AB)Γ x:AB(Γ)

Similarly,anequalitytypeinadependentcontextisinterpretedessentiallybyitself,exceptthatwemustformthenesteddependentsumsinordertointerpretthedependentcontextinwhichthetypeisplaced.

Consideranarrowx:A t:BinS.Wecanformthedependenttype

y:B x:AEqB(t,y)type

14

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