TRUNCATION LEVELS IN HOMOTOPY TYPE THEORY by Nicolai Kraus Thesis submitted to the University of Nottingham for the degree of Doctor of Philosophy June 2015 Summary We present several original results in homotopy type theory which are related to the truncation level of types, a concept due to Voevodsky. To begin, we give a few simple criteria for determining whether a type is 0-truncated (a set), inspired by a well-known theorem by Hedberg, and these criteria are then generalised to arbitrary n. This naturally leads to a discussion of functions that are weakly con- stant, i.e. map any two inputs to equal outputs. A weakly constant function does in general not factor through the propositional truncation of its domain. How- ever, the factorisation is (among other cases) always possible for weakly constant endofunctions, which we use to define a propositional notion of existence. Further, we present a couple of constructions which are only possible with the judgmental computation rule for the truncation, for example an invertibility puzzle that seem- ingly inverts the canonical map from N to ∥N∥. One of the two main results is the construction of strict n-types in Martin-Löf type theory with a hierarchy of univalent universes (and without higher induct- ive types), and a proof that the universe U is not n-truncated. The other main n result of this thesis is a generalised universal property of the propositional trun- cation, using a construction of coherently constant functions. We show that the type of such coherently constant functions from A to B is equivalent to the type ∥A∥ → B. In the general case the definition requires an infinite tower of condi- tions, which exists if the type theory has Reedy limits of diagrams over ωop. If B is an n-type for some given finite n, (non-trivial) Reedy limits are unnecessary, allowing us to construct functions ∥A∥ → B in homotopy type theory without further assumptions. To obtain these results, we develop some theory on equality diagrams, especially equality semi-simplicial types. In particular, we show that the semi-simplicial equality type over any type satisfies the Kan condition, which can be seen as the simplicial version of the result by Lumsdaine, and by van den Berg and Garner, that types are weak ω-groupoids. Finally, we present some results related to formalisations of infinite structures. For example, we show how the category ∆ of finite non-empty sets and strictly + increasing functions can be implemented so that the categorical rules hold strictly. In the presence of very dependent types, we speculate that this makes the “Reedy approach” for the famous open problem of defining semi-simplicial types work. i Acknowledgements Firstofall,IwanttoexpressmydeepandhonestgratitudetoThorstenAltenkirch. It has been a privilege to be his PhD student. During the last years, he has always given me freedom to pursue my own ideas, and offered me guidance whenever I could benefit from it. When I encountered a problem, he always readily provided suggestions and support (even at times when other things kept him busy as well). He made it possible that I could visit the univalent foundations special year in Princeton and many other interesting events. He is an excellent teacher of all sorts of academic topics and an inspiring discussion partner for research ideas. Maybe most importantly, he has always been a thoughtful and caring mentor for me. Special thanks goes to Christian Sattler. In the last decade, I have learned far more mathematics from him than from any of my professors. He is an exceptional academic colleague and an invaluable friend. I am thankful for many interesting discussions, especially with Martín Escardó and Paolo Capriotti. Without all the ideas Martín and I have shared, the contents and probably even the title of my thesis would be different today, which I believe says it all. With Paolo, I could always discuss all sorts of questions, and I have learned a lot from him and from all our reading groups. I also thank everyone else for their interest and contributions to our regular meetings, in particular Venanzio Capretta and, of course, Christian and Thorsten, but also Gabe Dijkstra, Ambrus Kaposi, Nuo Li and, in the end, Manuel Bärenz. My two thesis examiners, Julie Greensmith (internal examiner) and Steve Awodey (external examiner) have both spent a lot of time with my thesis. I truly appreciate their work, which has helped me in several ways. Their advice has enabled me to improve the general style of the thesis and the readability of multiple text passages, and, of course, to fix various smaller typographical mis- takes. Steve’s comments on my research itself have been valuable and have led to not only interesting ideas for future research, but also to a couple of remarks that I have added in the current (final) version of the thesis. I was very lucky that I happened to be a student at the same time as Ambrus and Nuo. We have shared many interests, academic ones and non-academic ones. In the early days of my PhD studies, I have received support from Andreas Abel and Neil Sculthorpe. Already a decade before that, my interest for mathematics was stimulated by my high school teacher Markus Jakob. There are many more people who would deserve to be mentioned. I thank the participants (especially the organisers, Steve Awodey, Thierry Coquand, and Vladimir Voevodsky) of the special year in Princeton and all other meetings for a lot of stimulating input, in particular Thierry Coquand and Michael Shulman. The first has given me advice on several occurrences and I had the pleasure of working with him, as well as with Martín and Thorsten, on a joint project. The latter has inspired me a lot through his numerous amazing blog posts. I am also grateful for the interesting remarks of Vladimir Voevodsky on one of my main iii results, and I thank Andrea Vezzosi for his contributions to one of the projects I have worked on. Many people have given me feedback on my work, and I would like to thank everyone who did, as this has been very valuable for me. Some of the comments I could understand immediately, and others required (or still require) me to spend some time before I could fully benefit from them. I explicitly want to include the anonymous reviewers of the work that I have published during the time of my PhD studies, who have all given very helpful feedback. In general, the community of this research area is welcoming and friendly, making it easy for a student to become a part of it. I am also grateful to Venanzio Capretta for spending time with my work and for making valuable suggestions during my annual reviews. Apart from Martín and Thorsten, I especially thank Graham Hutton for his general support in many situations. All the members of the functional programming lab in Nottingham have made the last years truly enjoyable. I want to restrict these acknowledgements to the mostly academic component. I am not someone who likes to make details of his private life public. Nevertheless, thesupportthatmanypeople(especiallyIrmgardandNorbertKraus, andJocelyn Chen) have given me outside of the academic environment has been extremely important, and I know they are aware of my thankfulness. iv Contents Summary i Acknowledgements iii Contents v 1 Introduction 1 1.1 Historical Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 A brief introduction to truncation levels and operations . . . . . . 6 1.3 Overview over Our Results . . . . . . . . . . . . . . . . . . . . . . . . 8 1.4 Computer-Verified Formalisations . . . . . . . . . . . . . . . . . . . . 13 1.5 Declaration of Authorship and Previous Publications . . . . . . . . 15 2 Overview over Homotopy Type Theory and Preliminaries 17 2.1 Martin-Löf Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.2 Constructions with Propositional Equality . . . . . . . . . . . . . . . 23 2.3 Homotopy Type Theory . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2.4 A Word on Ambiguity Avoidance and Readability . . . . . . . . . . 40 3 Truncation Level Criteria 43 3.1 Hedberg’s Theorem Revisited . . . . . . . . . . . . . . . . . . . . . . 43 3.2 Generalisations to Higher Levels . . . . . . . . . . . . . . . . . . . . . 49 4 Anonymous Existence 51 4.1 Collapsible Types have Split Support . . . . . . . . . . . . . . . . . . 51 4.2 Populatedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.3 Comparison of Notions of Existence. . . . . . . . . . . . . . . . . . . 58 5 Weakly Constant Functions 69 5.1 The Limitations of Weak Constancy . . . . . . . . . . . . . . . . . . 69 5.2 Factorisation for Special Cases . . . . . . . . . . . . . . . . . . . . . . 72 6 On the Computation Rule of the Propositional Truncation 79 6.1 The Interval . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 6.2 Function Extensionality . . . . . . . . . . . . . . . . . . . . . . . . . . 83 v 6.3 Judgmental Factorisation . . . . . . . . . . . . . . . . . . . . . . . . . 83 6.4 An Invertibility Puzzle . . . . . . . . . . . . . . . . . . . . . . . . . . 85 7 Higher Homotopies in a Hierarchy of Univalent Universes 89 7.1 Background of the Problem. . . . . . . . . . . . . . . . . . . . . . . . 89 7.2 The First Cases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 7.3 Pointed Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 7.4 Homotopically Complicated Types . . . . . . . . . . . . . . . . . . . 98 7.5 A Solution with the “Wrapping” Approach . . . . . . . . . . . . . . 101 7.6 Connectedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 7.7 Combining the Results . . . . . . . . . . . . . . . . . . . . . . . . . . 112 8 The General Universal Properties of Truncations 115 8.1 A First Few Special Cases . . . . . . . . . . . . . . . . . . . . . . . . 119 8.2 Fibration Categories, Inverse Diagrams, and Reedy Limits . . . . . 124 8.3 Subdiagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 8.4 Equality Diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130 8.5 The Equality Semisimplicial Type . . . . . . . . . . . . . . . . . . . . 131 8.6 Fibrant Diagrams of Natural Transformations . . . . . . . . . . . . 135 8.7 Extending Semi-Simplicial Types . . . . . . . . . . . . . . . . . . . . 137 8.8 The Main Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141 8.9 Finite Cases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147 8.10 Elimination Principles for Higher Truncations . . . . . . . . . . . . 150 8.11 The Big Picture: Solved and Unsolved Cases . . . . . . . . . . . . . 161 9 Future Directions and Concluding Remarks 167 9.1 The Problem of Formalising Infinite Structures . . . . . . . . . . . . 167 9.2 Semi-Simplicial Types . . . . . . . . . . . . . . . . . . . . . . . . . . . 168 9.3 Yoneda Groupoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 178 9.4 Set-Based Groupoids. . . . . . . . . . . . . . . . . . . . . . . . . . . . 183 9.5 Further Notes on Related Work and Conclusions . . . . . . . . . . . 186 Bibliography 193 ○A Electronic Appendix vi Chapter 1 Introduction Homotopy type theory is a new branch of mathematics. It forms a bridge between seemingly very distant topics: Only ten years ago, very few, if any, type theorists would have expected to get involved in algebraic topology or the theory of weak ω-categories, and neither would researchers who feel at home when it comes to the fundamental groups of spaces have believed that a significant amount of their discoveries can be formalised and computer-verified in an elegant way, using a foundation of mathematics that is based on something known as Martin-Löf type theory. This thesis presents several results on truncation levels, informally, the higher homotopical structure of types. The important observation that this concept can be formulated internally in type theory is due to Voevodsky [Voe10a]. The thesis is subdivided into nine chapters. At the beginning of each chapter, we give a very concise overview over its contents. In this introductory Chapter 1, we first present a short historical outline (Section 1.1), and the ideas of truncation levels is explained in Section 1.2. We then give a detailed overview over the contents of this thesis and the results with their developments. In particular, a list stating which results I consider my main contributions to the field of homotopy type theory can be found at the end of Section 1.3. An important aspect of the considered field of research are computer-verified formalisations. Because of this, the current thesis has an electronic appendix with such formalisations, and some details are described in Section 1.4. Finally, in Section 1.5, we provide additional information on journal and conference publications that have been based on the contents of this thesis. Much of the work has been done in collaboration, and we strive to give a detailed statement on authorships. Therearemanyexcellentintroductionstohomotopytypetheory, bothinterms of its development and its concepts and results. Although some information is provided in this thesis, in particular in Chapter 2, a beginner is advised to read through an introduction that covers the basic concepts in higher detail. The ca- nonical reference is certainly the book Homotopy Type Theory: Univalent Founda- tions of Mathematics [Uni13], writtenbytheparticipantsofthe2012/13Univalent 1 1. Introduction Foundations Program at the Institute for Advanced Study, Princeton. Others in- clude the overview by Awodey [Awo12], the notice of Awodey, Pelayo, and Warren for the AMS [APW13], and the introduction by Pelayo and Warren [PW12]. 1.1 Historical Outline Martin-Löf type theory (MLTT), more precisely intensional Martin-Löf type the- ory, and sometimes also referred to as Intuitionistic or Constructive type theory, was introduced and pushed forward by Martin-Löf [ML98; ML75; ML82; ML84]. It constitutes a branch of mathematical logic with many applications in computer science, especially in the theory of programming languages. At the same time, it is powerful enough to serve as a framework for the formalisation of huge parts of mathematics. These two, namely “programming” and “proving” (loosly speak- ing), can indeed be viewed as the main applications of MLTT. Obviously, this connection is based on the Curry-Howard Correspondence [How80] and one could argue that the two concepts are the same thing; however, in praxis, someone using MLTT for programming often has slightly different requirements than someone who is trying to prove a theorem. Among mathematicians, fairly well known is the proof assistant Coq which is basedonavariantofMLTT,theCalculus of Inductive Constructions [CH88]. Coq has acquired much of its publicity when it was utilised by Gonthier and Werner to formalise a proof of the famous Four Colour Theorem [Gon08] which says that at most four colours are necessary to colour a map such that adjacent countries do not have the same colour. For more recent work in Coq, we want to mention the Feit-Thompson Odd Order Theorem [Gon+13] and the ForMath project. Another implementation of MLTT is Agda [Nor07]. Of course, it can be used as a proof assistant, and indeed, we have used it to formalise many of our res- ults presented in this thesis. Yet, it is often viewed as a programming language, even though there is in theory (close to) no difference between a dependently typed programming language and a proof assistant. Programming in a depend- ently typed language bears huge advantages. The rich type system can be utilised to provide an immediate precise formal specification or correctness proof of a program. Moreover, even though beginners of Agda who come from another func- tional programming language such as Haskell can find the powerful type system a burden, this opinion changes as they get accustomed to it. If a program does not type check in Agda, something is wrong, and a second thought would be re- quired in Haskell as well, the only difference being that Haskell would not tell the programmer. A core aspect of MLTT is computation: terms are identified with their normal forms. For concrete implementations, such as Agda and Coq, this means that we have an automatic simplification of expressions. For a programmer, this is an obvious necessity. On the other hand, in a proof on paper, such a simplification would have to be done manually by the mathematician, and we believe that the 2