Lecture Notes in Mathematics 2321 Benno van den Berg Eric Faber Effective Kan Fibrations in Simplicial Sets Lecture Notes in Mathematics Volume 2321 Editors-in-Chief Jean-MichelMorel,CMLA,ENS,Cachan,France BernardTeissier,IMJ-PRG,Paris,France SeriesEditors KarinBaur,UniversityofLeeds,Leeds,UK MichelBrion,UGA,Grenoble,France AnnetteHuber,AlbertLudwigUniversity,Freiburg,Germany DavarKhoshnevisan,TheUniversityofUtah,SaltLakeCity,UT,USA IoannisKontoyiannis,UniversityofCambridge,Cambridge,UK AngelaKunoth,UniversityofCologne,Cologne,Germany ArianeMézard,IMJ-PRG,Paris,France MarkPodolskij,UniversityofLuxembourg,Esch-sur-Alzette,Luxembourg MarkPolicott,MathematicsInstitute,UniversityofWarwick,Coventry,UK SylviaSerfaty,NYUCourant,NewYork,NY,USA László Székelyhidi , Institute of Mathematics, Leipzig University, Leipzig, Germany GabrieleVezzosi,UniFI,Florence,Italy AnnaWienhard,RuprechtKarlUniversity,Heidelberg,Germany This series reports on new developments in all areas of mathematics and their applications-quickly,informallyandatahighlevel.Mathematicaltextsanalysing newdevelopmentsinmodellingandnumericalsimulationarewelcome.Thetypeof materialconsideredforpublicationincludes: 1.Researchmonographs 2.Lecturesonanewfieldorpresentationsofanewangleinaclassicalfield 3.Summerschoolsandintensivecoursesontopicsofcurrentresearch. Textswhichareoutofprintbutstillindemandmayalsobeconsiderediftheyfall withinthesecategories.Thetimelinessofamanuscriptissometimesmoreimportant thanitsform,whichmaybepreliminaryortentative. Titles from this series are indexed by Scopus, Web of Science, Mathematical Reviews,andzbMATH. Benno van den Berg (cid:129) Eric Faber Effective Kan Fibrations in Simplicial Sets BennovandenBerg EricFaber InstituteforLogic,Languageand FrankfurtamMain,Germany Computation UniversiteitvanAmsterdam Amsterdam,TheNetherlands ISSN0075-8434 ISSN1617-9692 (electronic) LectureNotesinMathematics ISBN978-3-031-18899-2 ISBN978-3-031-18900-5 (eBook) https://doi.org/10.1007/978-3-031-18900-5 MathematicsSubjectClassification:18N45,18N50,55U10,55U35,18C50 ©TheEditor(s)(ifapplicable)andTheAuthor(s),underexclusivelicensetoSpringerNatureSwitzerland AG2022 Thisworkissubjecttocopyright.AllrightsaresolelyandexclusivelylicensedbythePublisher,whether thewhole orpart ofthematerial isconcerned, specifically therights oftranslation, reprinting, reuse ofillustrations, recitation, broadcasting, reproductiononmicrofilmsorinanyotherphysicalway,and transmissionorinformationstorageandretrieval,electronicadaptation,computersoftware,orbysimilar ordissimilarmethodologynowknownorhereafterdeveloped. Theuseofgeneraldescriptivenames,registerednames,trademarks,servicemarks,etc.inthispublication doesnotimply,evenintheabsenceofaspecificstatement,thatsuchnamesareexemptfromtherelevant protectivelawsandregulationsandthereforefreeforgeneraluse. Thepublisher,theauthors,andtheeditorsaresafetoassumethattheadviceandinformationinthisbook arebelievedtobetrueandaccurateatthedateofpublication.Neitherthepublishernortheauthorsor theeditorsgiveawarranty,expressedorimplied,withrespecttothematerialcontainedhereinorforany errorsoromissionsthatmayhavebeenmade.Thepublisherremainsneutralwithregardtojurisdictional claimsinpublishedmapsandinstitutionalaffiliations. ThisSpringerimprintispublishedbytheregisteredcompanySpringerNatureSwitzerlandAG Theregisteredcompanyaddressis:Gewerbestrasse11,6330Cham,Switzerland Preface This book starts to redevelop the foundations of simplicial homotopy theory, in particular around the Kan-Quillen model structure on simplicial sets, in a more effective or “structured” style. Our motivation comes from homotopy type theory (HoTT) and Voevodsky’s construction of a model of HoTT in simplicial sets [1], which relies heavily on the existence and properties of the Kan-Quillen model structure. Type theory refers to a family of formal systems which can act both as foundationsfor(constructive)mathematicsandfunctionalprogramminglanguages. Recently, it has become apparent that there exist many connectionsbetween type theory on the one hand and homotopy theory and higher category theory on the other. Besides Voevodsky’s fundamental contributions, other key steps have been thegroupoidmodelbyHoffmanandStreicher[2],theinterpretationofMartin-Löf’s identitytypesin categoriesequippedwith a weak factorisationsystem [3] andthe proof that types in type theory carry the structure of an ∞-groupoid [4, 5]. As a result of these contributions, homotopy type theory has become an active area of researchwhichkeepsondevelopingataquickpace,withimplicationsforbothtype theoryandhomotopytheory.(Foranoverview,seetheHoTTbook[6].) However,fortypetheorytofullybenefitfromtherichtreasurechestofhomotopy theory and higher category theory, a computational understanding of the relevant resultsfromtheseareasiscrucial.Indeed,wewouldliketothinkoftypetheoryasa frameworkforcomputation.Thentofullyexploithomotopy-theoreticideasinthis framework,onemustbeabletocomputationallyreducethem.Soanaturalquestion is how constructive Voevodsky’s model in simplicial sets is, or the proofs of the propertiesoftheKan-Quillenmodelstructureonwhichitrelies. OnefundamentalobstaclewithbuildingVoevodsky’smodelinsimplicialsetsin aconstructiveframeworkwasidentifiedbyBezem,CoquandandParmann[7].To interpret(cid:2)-typesinsimplicialsets, oneusesthatthecategoryofsimplicialsetsis locallyCartesianclosed:thatis,thatthepullbackfunctoralonganymaphasaright adjoint,whichwecallpushforward.SincethetypefamiliesareinterpretedasKan fibrations in Voevodsky’s model, we need to show that Kan fibrations are closed underpushforwardalongKanfibrations.Thisistrueclassically,butastheauthors v vi Preface of[7]show,thisresultisunprovableconstructively.WewillrefertothisastheBCP- obstructionand,giventheimportanceof(cid:2)-typesintypetheory,itisquiteaserious problem. That this problem is not insurmountable was shown by Gambino and Sattler [8]: the key idea here is to treat being a Kan fibration not as a property, but as structure. Inspired by the work in HoTT on cubical sets ([9] in particular), they defineastructurednotionofauniformKanfibrationandgiveaconstructiveproof thatuniformKanfibrationsareclosedunderpushforward.Theyalsoshowthattheir definitionis “classically correct”in that a map can be equippedwith the structure ofauniformKanfibrationifandonlyifithastherightliftingpropertyagainstthe horninclusions(isaKanfibrationintheusualsense). In this book, we will introduce another solution to this problem: the effective Kan fibrations. The reason for introducing a new solution is that Gambino and Sattler ran into trouble with another type constructor: universes. Indeed, the only known method for constructing universal fibrations in presheaf categories is via the Hofmann-Streicherconstruction [10], and this method can only be applied to notionsoffibredstructurewhicharelocal(seeDefinition2.4below).Theproblem isthattheuniformKanfibrationsarenotlocal,whereasweareabletoshowthisfor ournotionofaneffectiveKanfibration.(ThatuniformKanfibrationsarenotlocal wasshownbyChristianSattler;hisproofcanbefoundinAppendixDinthisbook.) So, to summarise, ourmain contributionis the introductionof the notionof an effectiveKanfibration,astructurednotionofKanfibrationforwhichwewillprove thefollowingresults: 1. EffectiveKanfibrationsareclosedunderpushforward. 2. The notion of an effective Kan fibration is local and hence universal effective Kanfibrationsexist. 3. EffectiveKanfibrationshavetherightliftingpropertyagainsthorninclusions. 4. A map which has the right lifting property against horn inclusions can be equippedwiththestructureofaneffectiveKanfibration. Wewillgiveconstructiveproofsof(1)–(3),whereastheproofof(4)willnecessarily beineffective(duetotheBCPobstruction).Asaresult,theeffectiveKanfibrations arethefirst,andsofaronly,structurednotionoffibrationforwhichtheseproperties havebeenshown. Besideshavingaclearcomputationalcontent,anotheradvantageofconstructive proofs is that they can be internalised to arbitrary Grothendieck toposes (not just Sets). In fact, our arguments can be formalised in any locally Cartesian closed category with finite colimits and a natural numbers object. For those who prefer to think in terms of set theory, our arguments can be performed in (a subsystem of) Aczel’s constructive set theory CZF (for which see [11]), which in turn is a subsystemofclassicalZF,Zermelo-Fraenkelsettheory(withoutchoice). But however this may be, we feel that laying too great an emphasis on the metamathematicalaspects of our work may be misleading.The task of reworking someofthefundamentalconceptsinsimplicialhomotopytheoryinamoreexplicit orstructuredstyleisaninterestingundertakinginitself,whateverone’sfoundational Preface vii convictions,andwehopethatanyhomotopytheoristsreadingthisworkwillcometo seeitthatwayaswell.Indeed,anymathematicianwhowishestoskiptheoccasional foundationalaside on our part shouldfeel free to do so and can read this bookas justanotherpieceofnewmathematics. Related Work Besides the work of Gambino and Sattler we already mentioned, there are two strandsofresearchwithwhichourapproachshouldbecompared. Inresponseto theBCPobstruction,mostresearchersinHoTThaveabandoned simplicial sets and switched to cubical sets. In doing so, people have managed to constructively prove the existence of a model structure and a model of HoTT in cubicalsets. Inaddition,theircubicalmodelscanbeseenasinterpretingacubical type theory, in which principles like univalence can be derived and which enjoys (homotopy)canonicity(see[9,12–14]). Theseareimpressiveresultsandourapproachisbynomeansthatfaradvanced. However,westillfeelthatanalogousresultsforsimplicialsetswouldbepreferable: indeed, simplicial techniques pervade modern homotopy theory, much more than cubical approaches do, and in order to connect to most of the ongoing work in homotopytheoryand higher categorytheory,a simplicialapproachis more likely to be successful. In addition, it is at present not entirely clear whether any of the constructivemodelstructuresthatpeoplehavedevelopedincubicalsetsmodelthe worldofhomotopytypesor∞-groupoids. TheotherapproachwithwhichourworkshouldbecomparedisthatofGambino, Henry,SattlerandSzumiło,who,infaceoftheBCPobstruction,decidetobitethe bullet(see[15–17]).TheirstartingpointwastheconstructiveproofbySimonHenry of the existence of the Kan-Quillen model structure on simplicial sets, using the standard definitions of the Kan and trivial Kan fibrations (having the right lifting propertyagainstthehorninclusionsandboundaryinclusions,respectively).Based onthiswork,HenryincollaborationwithGambinomanagedtoconstructamodelof HoTT,modulosometrickycoherenceproblems.Theirworkhastheadvantagethat itisbasedontheusualdefinitionsofthe(trivial)Kanfibrations,sointhatsenseit looks,atleastatfirstglance,morefamiliarthanourstructuredapproach.Inaddition, theirworkisdefinitelymoreadvancedthanours. However,westillthinkthatastructuredapproachlooksmoreappealing.Dueto theBCP obstruction,theyonlyhavea weakformof(cid:2)-types.Incomparision,our approachshouldgiveusgenuine(cid:2)-typeswithdefinitionalη-andβ-rules.Also,it seemsthattoobtainagenuinemodelofhomotopytypetheorybasedontheirwork forcesonetosolvesomequitedifficultcoherenceproblems,forwhichatpresentno solutionsareknown.Incontrast,weexpectthatamorestructuredapproachwillbe helpfulinsolvinganycoherenceproblemswewouldencounterifwewouldstartto turnourworkintoamodeloftypetheory. viii Preface Acknowledgements We thank Richard Garner for some very useful conversations on polynomial functors,whichhadamajorinfluenceonChap.9.WealsothankChristianSattlerfor allowingustoincludehisproofaboutthenon-localityoftheuniformKanfibrations. Finally,wearealsogratefultotherefereesforveryhelpfulfeedback. Amsterdam,TheNetherlands BennovandenBerg FrankfurtamMain,Germany EricFaber Contents 1 Introduction................................................................. 1 1.1 FibrationsasStructure ............................................... 1 1.2 EffectiveKanFibrations ............................................ 4 1.3 SummaryofContents ............................................... 8 PartI (cid:2)-TypesfromMoorePaths 2 Preliminaries................................................................ 13 2.1 FibredStructure ...................................................... 16 2.2 DoubleCategoriesofLeftandRightLiftingStructures ........... 19 2.3 AlgebraicWeakFactorisationSystems ............................. 26 2.4 ADoubleCategoryofCoalgebras .................................. 31 2.5 CofibrantGenerationbyaDoubleCategory ....................... 37 2.6 FibredStructureRevisited .......................................... 38 2.7 ConcludingRemarkonNotation ................................... 40 3 AnAlgebraicWeakFactorisationSystemfromaDominance......... 43 4 AnAlgebraicWeakFactorisationSystem fromaMooreStructure.................................................... 49 4.1 DefiningtheAlgebraicWeakFactorisationSystem ............... 51 4.1.1 FunctorialFactorisation ..................................... 51 4.1.2 TheComonad ................................................ 52 4.1.3 TheMonad................................................... 53 4.1.4 TheDistributiveLaw ........................................ 53 4.2 HyperdeformationRetracts ......................................... 55 4.2.1 HyperdeformationRetractsareCoalgebras ................ 59 4.2.2 HyperdeformationRetractsareBifibred ................... 62 4.3 NaiveFibrations ..................................................... 66 5 TheFrobeniusConstruction .............................................. 75 5.1 NaiveLeftFibrations ................................................ 77 5.2 TheFrobeniusConstruction ......................................... 79 ix