The Royal Swedish Academy of Sciences(23)

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,

5.1=[1]

6.[A×ΓB]=[A]×Γ[B]

Moreover,(1)–(4)characterize[ ]uniquelyamongstablefunctorsonregularcategories.

Proof.Theactionof[ ]onanarrowx:A t:Bisthebottomarrowinthefollowingdiagram

x:A

[ ]tB[ ]

u:[A][t]where[x]=u[B]Theactionofthefunctor[ ]onthearrowtisnottobeconfusedwiththearrowt [ ]=[t]:A→[B],whichdoesnotevenhavethecorrectdomain.

Therestofthepropositionisprovedeasily.Bywayofexample,weprovethat[[A]]=[A].InthediagramΓ{{{{{{{{{{[[A]][A]A

thearrow[A]→[[A]]istheregularepipartofanimagefactorizationofthemono[A]→Γ,thereforeitisanisomorphism.

Letusseehowtheadjunction(2)isvalidated,foranytypeAandapropositionP,bywhichwemeanthatPsatis es(8):givenanyarrow(term)A→P,weapplythefunctor[ ]togetauniqueone[A]→[P],but

[P]=PsincePisaproposition.Conversely,given[A]→P,weprecomposewithA→[A]togetA→ P. Toseehow[ ]andinteract,considerthetypes[B]and[AA[B]] inacontextΓ,obtainedbyapplyingtheand[ ]formationrulesintwo

18

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