The Royal Swedish Academy of Sciences(7)

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,

Now(3)saysthats [ ]=t [ ]impliess=tforarbitrarys,t:A→B,whichmeansthat[ ]isepic.Toprove(3),observe rstthatbytheequalityrulewehave

Γ,x:A,y:A [x]=[y]:[A]

therefore

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

whichmeansthatwecanformtheterms{[x]/u}where[x]=u.Similarly,wecanformthetermt{[x]/u}where[x]=u.Nowweget

s=η(s{[x]/u}where[x]=u)=(t{[x]/u}where[x]=u)=ηt.

Thesecondequalityfollowsfromtheassumptions{[x]/u}=t{[x]/u}andthecompatibilityruleforwhereterms.

Aconsequenceof(3)isthefollowingconversion,calledexchange:bwhere[x]=(pwhere[y]=q)=(bwhere[x]=p)where[y]=q.Theruleisvalidwheny=xandy∈FV(b).By(3)itsu cestoverifytheexchangeruleforthecaseq=[z]wherez:Aisafreshvariable.Wethenget(bwhere[x]=p)where[y]=[z]=β

=

=βb{z/y}where[x]=(p{z/y})bwhere[x]=(p{z/y})bwhere[x]=(pwhere[y]=[z])

Inthesecondequalitywetookintoaccountthefactthatydoesnotoccurfreelyinb,andinthethirdequalityweappliedtheηruletothesubtermp{z/y},whichwecandobecauseofthecompatibilityrules.

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