913 index index.xml Fredrik Bakke Fredrik Bakke false I am a PhD student at the Norwegian University of Science and Technology, doing work in higher category theory and univalent type theory. I am also a maintainer of the agda-unimath project.This is my personal page where I manage my personal notes as well as miscellaneous exposition related to my work. The web page is written using Forester.Please keep in mind that this is an informal web page that is in early development. 841fb-0002fb-0002.xmlLecture notesFredrik Bakke843fb-0004fb-0004.xmlSegal spaces in Homotopy Type TheoryLecture note2024516Fredrik BakkeFMF, University of Ljubljana 571#257unstable-257.xmlAbstract2024516Fredrik Bakkefb-0004Homotopy Type Theory is a language for doing homotopy invariant mathematics. As such one would expect it to be a good setting for doing ∞-category theory. Indeed, by extending the type theory with a directed interval object we get a type theory where every type is automatically equipped with simplicial structure and every construction preserves this structure in the appropriate sense. In this setting we can define and work with ∞-categories synthetically. We will have a look at some of the basic aspects of category theory in this setting. 573hott-0001hott-0001.xmlOrthogonal mapsFredrik BakkeWe establish the basics of orthogonal maps. This concept forms an effective tool in the study of categories using simplicial types just as it does in the study of spaces using homotopy types. We assume function extensionality, but will not have need for univalence. Most of this has been formalized here@agda-unimath.464hott-0006hott-0006.xmlPullback-powerDefinition2024520Given two maps and , the type of morphisms of maps between and , is the pullback of the cospan The pullback-power is the gap map from the function type to morphisms of maps defined by the exponential square 465hott-0007hott-0007.xmlPushout-productDefinition2024520Given two maps and , the pushout-product is the cogap map into the cartesian product as defined by the product square 468#256unstable-256.xmlRemarkFredrik Bakkehott-0001 The pushout-product is dual to the pullback-power via the product-hom adjunction. 470hott-0008hott-0008.xmlAdjoint relation between pullback-powers and pushout-productsFact2024520Given three maps , , and , there is a natural equivalence of maps 473hott-0002hott-0002.xmlOrthogonal mapsDefinition2024528Given two maps and , we say is orthogonal to , written , if any of the following equivalent conditions hold For every commuting square there is a unique lifting square that factorizes the original one. The pullback-power is an equivalence. The exponential square is a pullback. The dependent precomposition map is an equivalence for all . We extend the concept of orthogonality to types by substituting them for their terminal projections, and to type families by substituting them for their total space projections. In particular, the type is orthogonal to the type iff it is -null. 480#255unstable-255.xmlProof of equivalence2024528hott-0002 For observe that the data of a lifting square is precisely the fiber of the pullback-power, and a map is an equivalence if and only if its fibers are contractible. For , note that the type is the standard pullback of the cospan, and a cone over a cospan is a pullback if and only if it is equivalent to the standard pullback. Condition is an instance of the vertical fiber condition for pullbacks. 481hott-000Ghott-000G.xmlOrthogonal mapsExample2024528Maps that are -orthogonal are precisely the equivalences. Observe how the unique lifting condition unfolds: The unique lifting condition asks that there, for every element exists a unique such that . In other words, the fibers of must be contractible. More generally, a map is -truncated iff it is -orthogonal.484hott-0004hott-0004.xmlClosure properties of right orthogonal mapsTheorem2024519Assume all maps labeled with a "" are -orthogonal. Then we have the following: iff if is a retract of , then if is a base change of , then . In particular, the fibers of are -orthogonal. if is an -transfinite cocomposition of 's, then . 485#252unstable-252.xmlProof2024519hott-0004 Follows from the pasting property of pullback-squares. The pullback-power is covariantly functorial in the right-hand argument, and equivalences are closed under retracts. Pullbacks are preserved by swapping arguments. Is a corollary of closure under dependent products. Is a corollary of closure under dependent products. See synthetic fibered -category theory. See synthetic fibered -category theory or the accompanying formalization. See synthetic fibered -category theory, Proposition 3.1.14. 486hott-0005hott-0005.xmlClosure properties of left orthogonal mapsCorollary2024519Assume is orthogonal to all maps labeled with an "". Then we have the following: iff if is a retract of , then if is a cobase change of , then if is an -transfinite composition of 's, then . 447#251unstable-251.xmlProof2024519hott-0005 The results follow by dualizing closure properties of right orthogonal maps. In particular, for property 2 we use that the pullback-power is contravariantly functorial in the left-hand argument. For property 6 we use the adjoint relation between pushout-products and pullback-powers. 487hott-000Fhott-000F.xmlAnodyne mapsDefinition2024529A map is said to be -anodyne if every map that is -orthogonal is also -orthogonal.488hott-000Hhott-000H.xmlAnodyne mapsExample2024528Equivalences are orthogonal to every map, so every map is -anodyne. -truncated maps are also -truncated, so the map is -anodyne.575stt-0001stt-0001.xmlSimplicial type theoryFredrik BakkeWe extend Martin-Löf type theory with a directed interval. The existence of this object endows every type with simplicial structure that every definable map automatically preserves. With this added structure, we can concisely define what will correspond in the semantics to -categories, maps between which will automatically be functors.577stt-0006stt-0006.xmlThe theory of a directed intervalSubsectionFredrik Bakke579stt-0002stt-0002.xmlThe coherent theory of a directed intervalDefinitionFredrik BakkeThe coherent theory of a directed interval consists of A single sort , the directed interval. Two constants . A single binary relation symbol on . such that The directed interval is nontrivial: . The directed relation is a total order on with as minimum and as maximum. I.e., (Reflexivity) (Transitivity) (Antisymmetry) (Totality)We interpret the theory of the directed interval directly in Martin-Löf type theory, with as a type, as the identitity type and as a binary family of propositions on .581stt-0004stt-0004.xmlPropositionFredrik BakkeThe directed interval forms a set. 583#247unstable-247.xmlProofFredrik Bakkestt-0004 formalization@agda-unimath Posets are sets. 585stt-0003stt-0003.xmlAlternate theory of a directed intervalRemarkFredrik BakkeThere's a second presentation of the theory of a directed interval, given by replacing the directed relation by two function symbols satisfying the laws . This theory admits the theory of the CCHM cubical interval as a subtheory.When interpreting this theory in Martin–Löf type theory, one must assume as an axiom that forms a set.587stt-0005stt-0005.xmlFactFredrik BakkeThe classifying topos of the directed interval is simplicial sets. The universal model of the directed interval is . The classifying -topos of the directed interval is simplicial spaces.589stt-0007stt-0007.xmlBasics of simplicial typesSubsectionFredrik BakkeWe consider some basic constructions we can form in the precense of the directed interval object.591stt-0009stt-0009.xmlDirected mapping cylinderDefinitionFredrik BakkeGiven a map , the directed mapping cylinder is the pushout In particular, when is a terminal projection we recover the directed cocone type under , . 595#246unstable-246.xmlRemarkFredrik Bakkestt-0009 Notice the similarity to how one makes cofibrant replacements in order to construct homotopy colimits in classical homotopy theory using strict colimits. In our scenario, we bake simplicial structure into the colimit by multiplying by the directed interval – the added structure does not come automatically as with higher homotopy structure in homotopy type theory. 597stt-000Astt-000A.xmlSome basic shapesDefinitionFredrik BakkeThe standard 1-simplex . The boundary of the standard 1-simplex The standard 2-simplex This shape should be understood as the filled lower triangle of the directed square . The standard 2-simplex has the universal property of the directed cocone under . In fact, inductively, The boundary of the standard 2-simplex Pictorially, without a filled interior. The boundary of too has a couple of defining inductive formulas. The standard 2-horns can be extracted from the boundary formula of the standard 2-simplex by omitting the 'th clause read from left to right. E.g., , the inner 2-horn, is the subshape 603stt-000Bstt-000B.xmlPushout property of the directed squareFactFredrik BakkeThe totality property of the directed relation on states precisely that the directed square is the gluing of two triangles along their diagonal, i.e., that we have a pushout square This is useful as it means we can construct functions in two interval variables by case analysis on the lower and upper triangle. 607#245unstable-245.xmlRemarkFredrik Bakkestt-000B As pointed out by Alex, we could broaden the semantics of the type theory by omitting the totality axiom and rather define simplicial types as those which view the directed relation to be total. I.e., those that are orthogonal to the cogap map 609stt-0008stt-0008.xmlArrows and homsDefinitionFredrik BakkeAn arrow in a type is a function . A directed edge from to in is an element of the type Using the language of lifting squares, a directed edge from to is a lifting of the square We also speak of higher cells of a type. For instance, given a triangle of directed edges in , we may ask that there exists a filler of the triangle The type of such datum is denoted and we interpret its elements as witnesses that the triangle of edges commutes. In particular, if such data is unique we can understand to be a composite edge of before in at most one way.617stt-000Dstt-000D.xmlConstant edgesDefinitionFredrik BakkeGiven an element , we can define the constant arrow at 619stt-000Cstt-000C.xmlFunctions are functorsConstructionFredrik BakkeGiven a map and elemens , we have an action on directed edges of type The map is given by postcomposition on the underlying arrow, and 's action on identifications on the endpoints.Since constant maps are closed under postcomposition this action on directed edges preserves constant edges There is moreover an action on 2-simplices meaning that also preserves composites. Hence, every map is already a functor of simplicial types although we have yet to define those types that look like categories.621stt-000Estt-000E.xmlSegal typesSubsectionFredrik Bakke623stt-000Fstt-000F.xmlSegal types/-precategoriesDefinitionFredrik BakkeA Segal type is a type that is orthogonal to the inner 2-horn inclusion .This means that a Segal type is a type such that every pair of compatible edges in can be extended uniquely to a commuting triangle In particular, we obtain the Segal composition operation by restricting along the diagonal of this lifting.The name "Segal type" comes from the semantics in the motivating model of simplicial spaces, where Segal types correspond to Segal spaces. We can understand these objects as (concrete) -precategories, or flagged -categories, because they are -categories that come equipped with extra structure on their objects. More concretely, they come equipped with two in advance unrelated homotopy structures: one given by the underlying space of objects and the other given by the space of isomorphisms of objects.625stt-000Hstt-000H.xmlInner maps and type familiesDefinitionFredrik BakkeMore generally, we say a map is inner if it is orthogonal to the inner 2-horn inclusion, and a type family is inner if its total space projection is.When a type family is inner over , we understand to be Segal relative to the context . We have unique dependent composites in over composites in : given a composition of before in , and a dependent directed edges over , and over in , we have a unique lifting of the square 629stt-000Gstt-000G.xmlClosure properties of Segal types/-precategoriesPropositionFredrik BakkeLet be a Segal type and let every type labelled with a "" be Segal. Then the following types are also Segal Retracts of . Moreover, if is an inner family over , then is Segal. 551#244unstable-244.xmlProofFredrik Bakkestt-000GFollows by closure properties of right orthogonal maps. 631stt-000Kstt-000K.xmlAssociativity of Segal compositionSubsubsectionFredrik Bakke633stt-000Istt-000I.xmlUnfolding squaresConstructionFredrik BakkeGiven a commuting triangle of directed edges we can, using the pushout property of the directed square, construct a commuting square called the unfolding square of the triangle. By currying, this unfolding square gives us a directed edge in the arrow type of from to .In a Segal type, given any composable pair of arrows we have such a triangle, hence there is also a directed edge . Moreover, by the closure property of Segal types under exponentials, the arrow type of is also Segal. Hence, if we have a triple of composable arrows we have a pair of composable arrows whose composite is unique. This means we have a commuting prism By uniqueness of composites in , the top triangle must be the composition of before , and the bottom triangle must be the composition of before . Hence, extracting the back square face of the prism we have a commuting square Restricting along the diagonal of this square we have a directed edge that is witnessed as both the composition and the composition , so again by uniqueness we have Thus, we have just shown the following:647stt-000Jstt-000J.xmlTheoremFredrik BakkeComposition of edges in Segal types is associative.649stt-000Lstt-000L.xmlSimplicially discrete typesSubsectionFredrik BakkeThere is a subuniverse of simplicially trivial types. We call these types simplicially discrete.651stt-000Mstt-000M.xmlSimplicially discrete typesDefinitionFredrik BakkeA type is simplicially discrete if the canonical map is an equivalence for all .653stt-000Nstt-000N.xmlEquivalent characterizations of simplicially discrete typesPropositionFredrik BakkeThe following conditions are equivalent The type is simplicially discrete. The type is -orthogonal. The type is orthogonal to the left end-point inclusion . The type is orthogonal to the right end-point inclusion . 655#243unstable-243.xmlProofFredrik Bakkestt-000N formalization@agda-unimath For , we have an equivalence of maps given by torsoriality of the identity types. Therefore, the left vertical map is an equivalence if and only if the right vertical map is. The left vertical map is an equivalence if and only if the type is -orthogonal, and the right vertical map is an equivalence if and only if the fiberwise map is. For , observe that the lifting conditions unfold to asking precisely that the left- or right-hom-family is torsorial and hence characterizes the identity types. 659stt-000Ostt-000O.xmlFibrationsSubsectionFredrik BakkeWe want a notion that captures families of spaces that vary covariantly or contravariantly over a base Segal space, the prime examples being and respectively.438stt-000Pstt-000P.xmlCovariant type familiesDefinitionFredrik BakkeA type family is covariant if it is orthogonal to the left end-point inclusion of the directed interval.This means that for every arrow in the base and every point in lying over there must be a unique dependent directed edge starting at │ │ B │ │ ∙ │ │ │ │ │ ~~~~~~~~~~~~~~~~~~~~~~~~~ ↧ ↧ ----- ∙ ——————————> ∙ ----- A. x α y]]> Thus, in particular, restricting to the right-end point of the unique lifting we obtain a transport function and it is from this transport function the concept gets its name: the fibers of vary covariantly in . Also note that by pullback stability the fibers of are all simplicially discrete.Had we instead imposed that the type families are orthogonal to the right end-point inclusion of the directed interval, we obtain the notion of a contravariant type family. These instead have a transport function of the form 440stt-000Qstt-000Q.xmlProposition2024529Fredrik BakkeCo- and contravariant type families are inner.In other words, the inner horn inclusion is anodyne at the left and right end-point inclusions of the directed interval. 432#242unstable-242.xmlProof2024529Fredrik Bakkestt-000Q We have a retract of maps so the result follows by pushout-product and retract stability of left orthogonal maps. Thanks to Sam Toth pointing out that a previous proof was incorrect.442stt-000Rstt-000R.xmlCorollary2024529Fredrik BakkeIf is a covariant type family over a Segal type, then is Segal.444stt-000Sstt-000S.xmlBased hom-space condition for Segal typesTheorem2024529Fredrik BakkeGiven a type the type family is covariant for all if and only if is Segal. 339#241unstable-241.xmlProof2024529Fredrik Bakkestt-000S Assume given directed edges and . The lifting condition of a covariant type family asks precisely that there is a unique lift │ │ hom(a,-) │ │ ∙ │ │ │ │ │ ~~~~~~~~~~~~~~~~~~~~~~~~~ ↧ ↧ ----- ∙ ——————————> ∙ ----- A b g c]]> hence, by uncurrying, that we have a unique filler so the result follows from the universal property of as the directed cone over . 845fb-0005fb-0005.xmlOther notesFredrik Bakke 333stt-0020stt-0020.xml2-Segal types2024717Fredrik BakkeWe consider the notion of a 2-Segal space after Dyckerhoff-Kapranov (and others) in simplicial type theory using a characterization given in Quasi-2-Segal sets. 287#235unstable-235.xmlDefinition2024717Fredrik Bakkestt-0020 The 2-Segal horn is the union of all face maps aside from and , where and if then . In other words, and are not adjacent mod . Here are and respectively as subshapes of Viewed differently, and yet differently again, as chains of morphisms in the coslice and slice 289#236unstable-236.xmlDefinition2024717Fredrik Bakkestt-0020 A type is 2-Segal if it is local at the 2-Segal horn inclusions and . 291#237unstable-237.xmlTheorem2024717Fredrik Bakkestt-0020 A type is 2-Segal if and only if its left- and right-based hom-spaces are Segal for all . This is Theorem 6.3.2 in Higher Segal spaces. 293#238unstable-238.xmlProof2024717Fredrik Bakkestt-0020 Let us unfold what it means for the left-based hom-spaces to be Segal. A pair of "composable" arrows in corresponds to the coherent data in , where corresponds to an extension of the span along the inclusion and likewise corresponds to an extension of the span . This correspondence can be written out more explicitly via, for instance, a similar argument to what is made for Proposition 8.13 of A type theory for synthetic ∞-categories. Under this correspondence, a composite of before corresponds to an extension of the above diagram along the inclusion , so, evidently, asking that the left-based hom-spaces of are Segal corresponds to asking that is -local. Dually, the right-based hom-spaces of are Segal precisely if is -local. 297#239unstable-239.xmlCorollary2024717Fredrik Bakkestt-0020Segal types are 2-Segal. 299#240unstable-240.xmlProof2024717Fredrik Bakkestt-0020By the based hom-space condition for Segal types the left- and right-based hom-spaces of a Segal type are contractible, and contractible types are local with respect to all maps. 847fb-0003fb-0003.xmlFormalizationsFredrik BakkeHere is a list of select formalizations by me.849agda-0002agda-0002.xmlQuasicoherent idempotents splitFormalization2024417Fredrik Bakkehttps://unimath.github.io/agda-unimath/foundation.split-idempotent-maps.htmlpartially finishedFormalized Agda proof that quasicoherent idempotents split, and some surrounding facts. agda-unimath#1105851agda-0001agda-0001.xmlCohesionFormalization2024320Fredrik Bakkehttps://unimath.github.io/agda-unimath/modal-type-theory.htmlto be reviewedA basic library for doing cohesive type theory. A large portion is currently waiting to be merged. agda-unimath#1078853agda-0004agda-0004.xmlComputational identity typesFormalization202428Fredrik Bakkehttps://unimath.github.io/agda-unimath/foundation.computational-identity-types.htmlfinishedThe computational identity types form an identity system on any type and comes equipped with a strictly involutive inverse operation and a strictly associative and one-sided unital concatenation operation. agda-unimath#1015855agda-0003agda-0003.xmlPreunivalent categoriesFormalization20231020Fredrik Bakkehttps://unimath.github.io/agda-unimath/category-theory.preunivalent-categories.htmlin progressagda-unimath#861Preunivalent categories form the common generalization of strict, set-level categories and univalent categories. agda-unimath#861857agda-0005agda-0005.xmlWild higher categoriesFormalizationFredrik Bakkehttps://unimath.github.io/agda-unimath/wild-category-theory.htmlon the shelfWe can utilize parts of higher category theory in univalent type theory using a globular model. agda-unimath#1099 This is a collaborative effort together with vojtech-stepancik. References 915 feller-2023 feller-2023.xml Quasi-2-Segal sets Reference 2023 Matt Feller 10.2140/tunis.2023.5.327 917 dyckerhoff-kapranov-2019 dyckerhoff-kapranov-2019.xml Higher Segal spaces Reference 2019 Tobias Dyckerhoff Mikhail Kapranov 10.1007/978-3-030-27124-4 920 riehl-shulman-2017 riehl-shulman-2017.xml A type theory for synthetic ∞-categories Reference 2017 5 21 Emily Riehl Michael Shulman Higher Structures 10.21136/HS.2017.06 We propose foundations for a synthetic theory of -categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define Segal types, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define Rezk types, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities - a “local univalence” condition. And we define covariant fibrations, which are type families varying functorially over a Segal type, and prove a “dependent Yoneda lemma” that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using “extension types” that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces. Related 923 agda-unimath agda-unimath.xml Agda-unimath Project https://unimath.github.io/agda-unimath/