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,
Propositionsas[Types]
SteveAwodey AndrejBauer
InstitutMittag-Le er
TheRoyalSwedishAcademyofSciences
June2001
Abstract
Imagefactorizationsinregularcategoriesarestableunderpull-backs,sotheymodelanaturalmodaloperatorindependenttypethe-ory.Thisunarytypeconstructor[A]hasturneduppreviouslyinasyntacticformasawayoferasingcomputationalcontent,andformal-izinganotionofproofirrelevance.Indeed,semantically,thenotionofasupportissometimesusedassurrogatepropositionassertinginhab-itationofanindexedfamily.
Wegiverulesforbrackettypesindependenttypetheoryandpro-videcompletesemanticsusingregularcategories.Weshowthatdepen-denttypetheorywiththeunittype,strongextensionalequalitytypes,strongdependentsums,andbrackettypesistheinternaltypetheoryofregularcategories,inthesamewaythattheusualdependenttypetheorywithdependentsumsandproductsistheinternaltypetheoryoflocallycartesianclosedcategories.
Wealsoshowhowtointerpret rst-orderlogicintypetheorywithbrackets,andwemakeuseofthetranslationtocomparetypetheorywithlogic.Speci cally,weshowthatthepropositions-as-typesinter-pretationiscompletewithrespecttoacertainfragmentofintuitionistic rst-orderlogic.Asaconsequence,amodi eddouble-negationtrans-lationintotypetheory(withoutbrackettypes)iscompleteforallofclassical rst-orderlogic.
MSC2000Classi cation:03G30,03B15,18C50
Keywords:categoricallogic,typetheory,regularcategories,brackettypesDepartmentofPhilosophy,CarnegieMellonUniversity,Pittsburgh,USA,e-mail:awodey@cmu.edu
IMFM&DepartmentofMathematics,UniversityinLjubljana,Slovenia,e-mail:Andrej.Bauer@
1
搜索“diyifanwen.net”或“第一范文网”即可找到本站免费阅读全部范文。收藏本站方便下次阅读,第一范文网,提供最新人文社科The Royal Swedish Academy of Sciences全文阅读和word下载服务。
相关推荐: