The Royal Swedish Academy of Sciences(15)

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,

Sincepandqaresectionsofthemono[[Γ [A]]]theymustbeequal.Next,considertheβ-rule

bwhere[x]=[a]

Therelevantdiagramis

JJJJJJJ[ ](bwhereJbJJJJ(Γ,A,B)(Γ,[A])=βb{a/x}.(Γ,A)a(Γ)[x]=[a])

Thearrowistheuniquefactorizationofbthrough[ ].Byconstruction,thelower-lefttrianglecommutes,andtheright-handarrowisde nedtobethecomposition [ ] a,whichimpliesthattheupper-righttrianglecommutes.Thisispreciselywhattheβ-rulestates.

Toverifytheη-rule

b{[x]/u}where[x]=q

weconsiderthefollowingdiagram:

(Γ,x:A)[ ]=ηb{q/u}

KKKKKKKKKb{[x]/u}KKKK(Γ,u:[A])bq

(Γ,A,B)wwwwwwwww(b{[x]/u}wwww(Γ)where[x]=q)

Thearrowb{[x]/u}isthecompositionof[ ]andb.Thereisauniquefactorizationofb{[x]/u}through[ ],andtheinterpretationofb{[x]/u}where[x]=qisthecomposition q.Butb{[x]/u}alsofactorsthrough[ ]viab,soitmustbethat=b.Nowtheη-rulefollows,becausethearrowb qistheinterpretationofb{q/u}.

Thesubstitutionrulesarevalidbecausetheregularepi–monofactoriza-tionsarestableunderpullbacks.Thecompatibilityrulesarevalidsimplybecauseweinterpretedthebrackettypesandtermsbywellde nedcategor-icaloperations(whichthereforepreserveequality).

Theorem3.4Thesemanticsofbrackettypesinregularcategoriesiscom-plete.

12

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