The Royal Swedish Academy of Sciences(22)

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,

Theouterrectangleandthelowersquareareobviouslypullbacks,hencetheuppersquareisaswell.

Wecanexpresstheregularepi–monofactorizationofanarrowx:A t:Bas

At

DDDDqDDBzzzzzzm

Im(t)

with

Im(t)

m

e=== y:B[x:AEqA(t,y)]z:Im(t) π1(z):Bx:A t,[ x,r(t) ] :Im(t).

4PropertiesofBracketTypes

Asaconsequenceofthecompletesemanticsoftheprevioussectionwecanprovefactsaboutbrackettypesbyarguinginageneralregularcategory.Thusweidentifytypeswithobjectsandtermsincontextswitharrows.Weusethistechniqueinthepresentsectiontoestablishsomeofthebasicpropertiesofbrackettypes.

Firstobservethat,inanycontextΓ,thetypessatisfyingproofirrele-vance(1),areexactlythecartesianidempotents:

Pprop P=P×ΓP(8)

wherehereandinwhatfollows,=betweentypesmeansthattheyarecanon-icallyisomorphic.Forexample,in(8)thecanonicalisomorphismsarethediagonalandtheprojection.IfPandQarepropositionsinthecontextΓthenthecorrespondingdisplaymaps(Γ,P)→(Γ)and(Γ,Q)→(Γ)aremonos,sothatwecanthinkofPandQassubobjectsofΓ.Inparticular,wecanwriteP≤Qwhenthereexistsa(necessarilyunique)arrowP→QinthesliceoverΓ.

Proposition4.1ForanytypesA,BinacontextΓ:

1.[ ]isfunctorial

2.ThereisacanonicalarrowA→[A],naturalinA

3.[[A]]=[A]

4.A=[A] A=A×ΓA

17

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