Segal Spaces in Homotopy Type Theory

Abstract

Homotopi type teori er et grunnleggende språk for å gjøre homotopi invariant matematikk, og dermed ville en forventet at det var et naturlig rammeverk å studere (∞,1)-kategorier i. Desverre er det for øyeblikket et åpent problem å formulere slike objekter i denne type teorien. Som et alternativ kan vi ta for oss en utvidelse av type teorien med en underliggende form for strenge rettede former. Vi kaller denne utvidelsen simplisiell homotopi type teori. De grunnleggende objektene i homotopi type teori kan forstås som ∞-gruppoider. Tilsvarende kan de grunnleggende objektene i simplisiell homotopy type teori forstås som simplisielle ∞-gruppoider. I denne utvidelsen har vi enkle aksiomatiseringer av (∞,1)-prekategorier og (∞,1)-kategorier som semantisk tilsvarer Segal rom og Rezk rom, også kjent som komplette Segal rom. Siden alle konstruksjoner i denne teorien er homotopi invariante, presenterer den et naturlig miljø å studere disse objektene.

Vi bygger oss opp fra bunnen, og deler oppgaven i tre hoveddeler. Først studerer vi homotopi type teori og mange av dens aspekter. Så beveger vi oss til simplisiell homotopi teori, som er et naturlig område i tolke disse to type teoriene i. Til slutt, etter å ha lagt det rette fundamentet, presenterer vi simplisiell homotopi type teori og studerer (∞,1)-kategori teori i den. Spesielt internaliserer vi visse løftingsegenskaper og fibrasjoner.

De originale arbeidet i denne oppgaven ligger i sammenkoblingene av ideer, generell elaborering om simplisiell homotopi type teori, i tillegg til internaliseringen av visse konsepter fra (∞,1)-kategori teori i klassisk matematikk til denne type teorien.

Homotopy type theory is a foundational language for doing homotopy invariant mathematics, hence one would expect it to be a natural environment in which to study (∞,1)-categories. However, it is currently an open problem to formulate such objects in this type theory. As an alternative, we may consider an extension of this type theory with a basic notion of strict directed shapes we dub simplicial homotopy type theory. The basic objects of homotopy type theory can be understood as ∞-groupoids. Correspondingly, the basic objects of simplicial homotopy type theory can be understood as simplicial ∞-groupoids. Inside this extension, we have simple axiomatizations of (∞,1)-precategories and (∞,1)-categories semantically corresponding to Segal spaces and Rezk spaces, also known as complete Segal spaces. Since all constructions in this theory are homotopy invariant, it presents a natural environment in which to study these objects.

We take a ground up approach and subdivide the thesis into three main parts. First, we study homotopy type theory itself and many of its facets. We then move on to the study of simplicial homotopy theory which is a natural area to interpret the two type theories in. Finally, having laid the proper foundation, we present simplicial homotopy type theory and study (∞,1)-category theory inside of it. In particular, internalizing certain lifting properties and fibrations.

The original work in this thesis lies in the connecting of ideas, general elaboration on simplicial homotopy type theory, as well as in the internalization of some concepts from (∞,1)-category theory in classical mathematics into this type theory.