The Royal Swedish Academy of Sciences(27)

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,

logicisthatthe rst-orderlogicaloperationsonthepropositionsareherede nedintermsoftheoperationsontypes,ratherthantakenasprimitive.

Inadditionto rst-orderlogic,onecanusebracketstode nesubsettypes.ForanytypeΓ,x:A Btype,theassociatedsubsettype

Γ {x:A|B}type

isde nedby

{x:A|B}= x:A[B(x)].

ThesecanbecomparedtothetoolboxforsubsettypesbySambin[SV98].Bywayofexample,weremarkthatthecategoryEquofequilogicalspaces[Sco96,BBS]isaregularlccc,andsosupportsallofthelogicaloperationsconsideredabove.ForX∈Equ,thebracketofanX-indexedfamilyofequilogicalspaces

(Ex)x∈X

isofcoursetheregularepi–monoimagefactorizationofthecorrespondingdisplaymap

p:E→X.

Thedomainoftheimage[E] Xisconstructedfromthesameunderlyingspace|E|asE=(|E|,～E),butwiththenewequivalencerelation,givenby

e～[E]e pe=pe .

ThefactthatEquhasthismuchinternallogicwithoutbeingatopos,orevenapretopos,wastheoriginalobservationfromwhichthepresentworkgrew[BBS].

6FirstOrderLogicvs.Propositions-as-Types

Asanapplicationofbrackettypes,wecancomparetheconventionalinter-pretationof rst-orderlogicwiththepropositions-as-typesinterpretation,andrelate rst-orderprovabilitytoprovabilityindependenttypetheory(withoutbrackets).

Supposewehaveasingle-sorted rst-ordertheoryT,consistingofcon-stants,functionandrelationletters,andaxiomsgivenasclosedformulas.Thestandardpropositions-as-typesinterpretation ofTintotypetheory,

TDTT(14)

isdeterminedby xingtheinterpretationsofthebasicsort,theconstants,functionandrelationsymbols.Therestoftheinterpretationisdetermined

21

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