The Royal Swedish Academy of Sciences

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

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,

Acknowledgement.WegratefullyacknowledgethesupportoftheIn-stitutMittag-Le er,theRoyalSwedishAcademyofSciences,wherethisresearchwasconducted.WealsothankPeterAczel,LarsBirkedal,ThierryCoquand,NicolaGambino,MilliMaietti,PerMartin-L¨of,GrigoriMints,ErikPalmgren,FrankPfenning,DanaScott,andAntonSetzerfortheircontributions.ThisworkispartoftheLogicofTypesandComputationprojectatCarnegieMellonUniversityunderthedirectionofDanaScott.1Introduction

Accordingtooneconceptionofthetheoryoftypes,propositionsandtypesareidenti ed:

Propositions=Types.

Thisideaiswell-knownundertheslogan“Propositionsastypes”,andhasbeendevelopedbyMartin-L¨of[ML84]andothers[How80,Tai].Inthisre-portwedistinguishpropositionsandtypes,butstaywithinatype-theoreticframework.Weregardsometypestobepropositions,butnotnecessarilyallofthem.Additionally,eachtypeAhasanassociatedproposition[A].Thisgivesusacorrespondence

PropositionsTypes

[ ]

whichisinfactanadjunction.Sinceitwillturnoutthat[P]=PforanypropositionP,thepropositionsareexactlythetypesintheimageofthebracketconstructor[ ].Wecallthesetypes[A]thebrackettypes.Thepictureisthensimply

Propositions=[Types].

Theseideasarenotnew.OurworkoriginatedwithFrankPfenning’sbrackettypesforerasingcomputationalcontent[Pfe01].Speakingsomewhatvaguely,theideaistouseabrackettypeforhidingcomputationalcontentofatype.Asasimpleexample,considerthecomputationalcontentofatermpoftype

n:Nm:NEq(2m,n)+m:NEq(2m+1,n).

Givenanaturalnumbern,thenpn= i,m ,wherei∈{0,1}andm∈N,suchthatn=2m+i.Bybracketingthetwodependentsums,weobtainthetype

.n:Nm:NEq(2m,n)+m:NEq(2m+1,n)

2

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,

Atermqofthistypehidestheinformationthatisprovidedbythedependentsumssothatqniseither0or1,dependingonwhethernisevenorodd.Intheextremecase,atermroftype n:Nm:NEq(2m,n)+m:NEq(2m+1,n)

doesnotcarryanycomputationalcontentatall—itjustwitnessesthefactthateverynumberisevenorodd.

ThebrackettypeswhichweconsiderareessentiallythesameasthemonotypesofMaietti[Mai98],inasuitablesetting.Palmgren[Pal01]formulatedaBHKinterpretationofintuitionisticlogicandusedimagefactorizations,whichareusedinthesemanticsofourbrackettypes,torelatetheBHKinterpretationtothestandardcategory-theoreticinterpretationofproposi-tionsassubobjects.AczelandGambino[AG01]havepromotedwhattheycalllogic-enrichedtypetheoryinwhichtheyseparatethelogicfromtypethe-ory.Thebrackettypescanbeusedtotranslatetheprimitivelogicbackintotypetheory(theusualtranslationof“propositionsastypes”worksaswell).AlreadyinhisDialecticaarticle,Lawvere[Law69]proposedacategoricaltreatmentofprooftheorythatiscloselyrelatedtobrackettypes.

Thereportisorganizedasfollows.InSection2weintroducethebrackettypes.InSection3wegivethesemanticsofbrackettypesinregularcat-egories,andproveitssoundnessandcompleteness.InSection4westudysomepropertiesofbrackettypes.InSection5weshowhowbrackettypesareusedinconjunctionwithotherdependenttypestode nethelogicalconnectivesandquanti erswithintypetheory.InSection6weusebrackettypestocomparetwointerpretationsoflogic:thestandard“propositionsastypes”interpretation,andtheusual rst-orderone.

2BracketTypes

WeconsideraMartin-L¨ofstyledependenttypetheory[ML84,ML98].Fortheformulationofbrackettypeswedonotneeddependentsumsorproducts,butwesometimesassumethattheyarepresentinthetypetheory.Weworkinatypetheorywithstrongandextensionalequalityandstrongdependentsums,cf.[Jac99].Forreference,welisttherulesinAppendixA.

Amongthetypes,therearesomethatsatisfythefollowingconditionof“proofirrelevance”:

Γ PtypeΓ q:P

Γ p=q:PΓ p:P(1)

Inwords,thismeansthatanytwotermspandqofsuchatypePare(extensionally)equal.Wecallthetypessatisfyingproofirrelevanceproposi-tions.TheywerecalledmonotypesbyMaietti[Mai98],andthereareotherequivalentformulations.

3

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,

IfPandQarepropositionsinthissense,thenclearlysoare

1,P×Q,P→Q,x:AP

whereinthelastexpressionPmaydependonanarbitrarytypeA.Inlogicalterms,thismeansthatpropositionsarealreadyclosedunderthefollowinglogicaloperations:

T,P∧Q,P= Q, x:A.P.

InSection5wewillseehowtode netheremaining rst-orderlogicaloper-ations.

Becauseofproofirrelevance,ifapropositionPisinhabited,thenitissobypreciselyoneterm(uptoextensionalequality).Thus,atypingjudgment

Γ p:P

islikeastatementofP’struth,

Γ Ptrue

aspdoesnotplayanyroleotherthanuniquelywitnessingthefactthatPholds.

Weintroduceanewtypeconstructor[ ]whichassociatestoeachtypeAaproposition[A],calledtheassociatedpropositionofA.TheaxiomsgiveninFigure1weredesignedwiththefollowingadjunctioninmind,foranytypeAandpropositionP:

x:A p:P

x :[A] p :P(2)

ingtherulesprovidedinFigure1,wecantakep =(pwhere[x]=x ),sincetheequalityconditiononp:Pforeliminationissatis edbyproofirrelevance(1).Seeremark5inSection7forconsiderationofalternateformulationsofbrackettypes.

Asanexample,letusshowthatthetermformingoperation[ ]is‘epic’inthefollowingsense:

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

Γ,u:[A] s=t:B(3)

IfwethinkofatermΓ,x:A r:BasanarrowA→BintheslicecategoryoverΓ,aswewillinSection3,thenwehavethefollowingsituationoverΓ:

A[ ][A]s

tB

4

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

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.

3CategoricalSemanticsofBracketTypes

Inthissectionwepresentasemanticsforbrackettypesinregularcategories,seee.g.[Bor94]forthelatter.TherulesinFigure1aresoundandcompleteforsuchsemantics.

De nition3.1AregularcategoryCisacategorywith nitelimitsinwhich

1.everykernelpairhasacoequalizer,and

2.thepullbackofaregularepimorphismisaregularepimorphism.

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,

The rstconditionstatesthatinaregularcategorywecanformquo-tientsbyequationallyde nedequivalencerelations,andthesecondconditionrequiressuchquotientstobehavewellwithrespectto nitelimits.

Letus rstrecallhowtointerpretdependenttypetheorywithdependent sumsandstrongextensionalequalityEqinacategorywith nitelimits.Weusethesemanticbracket[[X]]todenotetheinterpretationofX,whereXcouldbeatype,aterm,acontext,orajudgment.Whennoconfusioncanarise,weomitthesemanticbrackets,especiallyindiagrams,inordertoimprovereadability.Weusuallydenotetheinterpretationofacontextx1:A1,...,xn:Anas(A1,...,An)insteadof[[x1:A1,...,xn:An]].

Theemptycontextisinterpretedastheterminalobject1.Theinter-pretationofatypeinacontext

Γ Atype

isgivenintheslicecategoryC/[[Γ]]byanarrow,calledadisplaymap,

[[Γ,x:A]]

[[Γ A]]

[[Γ]]

wherewehereabbreviatedthenameofthearrow.Itsdomainistheinter-pretationofthecontextΓ,x:A.

Aterminacontext

Γ t:A

isinterpretedbyapointof(Γ,A)inthesliceC/[[Γ]]

(Γ)[[Γ t:A]]BBBBBB=B

(Γ)(Γ,A)xxxxxxΓ Axx

Inotherwords,atermΓ t:Aisinterpretedasasectionoftheinterpre-tationofΓ Atype.Normally,wewritejust[[t]]ortinsteadof[[Γ t:A]].

Weinterpretsubstitutionsofatermaforavariablex,

Γ a:AΓ,x:A Btype

Γ B{a/x}typeΓ a:AΓ,x:A t:BΓ t{a/x}:B{a/x}

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,

asindicatedinthefollowingpullbackdiagram:

(Γ)(Γ,x:A)MMMIIIIMMMII[[t{a/x}]]MMMtIIMMMIIIIMMMIIMMM(Γ,x:A,B)[[Γ,B{a/x}]]_=

[[Γ B{a/x}]]Γ,x:A Ba(Γ)(Γ,A)

Theinterpretationofadependentsumformedas

Γ,x:A BtypeΓ x:ABtype

isthecompositionofthearrows

(Γ,A,B)

Γ,A B

(Γ,A)

Γ AΓ AB

(Γ)

Thisgivesusaconnectionbetweentheinterpretationofcontexts andde-pendentsums,becauseitmustbethecasethat[[Γ,A,B]]=[[Γ,x:AB]].

Theinterpretationofanequalitytypeformedas

Γ s:AΓ t:A

Γ EqA(s,t)type

istheequalizerofsandt,asinthefollowingdiagram:

(Γ,EqA(s,t))[[Γ EqA(s,t)]](Γ)s

t(Γ,A)

Whensandtarethesameterm,theequalizeristrivialandwehave

[[Γ,EqA(t,t)]]=[[Γ]]

Fromthisweobtaintheinterpretationofa‘re exivity’term

Γ t:A

Γ r(t):EqA(t,t)

8

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

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,

thecompositiong f,whereasforacompletelywater-tightinterpretationequalityisrequired.

Thereareseveralstandardwaysofresolvingthisproblem,mostnotablybyinterpretingthetypetheoryinasuitable beredcategory[Jac99],andthenapplyingtechnicalresultspertainingtothese[Hof95].Wedonotwishtoobscuremattersbyemployingsuchtechnicaldevices.Theinterestedreadermayeithertranslateourpresentationintoasuitable beredsetting,orassumesomeotherremedy,suchasmakingacoherentchoiceofpullbacks.(ForthesyntacticcategoryinSection3,suchpullbackscanbechosensimplyassubstitutions.)

Wenowproceedwiththeinterpretationofbrackettypes.AregularcategoryChasstableregularepi–monoimagefactorizations.Everyarrowf:A→Bcanbefactoreduniquelyuptoisomorphismasaregularepifollowedbyamono

Af

EEEEEEByyyyyy

Im(f)

Thefactorizationisobtainedbytakingthecoequalizerqofthekernelpair(π1,π2)off,asinthefollowingdiagram:

A×BAπ1

2ADDDDqDDfBzzzzzzi

Im(f)

Thearrowi:Im(f)→Bexistsandisuniquewithi q=fbecausefcoequalizesitsownkernelpair.Itcanmoreoverbeshownthatiisalwaysmonic.

Abrackettype

Γ Atype

Γ [A]type

isinterpretedastheimageof[[Γ A]]:

(Γ,A)[[Γ,[A]]]=Im(Γ A)OOOOOOOOOO[[Γ [A]]]Γ AOOOOOOO[ ](Γ)

10

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,

Theregularepipartofthefactorizationisusedintheinterpretationoftermbracketing

Γ a:A

Γ [a]:[A]

Theinterpretationof[a]isthecomposition

(Γ)a(Γ,A)[ ](Γ,[A])

Itremainstointerpretthewhereterms.Consider

Γ q:[A]Γ,x:A b:BΓ,x:A,y:A b=b{y/x}:B

Γ bwhere[x]=q:B

Thevarioustermsandtypesoccurringaboveareinterpretedinthesliceover[[Γ]],asshowninthefollowingdiagram:

(Γ,x:A,y:A)x[ ](Γ,[A])q(Γ)(Γ,A)IIwIIwwIIwwIIwwIwbIIIw(bwhere[x]=q)Iwww

(Γ,A,B)

Byassumption,thearrowlabelledbcoequalizesthetwoprojections.Theregularepi[ ]isthecoequalizerofthosetwoprojections,thereforeΓ bfactorsuniquelythrough[ ]via.Theinterpretationof(bwhere[x]=q)isthecomposition q.

Theorem3.3Theinterpretationofbrackettypesinregularcategoriesissound.

Proof.Weomittheroutineproofofsoundnessoftheinterpretationofdependentsumsandequalitytypes,andconcentrateontheinterpretationofbrackettypes.Weneedtoverifytheequalityrule,twoconversionrules,thesubstitutionrulesandthecompatibilityrules.

Whentheequalityruleistranslatedintothesemantics,itstatesthatthearrowspandqinthefollowingdiagramareequal:

(Γ)(Γ,[A])EEEEEEEΓ [A]=EEEEEEp

(Γ)

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,

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

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,

Proof.Inordertoprovethetheoremwe buildasyntacticcategorySfromthedependenttypetheoryDwith1,,Eq,and[ ]types.WethenshowthatSisaregularcategory,andthattheinterpretationofDinSvalidatespreciselyalltheprovableequationsbetweenterms.

TheobjectsofSaretheclosedtypesofD.ThearrowsfromaclosedtypeAtoaclosedtypeBarerepresentedbyterms

x:A t:B

wheretwosuchtermssandtrepresentthesamearrowif,andonlyif,Dprovesthattheyareequalx:A s=t:B(sinceweareworkingwithextensionalequalityitdoesnotmatterwhichsenseof‘equal’wetake).Furthermore,twotermsinacontextwillbeconsideredequalifwecanobtainonefromtheotherbyrenamingboundandfreevariablesinacapture-avoidingway.

Thecompositionofarrowsx:A t:Bandy:B s:Cisthearrowx:A s{t/y}.Thatcompositioniswell-de nedandassociativefollowsfromthepropertiesofsubstitution.TheidentityarrowonAisrepresentedbyx:A x:A.

Sincetermsrepresentingthesamearrowmustbeprovablyequal,itsuf- cestoshowthatSisregular.Letusprove rstthatithas nitelimits.Theterminalobjectis1.Indeed,foranytypeAwehaveanarrowx:A :1,andforanyotherarrowx:A t:1wehavex:A t= :1bytheequalityaxiomfortheunittype.Itisfairlyeasytoverify thatShasbinaryproducts:theproductofAandBisthetypeA×B=x:AB.

Theequalizerofarrowsx:A s:Bandx:A t:Bisconstructedasfollows:

x:AEqB(s,t)π1AstB

Provingthatthearrowπ1equalizessandtamountstoprovingthat

v:x:AEqB(s,t) s{π1(v)/x}=t{π1(v)/x}.

Thisfollowsfromtheextensionalityofequalitysinceπ2(v)isatermoftype

EqB(s{π1(v)/x},t{π1(v)/x}).

Supposez:C h:Aequalizessandt:

z:C s{h/x}=t{h/x}:B

Thenwecanformthetermwitnessingtheequality

z:C r(s{h/x}):EqB(s{h/x},t{h/x})

13

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,

andfromthatthefactorizationofhthroughtheequalizer:

z:C h,r(s{h/x}) :x:AEqB(s,t)

Thisarrowisuniquebecauseanytwotermsofa(strongextensional)Eqtypeareequal.Therefore,Shasall nitelimits.

ItremainstoshowthatShasstablecoequalizersofkernelpairs.Beforeproceedingwith theproof,letusspellouttheinterpretationofdependenttypeswith1,andEqinS.

Dependentcontextsareinterpretedbynesteddependentsums

[[1]]=1 [[x1:A1,...,xn:An]]=x1:A1x2:A2···xn 1:An 1An

Inordertokeepthenotationsimplewedenotesuchanestedsumby(A1,...,An).Atypeinacontext,Γ Atype,isinterpretedbyasuit-abledisplaymap

(Γ,A)

Γ A

(Γ)

Moreprecisely,ifΓisy1:B1,...,yn:Bn,thenthedisplaymapΓ Aistheterm

n 1p:(B1,...,Bn,A) π1(p),π1(π2(p)),...,π1(π2(p)) :(B1,...,Bn).Withthisnotation,wegetagoodmatchbetweenthesyntaxofdependenttypesandtheirinterpretationinS.Forexample,adependentsuminadependentcontext

Γ,x:A BtypeΓ x:AB

isinterpretedessentially“byitself”asthearrow

(Γ, x:AB)Γ x:AB(Γ)

Similarly,anequalitytypeinadependentcontextisinterpretedessentiallybyitself,exceptthatwemustformthenesteddependentsumsinordertointerpretthedependentcontextinwhichthetypeisplaced.

Consideranarrowx:A t:BinS.Wecanformthedependenttype

y:B x:AEqB(t,y)type

14

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,

andre-interpretitinS.Itsinterpretationisthedisplaymap

p:y:Bx:AEqB(t,y) π1(p):B

ThisdisplaymapisisomorphicinS/Btothearrow x:A t:Bthatwestartedwith.Indeed,Aisisomorphictoy:Bx:AEqB(t,y)viatheisomorphisms

x:A t, x,r(t) :y:Bx:AEqB(t,y)

and

p: y:B x:AEqB(t,y) π1(π2(p)):A

Itiseasytocheckthatthesetwoisomorphismscommutewiththearrowstandπ1.ThisshowsthateveryarrowinSisisomorphictotheinterpretationofadependenttypeinacontextoftheformz:C Dtype.Thus,inordertoshowthatShascoequalizersofkernelpairs,weonlyneedto ndthecoequalizersofthekernelpairsofarrowsthatareinterpretationsofsuchtypes,namelythoseoftheform

p:z:CD π1(p):C(4)

Becauseanyp:z:CDcanbewrittenuniquelyasapair z,w withz:C

andw:D,weshallwrite(4)morereadablyas

z:C,w:D z:C(5)

Thiswayweavoidtheuseofnestedprojectionslateron,whenwehavetodealwithnesteddependentsums.Thekernelpairof(5)iseasilyseentobe

(z:C,v:D,w:D) z,v

z,w (C,D)(6)

Wecangetitscoequalizerbyapplyingbrackettypes:

(z:C,v:D,w:D) z,v

z,w (z:C,u:D) z,[u] (C,[D])(7)

Indeed, z,[u] coequalizesthekernelpairbytheequalityruleforbrackettypes:

z:C,v:D,w:D [v]:[D]z:C,v:D,w:D [w]:[D]

z:C,v:D,w:D [v]=[w]:[D]

Toseethatitisthecoequalizer,supposewehaveanarrow

z:C,u:D t:B

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,

thatcoequalizesthekernelpair,whichmeansthat

z:C,v:D,w:D t{v/u}=t{w/u}:B

Thenwecanformthefactorizationoftthrough[u]asthewhereterm

z:C,y:[D] twhere[u]=y:B

Thesituationisdepictedinthefollowingdiagram:

(z:C,v:D,w:D) z,v

z,w (z:C,u:D)NNNNNNNN z,[u] NNNt

(C,y:[D])(B)ttttttt(tttwhere[u]=y)

Thetrianglecommutesbecause

twhere[u]=[u]=t

bytheβ-ruleforbrackettypes.Thefactorizationisunique,because[ ]isepic,stly,letusshowthatinSregularepisarestableunderpullbacks.SinceeveryarrowinSisisomorphictooneoftheform(5),everykernelpairisisomorphictooneoftheform(6)andsoeveryregularepiisisomorphictooneoftheform(7).Letusthencompute,withoutlossofgenerality,apullbackofsuchacoequalizeralonganarrowoftheform(5):

(y:B,z:C,u:D)_

y,z,[u] z,u (z:C,u:D) z,[u]

(y:B,z:C,v:[D]) z,v (C,[D])

Itisevidentthattheleft-handarrowisaregularepi,becauseitisoftheform(7).Itisalsoclearthatthediagramcommutes.Toseethatitisapull-back,observethatitappearsastheupperhalfofthefollowingcommutativediagram:

(y:B,z:C,u:D) y,z,[u] z,u (z:C,u:D) z,[u]

(y:B,z:C,v:[D])

y,z z,v (z:C,[D])z

(B,z:C)

16(C)

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,

Theouterrectangleandthelowersquareareobviouslypullbacks,hencetheuppersquareisaswell.

Wecanexpresstheregularepi–monofactorizationofanarrowx:A t:Bas

At

DDDDqDDBzzzzzzm

Im(t)

with

Im(t)

m

e=== y:B[x:AEqA(t,y)]z:Im(t) π1(z):Bx:A t,[ x,r(t) ] :Im(t).

4PropertiesofBracketTypes

Asaconsequenceofthecompletesemanticsoftheprevioussectionwecanprovefactsaboutbrackettypesbyarguinginageneralregularcategory.Thusweidentifytypeswithobjectsandtermsincontextswitharrows.Weusethistechniqueinthepresentsectiontoestablishsomeofthebasicpropertiesofbrackettypes.

Firstobservethat,inanycontextΓ,thetypessatisfyingproofirrele-vance(1),areexactlythecartesianidempotents:

Pprop P=P×ΓP(8)

wherehereandinwhatfollows,=betweentypesmeansthattheyarecanon-icallyisomorphic.Forexample,in(8)thecanonicalisomorphismsarethediagonalandtheprojection.IfPandQarepropositionsinthecontextΓthenthecorrespondingdisplaymaps(Γ,P)→(Γ)and(Γ,Q)→(Γ)aremonos,sothatwecanthinkofPandQassubobjectsofΓ.Inparticular,wecanwriteP≤Qwhenthereexistsa(necessarilyunique)arrowP→QinthesliceoverΓ.

Proposition4.1ForanytypesA,BinacontextΓ:

1.[ ]isfunctorial

2.ThereisacanonicalarrowA→[A],naturalinA

3.[[A]]=[A]

4.A=[A] A=A×ΓA

17

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,

5.1=[1]

6.[A×ΓB]=[A]×Γ[B]

Moreover,(1)–(4)characterize[ ]uniquelyamongstablefunctorsonregularcategories.

Proof.Theactionof[ ]onanarrowx:A t:Bisthebottomarrowinthefollowingdiagram

x:A

[ ]tB[ ]

u:[A][t]where[x]=u[B]Theactionofthefunctor[ ]onthearrowtisnottobeconfusedwiththearrowt [ ]=[t]:A→[B],whichdoesnotevenhavethecorrectdomain.

Therestofthepropositionisprovedeasily.Bywayofexample,weprovethat[[A]]=[A].InthediagramΓ{{{{{{{{{{[[A]][A]A

thearrow[A]→[[A]]istheregularepipartofanimagefactorizationofthemono[A]→Γ,thereforeitisanisomorphism.

Letusseehowtheadjunction(2)isvalidated,foranytypeAandapropositionP,bywhichwemeanthatPsatis es(8):givenanyarrow(term)A→P,weapplythefunctor[ ]togetauniqueone[A]→[P],but

[P]=PsincePisaproposition.Conversely,given[A]→P,weprecomposewithA→[A]togetA→ P. Toseehow[ ]andinteract,considerthetypes[B]and[AA[B]] inacontextΓ,obtainedbyapplyingtheand[ ]formationrulesintwo

18

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,

di erentorders,asindicatedinthefollowingdiagram.

(Γ,[(Γ,A,B)AB])<<<<<<<<<<<< <<AB [AB]<<(Γ,A,[B])MMM<<MMM<MMM<<<MMM<< MMM<<[B]AMMM< (Γ)(Γ,[[B]])A[A[B]]

Sincethetwowaysaroundthediagramfrom(Γ,A,B)to(Γ)arebothregularepi–monofactorizationsofthesamearrow,byuniquenessofimageswehave:

[A[B]]=[AB]

ForequalitytypesEqA,theeliminationrule,

Γ e:EqA(a,b)

Γ e=r(a):EqA(a,b)

impliesthat(EqA(a,b))2=EqA(a,b),whence:

[EqA(a,b)]=EqA(a,b).

Togetherwith[1]=1,thatsummarizesthepropertiesof[ ]onitsown.Thingsbecomemoreinterestinginthepresenceofothertype-formingoperations,

0,A+B,AB,A→B,¬A,

where¬AstandsforA→0.

For nitesumsweget

[0]=0,[A+B]=[[A]+[B]].

byanargumentsimilartothatfor. Forwehave(A[B])2=A[B]2=A[B],sothat

[A[B]]=A[B],

andoneseeseasilythat

[AB]≤A[B].

19(9)

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,

WhenwespecializethistoafunctiontypeA→Bweget

[A→[B]]=A→[B],[A→B]≤A→[B].(10)Forbracketsontheleft,itiseasytoseethat

A→[B]=[A]→[B]=[[A]→[B]].

TakingB=0thereforeyieldsthenoteworthy

¬A=¬[A]=[¬A].(12)(11)

Since¬Aisthusalwaysapropositionitisnaturaltoaskwhetherperhaps:

[A]=¬¬A?

Theanswerisingeneralnegative,sincetherearemanysimplemodelsinregularlccc’sinwhichdoublenegationclosureisnottrivialonmonos.5FirstOrderLogicviaBracketTypes

Independenttypetheorywiththetype-formingoperations,

0,1,[A],A+B,EqA,B,x:Ax:AB,

thepropositionsineverycontextmodel rst-orderlogic,underthefollowingde nitions:

⊥

∧ψ

∨ψ

= ψ

¬

x=Ay

x:A.

x:A. =========10 ×ψ[ +ψ] →ψ →0EqA(x,y) x:A [x:A ](13)

Thebracketisthususedtorectifytheoperations+andbecausethey

leadoutofpropositions.

Operationsde nedin(13)satisfytheusualrulesforintuitionistic rst-orderlogic,andtheresultingsystemisadependenttypetheorywith rst-orderlogicovereachtype.Itcanbedescribedcategoricallyastheinternallogicofaregularlcccwith nitesums.Thechiefdi erencebetweenthisformulationandmorecustomaryonesusingbothtypetheoryandpredicate

20

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,

logicisthatthe rst-orderlogicaloperationsonthepropositionsareherede nedintermsoftheoperationsontypes,ratherthantakenasprimitive.

Inadditionto rst-orderlogic,onecanusebracketstode nesubsettypes.ForanytypeΓ,x:A Btype,theassociatedsubsettype

Γ {x:A|B}type

isde nedby

{x:A|B}= x:A[B(x)].

ThesecanbecomparedtothetoolboxforsubsettypesbySambin[SV98].Bywayofexample,weremarkthatthecategoryEquofequilogicalspaces[Sco96,BBS]isaregularlccc,andsosupportsallofthelogicaloperationsconsideredabove.ForX∈Equ,thebracketofanX-indexedfamilyofequilogicalspaces

(Ex)x∈X

isofcoursetheregularepi–monoimagefactorizationofthecorrespondingdisplaymap

p:E→X.

Thedomainoftheimage[E] Xisconstructedfromthesameunderlyingspace|E|asE=(|E|,～E),butwiththenewequivalencerelation,givenby

e～[E]e pe=pe .

ThefactthatEquhasthismuchinternallogicwithoutbeingatopos,orevenapretopos,wastheoriginalobservationfromwhichthepresentworkgrew[BBS].

6FirstOrderLogicvs.Propositions-as-Types

Asanapplicationofbrackettypes,wecancomparetheconventionalinter-pretationof rst-orderlogicwiththepropositions-as-typesinterpretation,andrelate rst-orderprovabilitytoprovabilityindependenttypetheory(withoutbrackets).

Supposewehaveasingle-sorted rst-ordertheoryT,consistingofcon-stants,functionandrelationletters,andaxiomsgivenasclosedformulas.Thestandardpropositions-as-typesinterpretation ofTintotypetheory,

TDTT(14)

isdeterminedby xingtheinterpretationsofthebasicsort,theconstants,functionandrelationsymbols.Therestoftheinterpretationisdetermined

21

本文来源：https://www.bwwdw.com/article/oqs1.html