; TeX output 2013.09.08:1301 ˅v{?p0J cmsl10TheoryUUandApplicationsofCategories,K`y cmr10V*ol.q27,No.17,2013,pp.445{463.uK4|T=XQ ff cmr12ELEMENT4ARY/QUOTIENTCOMPLETION LvXQ cmr12MARIAEMILIAMAIETTIANDGIUSEPPERrOSOLINI$ $'- cmcsc10Abstract. W*e_qextend_pthenotionofexactcompletiononacategorywithweaknite $limits1to0Lawvere'selementarydoGctrines.9fW*eshow0howanysuchdoGctrine0admitsanele-$mentaryquotientcompletion,Ewhichistheuniversalsolutiontoaddingcertainquotients.$W*enotethattheelementaryquotientcompletioncanbGeobtainedasthecompGositeof$twootheruniversalconstructions:oneaddseectivequotients,ctheotherforcesexten-$sionalityBofmorphisms.kW*ealsoprovethateachBconstructionpreservescomprehension.&1.5IntrodCductionConstructionsRforQcompletingacategorybryquotientshaveQbSeenwidelystudiedincategory theoryV. tTheVmaininstanceistheso-calledexactcompletion,see[CarbSoniandCeliaMagno,*1982;CarbSoniandVitale,1998],whicrhistheuniversalconstructionofanexactcategory.orveracategory.withnitelimits;Pitformallyaddsquotienrtsof(pseudo-)equiv-alencerelations.3[Ingeneral,jthecategory-theoreticanalysisofthepropSertiesofquotienrtsprorvideslyalzveryrobust,mathematicallystructuredtheorylzwhichcanbSeappliedlzinvXarioussituations:the>yconrtents>xofthepresent>xpapSeroerspreciselythiswithrespSecttothestudyoffoundationaltheoriesforconstructivremathematics.Indeed,Hathe5use5ofquotienrtsispServXasivreininrteractivetheorem5provingwhere5proSofsareSpSerformedSinappropriatesystemsofformalizedmathematicsinacomputer-assistedwrayV.cIndeedsomekindofquotienrtcompletioniscompulsorywhenmathematicsisfor-malizedWwithinaninrtensionaltypSetheoryV,'suchastheCalculusof(Co)InductiveCon-structions#[CoSquand,1990;CoquandandPraulin-Mohring,1990]orMartin-L of 8'stypSetheoryk[Nordstr omketal.,+1990].Insucrhaconrtext,,anabstract,+nitaryconstructionofquotienrtcompletionprovidesaformalframeworkwheretocombinetheusualpracticeof(extensional)*mathematics,:withtheneed*offormalizingitinaninrtensionaltheorywithstrongdecidablepropSerties(sucrhasdecidabletypSe-checking)onwhichtopSerformtheextractionofalgorithmicconrtentsfromproSofs.TVomakreexplicittheuseofquotientcompletionintheformalizationofconstructivemathematics,}UthebpapSerb [Maietti,}V2009]includedsucrhnotionaspartofthevrerydenitionof"constructivre!foundationwhich!renesthatoriginallygivrenin[MaiettiandSamrbin,p2005]inԤtermsofatrwo-levelԤtheoryV.Accordingto[Maietti,#2009],aԤconstructivrefoundationmrustbSeequippedwithaninrtensionallevel,whichcanbSerepresentedbyasuitablestarting ff HE ReceivedUUbytheeditors2012-03-31and,inrevisedform,2013-09-01. PublishedUUon2013-09-08inthevolumeofarticlesfromCT2011. 2010UUMathematicsSub 8jectClassication:q03G3003B1518C5003B2003F55. KeyUUwordsandphrases:qquotientcompletion,splitbration,universalconstruction. c !", cmsy10 UYMariaUUEmiliaMaiettiandGiuseppGeRosolini,2013.qPermissiontocopyforprivqateusegranted. ֔445 *˅v{446bdMARIAUUEMILIAMAIETTIANDGIUSEPPEROSOLINIuK{category4&3;* pzcmi7tC",and4%anextensionallevrelthatcanbSeseenas(afragmenrtof 8)theinrternal languagepofasuitablequotienrtcompletionofpC".MAsinvestigatedin[MaiettiandRosolini,2013a],EsomeexamplesofquotienrtcompletionpSerformedonintensionaltheories,EsuchastheUinrtensionallevelToftheminimalistfoundationin[Maietti, 2009],ortheUCalculusofConstructions,donotfallundertheknorwnconstructionsofexactcompletiongivrenthatthecorrespSondingtrypetheoreticcategoriesclosedunderquotienrtsarenotexact.InN[MaiettiandRosolini,m2013a]wrestudiedtheNabstractcategory-theoreticalstructurebSehindsucrhquotientcompletions.0TVothispurpSoseweintroSducedthenotionofequivXalencerelationandquotienrtrelativetoasuitablebSeredposetandproducedaunivrersalcon-struction*Eaddingeectivre*Fquotients|hence*Ethenameelemenrtaryquotient*Ecompletion|toelemenrtarydoSctrines.InthepresenrtpapSerwreisolatethebasiccompSonenrtsoftheunivrersalconstructionsiny[MaiettiandRosolini, 2013a].RAfterrecallingthebasicnotionsxrequiredinthesequel,wreshowhowtoaddeectivequotientsuniversallytoanelementarydoSctrineinthesenseofF[Larwvere,^1970],^abSeredinf-semilatticeFonacategorywithniteproSducts,^endorwedwith,equalitryV.nSeparately,^we,describSe-howto-forceextensionalequality-ofmorphismsto\(the\baseof 8)anelemenrtarydoSctrine.Thenwreprove\thatthetwo\constructionscanbSecomrbinedtogivetheelementaryquotientcompletion. FinallywecheckthattheexactcompletionofacategorywithproSductsandwreakequalizersisaninstanceoftheelemenrtaryquotientcompletionwhiletheregularcompletionofacategoryisaninstanceofaratherdierenrtconstruction.&Í2.5DodCctrinesWVe*analyse+quotienrtswithinthegeneraltheoryofbrations,,inparticular,,thebasicbrational*conceptthat)wreshallemployisthat)ofadoSctrine. eItwasintroSduced,inaseriesofseminalpapSers,`TbryF.W.LarwveretosynthesizethestructuralpropSertiesoflogical]Hsystems,ysee]I[Larwvere,1969a;]HLawvere,1969b;]HLawvere,1970],ysee]Halso[LarwvereandxRosebrugh,4m2003]forauniedysurvreyV.PQLawvere'sxcrucialinrtuitionwasytoconsiderlogicallanguagesandtheoriesasbrationstostudytheir2-categoricalpropSerties,>@@ cmti12@e.g.connectivres3and4quantiersaredeterminedby4structuraladjunctions. Thatapproachprorvedٟextremely٠fruitful,U]see[MakkXaiandReyres,U^1977;CarbSoni,U]1982;LamrbekٟandScott,1986;Jacobs,1999;TVarylor,1999;vXanOosten,2008]andreferencestherein.TVakingfadvXanrtageeofthecategory-theoreticalpresenrtationoflogicbrybrations,?werstinrtroSduce{Xageneral{YnotionofelementarydoSctrinewhichwe{Yfoundappropriatetostudythe>notion>ofquotienrtofanequivXalencerelation,aQsee[MaiettiandRosolini,aQ2013a;MaiettiandRosolini,2013b].DenotebryInfSL)thecategoryofinf-semilattice,@i.e.HpSosetswithniteinma,andfunctionsbSetrweenthemwhichpreservesniteinma.A- cmcsc10A2.1.Definition.wLetPKCnbSeacategorywithPLbinaryproducts.lAnCF C cmbxti10CelementaryRdoKctrine(onC")isanindexedinf-semilattice*g cmmi12Pƹ:C"H(|{Y cmr8opV`-!", cmsy10 !URInfSL&{sucrhthat,=forevreryob jectAinC",thereisanob ject+2 cmmi8A ȌinPƹ(AA)sucrhthat ]˅v{}ELEMENT*ARYUUQUOTIENTCOMPLETION(447uK{(i)_theassignmenrt ߟXps: gsave currentpoint currentpoint translate 180 neg rotate neg exch neg exch translateE f ps: currentpoint grestore moveto j.K cmsy8hid\X.,; cmmi6A ;id\X.Ai $r()UR:=Ppr)Aa cmr61()^AAA _for\pKin\Pƹ(A)determinesaleftadjoinrttoPhid\X.A ;id\X.Ai#`:Pƹ(ASTA)~!P(A)|here\and_bSelorwwewritePf aǹforthevXalueoftheindexingfunctorPnonamorphismfG; P(ii)_forevrerymorphismeoftheformhprܟT1;pr ڟT2;pr ڟT2i:XP_!A!XPAAinC",5the_assignmenrt Xps: gsave currentpoint currentpoint translate 180 neg rotate neg exch neg exch translateE f ps: currentpoint grestore moveto e ()UR:=Phpr813;pr82i!()^X AA$Phpr823;pr83i(A)_for7inPƹ(X+A)determinesaleftadjoinrttoPeqp:P(X+AA)UR!P(X+A). A2.2.Remark.f(a)Condition(i)determinesA Ȍuniquelyforevreryob jectAinC".(b)SincehprܟT2;pr ڟT1ihid ʤA;idʢAiUR=hid ʤA;idʢAi,from(a)itfollorwsthat 诟Xps: gsave currentpoint currentpoint translate 180 neg rotate neg exch neg exch translateE f ps: currentpoint grestore moveto [hid\X.A ;id\X.Ai B()UR=Ppr2()^AAAforevrery7inPƹ(A). (c)IncaseCrʹhasaterminalob ject,conditions(ii)enrtailscondition(i).(d)Onehasthat>jAA 36Phid\X.A ;id\X.Ai#`(A)andAAA-Pf f (BN>)whenfG:AUR!B .@ A2.3.Remark.]FVor1 JinPƹ(X1אY1)and2 JinPƹ(X2Y2),itisusefultoinrtroSduceanotationlikre1j6 msam102fortheob ject ,