The Royal Swedish Academy of Sciences(14)

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,

Theregularepipartofthefactorizationisusedintheinterpretationoftermbracketing

Γ a:A

Γ [a]:[A]

Theinterpretationof[a]isthecomposition

(Γ)a(Γ,A)[ ](Γ,[A])

Itremainstointerpretthewhereterms.Consider

Γ q:[A]Γ,x:A b:BΓ,x:A,y:A b=b{y/x}:B

Γ bwhere[x]=q:B

Thevarioustermsandtypesoccurringaboveareinterpretedinthesliceover[[Γ]],asshowninthefollowingdiagram:

(Γ,x:A,y:A)x[ ](Γ,[A])q(Γ)(Γ,A)IIwIIwwIIwwIIwwIwbIIIw(bwhere[x]=q)Iwww

(Γ,A,B)

Byassumption,thearrowlabelledbcoequalizesthetwoprojections.Theregularepi[ ]isthecoequalizerofthosetwoprojections,thereforeΓ bfactorsuniquelythrough[ ]via.Theinterpretationof(bwhere[x]=q)isthecomposition q.

Theorem3.3Theinterpretationofbrackettypesinregularcategoriesissound.

Proof.Weomittheroutineproofofsoundnessoftheinterpretationofdependentsumsandequalitytypes,andconcentrateontheinterpretationofbrackettypes.Weneedtoverifytheequalityrule,twoconversionrules,thesubstitutionrulesandthecompatibilityrules.

Whentheequalityruleistranslatedintothesemantics,itstatesthatthearrowspandqinthefollowingdiagramareequal:

(Γ)(Γ,[A])EEEEEEEΓ [A]=EEEEEEp

(Γ)

11

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