The Royal Swedish Academy of Sciences(6)

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,

Brackettypes

Γ AtypeformationΓ [A]type

Γ q:[A]Γ BtypeΓ a:AintroΓ [a]:[A]Γ,x:A b:BΓ,x:A,y:A b=b{y/x}:BelimΓ bwhere[x]=q:B

Γ p:[A]Γ q:[A]equalityΓ p=q:[A]

Conversions

bwhere[x]=[a]

b{[x]/u}where[x]=q=β=ηb{a/x}b{q/u}

Freevariables

FV([A])=FV(A)

FV([a])=FV(a)

FV(bwhere[x]=q)=(FV(b)\{x})∪FV(q)

Substitution

[A]{t/x}=[A{t/x}]

[a]{t/x}=[a{t/x}]

(bwhere[x]=q){t/y}=b{t/y}where[x]=(q{t/y})

(providedx=yandcaptureofxintisavoided)

Compatibilityrules

A=A

a=a

b=b ∧q=q = = = [A]=[A ][a]=[a ](bwhere[x]=q)=(b where[x]=q )

Figure1:Brackettypes

5

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