Description

95 Homotopy type theory Álvaro Pelayo 1, Michael A. Warren 2 To Vladimir Voevodsky, whose Univalence Axiom has opened many mathematical doors We give a glimpse of an emerging field at the intersection

Information

Category:
## Crafts

Publish on:

Views: 92 | Pages: 16

Extension: PDF | Download: 0

Share

Transcript

95 Homotopy type theory Álvaro Pelayo 1, Michael A. Warren 2 To Vladimir Voevodsky, whose Univalence Axiom has opened many mathematical doors We give a glimpse of an emerging field at the intersection of homotopy theory, logic, and theoretical computer science: homotopy type theory. One key ingredient of this approach is Vladimir Voevodsky s Univalence Axiom. It is the goal of this paper to provide a short introduction to some of the ideas of homotopy type theory and univalence. The approach taken here is to first develop some of the historical and mathematical context in which homotopy type theory arose and then to describe the Univalence Axiom and related technical machinery. 1. Introduction The past decade has seen the birth of a new research field at the intersection of pure mathematics and theoretical computer science: homotopy type theory. It is in the framework of homotopy type theory, that Vladimir Voevodsky formulated his celebrated Univalence Axiom and stated his ideas regarding univalent foundations. Homotopy type theory [4, 21, 12] is an emerging field which brings together insights from research in pure mathematics (higher-dimensional category theory, homotopy theory, mathematical logic, etc.) and computer science (type theory, programming languages, proof assistants, etc.). Whereas in the usual approach to the foundations of mathematics one takes sets as the basic entities from which mathematical structures are constructed, in homotopy type theory the basic entities are spaces (homotopy types), in the sense of homotopy theory, rather than sets. The key insight which led to the development of homotopy type theory is the realization that a direct axiomatization of spaces already existed in Martin-Löf s work on type theory. Because type theory, which plays an important role in mathematical logic, is the theoretical basis for many current programming languages and computer proof assistants (Coq, Agda, etc.), proofs in homotopy theory and other parts of pure mathematics can be formally verified in proof assistants using the ideas of homotopy type theory. This approach is justified by the homotopy theoretic interpretation of type theory, which was independently discovered by Awodey and Warren [5, 30] and Voevodsky [27, 28], building on ideas of Hofmann and Streicher [11, 24], Moerdijk, Palmgren, and others. This interpretation relates structures arising 1 University of California, San Diego Mathematics Department La Jolla, USA. Pelayo is partly supported by NSF CAREER Award DMS and Spain Ministry of Science Sev Los Angeles, CA, USA 96 Á. PELAYO, M. A. WARREN in homotopy theory, such as Kan complexes and Quillen model categories, with Martin-Löf s [19, 17] dependent type theory. At around the same time, Gambino and Garner [7], van den Berg and Garner [6], and Lumsdaine [16] showed that this interpretation could be turned around to construct homotopy theoretic structures from the syntax of type theory. Crucial to this entire endeavor was Voevodsky s discovery of the Univalence Axiom which captures important features of his Kan complex model of type theory. (Kan complexes, which are especially nice combinatorial models of spaces and -groupoids, are discussed more in Section 2.8 below.) The following ingredients make homotopy type theory possible: (1) The homotopy theoretic interpretation of type theory. (2) The Univalence Axiom. (3) Higher-inductive types or other type theoretic encodings of homotopy theoretic data. We have already encountered items (1) and (2) above. Item (3) is roughly the type theoretic analogue of combinatorial models of spaces such as models using CW-complexes or simplicial sets. In summary, item (1) shows that it is indeed consistent to view types as spaces. Item (2) forces types to behave more like spaces and item (3) makes it possible to describe familiar spaces and constructions on spaces (spheres, suspensions, etc.) in terms of types. The goal of the present paper is to describe in an informal way some of the ideas which have made their way into homotopy type theory. In particular, we touch, in varying levels of detail, on all three of the ingredients mentioned above. Summary of the paper. In Section 2 we develop some of the background material which, while not strictly necessary, should provide a clearer historical and mathematical context for homotopy type theory. In particular, we describe the development of type theory in parallel with developing some simple, but important, ideas from algebraic topology. These small vignettes are designed to help draw out some of the analogies between homotopy theory and type theory. In particular, both homotopy theory, especially when viewed from the perspective of higher-dimensional category theory, and type theory have made use of ideas related to annotating known mathematical structures with additional data. For example, up-to-homotopy, algebraic structures are the result of taking familiar equational theories (such as the theory of groups) and replacing the equations by annotating homotopies. On the other hand, Church s simple type theory can be seen as the result of annotating derivations in propositional logic. In Section 3 we introduce the Univalence Axiom and other ideas of Voevodsky regarding the foundations of mathematics. This section is the heart of the paper. In Section 4 we make some concluding remarks regarding connections between homotopy type theory and computer assisted proof. This is something which we do not treat in detail, but which is important since it has been one of the motivating factors for Voevodsky and others working in this area. Other relevant literature. Although there is some overlap between the present paper and our papers [21, 4], the exposition here is focussed a bit more on the logical side of matters and we here include more detail of the historical context on HOMOTOPY TYPE THEORY 97 the logical side. For a very brief introduction to Voevodsky s Univalence Axiom we invite the reader to consult [4]. For a detailed look at homotopy type theory and univalent foundations with a view towards the formalization of mathematics in Coq we suggest [21]. The textbook [12] develops the theory more or less from first principles. Those readers interested in the semantics of homotopy type theory should look at [3, 26, 25]. A recent overview of a wider range of connections between category theory and logic can be found in [8]. Many of the ideas described in Sections 2.2 and 2.4 below are developed more fully in [9], which is one of the canonical references for type theory and its connection with logic. Voevodsky s own description of his Coq library can be found in [29]. We hope that this article will serve to persuade many readers to learn more about the fascinating emerging subjects of homotopy type theory and Voevodsky s univalent foundations program; we believe these subjects will be of mathematical interest in the long term, and that there is great potential that their further development will have a significant impact on the way working mathematicians read, write, and ddiscover proofs. 2. A few mathematical vignettes Although homotopy type theory is a new subject, there is a long history of connections between logic, topology and algebra. A brief survey of some of these connections should help to demystify some of the concepts of homotopy type theory and will allow us to develop some of the required background incrementally. Note though that we are not historians of mathematics and, as such, the sketch presented here is admittedly biased and incomplete Set theoretic antimonies and Russell s theory of types Modern abstract mathematics arose at around the time of Riemann s Habilitation lecture in 1854 on the foundations of geometry. Subsequent mathematicians such as Cantor and Dedekind developed the kind of naïve theory of sets and functions needed for the then new mathematics to flourish. In 1901, Russell discovered his well-known paradox: should we admit, for each property ϕ, the existence of a set {x ϕ} of all elements satisfying ϕ, then we are led to consider the troublesome set R := {x x / x}. In response to this and other paradoxes arising from the naïve view of sets, Russell introduced his type theory. In Russell s type theory, each set is to be associated with a natural number, which should be thought of as indicating the level at which it has been constructed. So we would write, x : 3, y : 13,... in such a way that the relation a b is allowed to hold only for a : n and b : n The natural numbers annotating the sets are called their types. This theory is usually taken to be the historical origin of type theory, although some of the ideas undoubtedly go back much further and modern type theory is quite different from Russell s theory. Ultimately, Russell s type theory failed to attract much of a following and the de facto foundational system eventually became, and still remains, Zermelo-Frankel set theory with the Axiom of Choice. Nonetheless, it is worth mentioning Russell s theory as the idea 3 The notation x : 3 is not Russell s, but is closer to notation we will employ later. Also, we are simplifying matters: Russell in fact introduced several theories of types. 98 Á. PELAYO, M. A. WARREN of annotating mathematical structures is present throughout the history of type theory Propositional logic Although mostly known for his work in topology, Brouwer advocated an approach to foundations starkly at odds with the set theoretic trend of the time. Brouwer himself was against the formal codification of mathematical principles, but his student Heyting formalized his ideas as what is called intuitionistic logic. We will briefly recall the simplest form of intuitionistic logic which is called propositional (intuitionistic) logic. Assume given a set V. We refer to elements of V as propositional variables. Usually these are thought of as representing declarative statements such as, 2+2=4, The normal distribution is symmetric about its mean, and so forth. A proposition is then either a propositional variable or is obtained by applying the logical connectives to other propositions. Here the logical connectives are summarized in Figure 1 below, where A and B denote propositions and is the constant false proposition (i.e., a nullary connective). We can define the negation not A of name of connective read as falsum false A B conjunction A and B A B disjunction A or B A B conditional If A, then B Figure 1. Logical connectives. a proposition A as A := A. The set P of propositions is the smallest set containing V and closed under the operations,, and. 4 In what follows we will restrict our attention to the portion of propositional logic concerned only with and. We now define a set C of what are called contexts. By definition a context, written Γ,, Θ,..., is a finite list (A 1,..., A n ) of propositions where we allow n = 0 (the empty context) and we allow A i = A j for i j. 5 Given a context Γ and a proposition A we will write Γ, A for the result of appending A to the list Γ. Next, we introduce a relation Γ B between contexts Γ and propositions B. This relation is the subset of C P determined by the inference rules of logic. For example, there is an inference rule, called -introduction, which says that if Γ A and Γ B, then Γ A B. It is often inconvenient to describe inference rules in such a verbose way so we use the common shorthand for such a rule as follows: Γ A Γ B introduction Γ A B 4 To be precise, we should also require some convention regarding the use of parentheses. However, we omit such logical arcana and refer the reader to any standard text in logic for a detailed treatment. 5 The reader will notice that we should allow several operations (structural rules), such as rearranging the order of the propositions occurring in the context, on contexts. These issues are important, but we have chosen to avoid them in the interest of simplifying our presentation. HOMOTOPY TYPE THEORY 99 The idea being that the relation below the line holds when the relations listed above the line hold. The name of the rule is indicated on the right. The additional rules governing and the rules for are summarized in Figure 2. We also require the following rule, Γ, A A Axiom which allows us to infer that A holds when it appears in the context. One usually Γ A B Γ A elimination (left) Γ A B Γ B elimination (right) Γ, A B Γ A B introduction Γ A B Γ B Γ A elimination Figure 2. Remaining rules of inference for and. works with these rules by stacking one on top of another to form a tree. For example, to prove that the relation ( A (B C) ) ( (A B) (A C) ) holds we simply construct the tree illustrated in Figure 3 where, for notational convenience, we set P := A (B C), and where the leaves are instances of the Axiom rule. P, A A (B C) P, A A E P, A B C E P, A B I P A B P (A B) (A C) P, A A (B C) P, A A E P, A B C E P, A C I P A C I Figure 3. Derivation tree of A (B C) (A B) (A C). Remarkably, the system formalized by Heyting can be interpreted using the open sets of a topological space X by letting be intersection, be union, be the empty set, and by defining as follows: U V := {W U W V } = ( (X U) V ) for open sets U and V. Consequently, it is quite easy to prove that the law of excluded middle P P, which holds in classical propositional logic, does not hold in intuitionistic propositional logic. E.g., taking as our ambient space R and letting P be the open set (0, + ) we see that P P = (0, + ) (, 0). 100 Á. PELAYO, M. A. WARREN 2.3. Weakening and annotating: a topological example Interestingly, in both topology and logic several important structures have arisen by virtue of annotating known structures with an additional mathematical layer. In some cases, this process has allowed for the original intended structure to be weakened in the sense that, e.g., equations governing the structure are now relaxed and replaced by a relation other than equality. 6 The most natural setting for this kind of machinery is higher-dimensional category theory, but we will here constrain ourselves to examples of this phenomenon coming from topology and logic. Let X be a topological space and let x 0 X be a point of X. The loop space of X based at x 0, which we write as Ω(X ) when x 0 is understood, is the space of continuous maps f : I X such that f (0) = x 0 = f (1), where I = [0, 1] is the unit interval. We define a concatenation f g operation on Ω(X ) by letting { f (2t) for t [0, 1 (f g)(t) := 2 ] g(2t 1) for t [ 1 2, 1] for f, g Ω(X ). Similarly, we have an inverse operation f 1 which traverses f in reverse. With the structure just described Ω(X ) is almost a group with multiplication (f g), inverses f 1 and unit element the constant loop r(x 0 ) given by r(x 0 )(t) := x 0 for t I. However, it is easy to see that this is not a group. E.g., the multiplication is not associative since (f (g h)) will still be traversing f at 3 8, whereas ((f g) h) will have already moved on to g at this point. One solution to this problem is to observe that although Ω(X ) is not a group, it is a group up to homotopy. Recall that if f and g are continuous maps X Y for X and Y topological spaces, a homotopy ϕ from f to g (written ϕ: f g) consists of a continuous map ϕ: X [0, 1] Y such that ϕ(x, 0) = f (x) and ϕ(x, 1) = g(x). Coming back to the loop space Ω(X ) we see that we have homotopies α f,g,h : ((f g) h) (f (g h)), ι f : (f f 1 ) r(x 0 ), and so forth, for f, g, h Ω(X ). So, we have weakened the group laws and replaced the equations specifying what it is to be a group by homotopies which provide a corresponding annotation. We sometimes say that the homotopies are witnesses of the algebraic laws in question. One can weaken many algebraic structures in similar ways and this has in fact been done. From our perspective the importance of this particular example will soon become clear. 6 The terminology of weak versus strict is used frequently in the literature on higher-dimensional category theory, but is rarely clarified. In practice, a structure being strict usually refers to the case where the defining conditions of the structure are axiomatized using the smallest possible relation or relations satisfying certain constraints. Often the constraint is simply that the relation should be an equivalence relation and strictness then refers to the case where the structure is axiomatized in terms of equations. By contrast, the weak case occurs when the structure is axiomatized using a larger relation satisfying the constraints. 2.4. Annotating: a logical example HOMOTOPY TYPE THEORY 101 Following the early use of the locution type theory by Russell, the next major development in type theory came with Church s simple type theory. Consider for a moment a derivation in propositional logic such as the derivation from Figure 3 above. Simple type theory can be regarded as an annotated version of the, fragment of intuitionistic propositional logic described above, where the annotations capture the structure of the derivation trees. We will write our annotations as a : A where A can, for now, be thought of as a proposition and a is regarded as a kind of code for the derivation tree of A (assuming A is derivable). For example, we would then annotate the introduction rule for as follows: Γ a : A Γ b : B Γ (a, b) : A B Here we use a tuple notation (a, b) for the annotation to indicate that a derivation of A B can be obtained by simply collecting a derivation of A together with a derivation of B. This notation is also reminiscent of elements of a cartesian product of sets A B and, in fact, this is the standard notation for A B in simple type theory. As such, we henceforth write A B. In simple type theory we do not speak of propositions and annotations. Instead when faced with a : A we say that A is a type and a is a term of type A. A context Γ is now a list (x 1 : A 1,..., x n : A n ) where the x i are variables. The rules of inference, aside from the introduction rule for given above, for and in simple type theory are summarized in Figure 4. In the introduction rule for, the variable x in λ x:a b is bound. Intuitively, λ x:a b is an algorithm for transforming derivations of A into derivations of B using b. It is sometimes convenient to think of A B as being like the set of all functions from a set A to a set B. In this case, λ x:a b is the function given by x b(x). Γ p : A B E (left) Γ π 1 (p) : A Γ, x : A b : B I Γ λ x:a b : A B Γ A B E (right) Γ π 2 (p) : B Γ f : A B Γ a : A E Γ f (a) : B Figure 4. Rules of inference for and in simple type theory. So we see that simple type theory can be viewed in (at least) two ways. In the first, we think of the terms as codes for derivation trees in propositional logic. This interpretation of simple type theory is sometimes called propositions as types or the Curry-Howard correspondence. In the second, we think of types as sets and terms as elements. There is actually a third way that is worth knowing about, even if we do not make use of it here, which is to think of types as objects in a cartesian closed category and terms as generalized elements. (Conversely, the morphisms of a cartesian closed category can be regarded as equivalence classes of proofs in a formal system and we refer the reader to [14] for a detailed exposition of these 102 Á. PELAYO, M. A. WARREN type former name logical set theoretic A B simple product A B cartesian product A B exponential A B function space B A Figure 5. Products and exponentials. matters.) The first two of these interpretations are summarized in Figure 5. In addition to being able to construct terms of given types a : A, we can also reason about equality of terms and types in type theory. This is taken as two further relations in addition to the basic relation Γ a : A. Namely, we write Γ A = B to indicate equality of types and Γ a = a : A equality of terms

Related Search

Similar documents

We Need Your Support

Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks