The Royal Swedish Academy of Sciences(5)

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,

IfPandQarepropositionsinthissense,thenclearlysoare

1,P×Q,P→Q,x:AP

whereinthelastexpressionPmaydependonanarbitrarytypeA.Inlogicalterms,thismeansthatpropositionsarealreadyclosedunderthefollowinglogicaloperations:

T,P∧Q,P= Q, x:A.P.

InSection5wewillseehowtode netheremaining rst-orderlogicaloper-ations.

Becauseofproofirrelevance,ifapropositionPisinhabited,thenitissobypreciselyoneterm(uptoextensionalequality).Thus,atypingjudgment

Γ p:P

islikeastatementofP’struth,

Γ Ptrue

aspdoesnotplayanyroleotherthanuniquelywitnessingthefactthatPholds.

Weintroduceanewtypeconstructor[ ]whichassociatestoeachtypeAaproposition[A],calledtheassociatedpropositionofA.TheaxiomsgiveninFigure1weredesignedwiththefollowingadjunctioninmind,foranytypeAandpropositionP:

x:A p:P

x :[A] p :P(2)

ingtherulesprovidedinFigure1,wecantakep =(pwhere[x]=x ),sincetheequalityconditiononp:Pforeliminationissatis edbyproofirrelevance(1).Seeremark5inSection7forconsiderationofalternateformulationsofbrackettypes.

Asanexample,letusshowthatthetermformingoperation[ ]is‘epic’inthefollowingsense:

Γ,x:A s{[x]/u}=t{[x]/u}:B

Γ,u:[A] s=t:B(3)

IfwethinkofatermΓ,x:A r:BasanarrowA→BintheslicecategoryoverΓ,aswewillinSection3,thenwehavethefollowingsituationoverΓ:

A[ ][A]s

tB

4

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