The Royal Swedish Academy of Sciences(11)

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,

simplyastheidentityarrow

(Γ)[[r(t)]]=1[[Γ]](Γ)=(Γ,Eq(t,t))A

Next,wegivetheinterpretationofthe rstandthesecondprojectionfromadependentsum.Considertheterms

Γ p:x:ABΓ p:x:AB

Γ π1(p):AΓ π2(p):B{π1(p)/x}

Weinterpretπ1(p)asthecompositionofarrows

(Γ)p(Γ,A,B)Γ,A B(Γ,A)

andπ2(p)asinthefollowingdiagram:(Γ)NNN[[Nπ2(p)]]NNNNNNp

=(Γ,B{π1(p)/x})_(Γ,x:A,B)

Γ,A B

(Γ)π1(p)(Γ,A)

Thearrow[[π2(p)]]istheuniquearrowobtainedfromtheuniversalpropertyofthedisplayedpullbackdiagram.Adependentpairformedas

Γ a:AΓ,x:A BtypeΓ b:B{a/x}Γ a,b :x:AB

(Γ,A,B)

Γ,A Bisinterpretedasthecompositionofbwiththetoparrowinthediagram(Γ,B{a/x})_bΓ B{a/x}

(Γ)(Γ,A)

This completestheoutlineoftheinterpretationofdependenttypetheorywithandEqtypesina nitelycompletecategory.

Remark3.2Itiswellknownthatcertaincoherenceproblemsarisewhenweinterpretdependenttypetheoryasabove.Theproblemsarecausedbythefactthatingeneraltheresultofsuccessivepullbacksalongar-rowsg:B→Candf:A→Bisonlyisomorphictothepullbackalong

9

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