Posts Tagged ‘Type theory’

J is singleton contractibility plus transport, definitionally

A somewhat technical result known in the homotopy type theory community is that the identity elimination rule (“J”) is interprovable with the following pair of facts:

  1. The based path space, \(\Sigma x:A.a=x\), is contractible; and
  2. Dependent families admit transport, \((x=y) \to C(x) \to C(y)\).

I learned this fact from Steve Awodey, who noticed it in 2009. (It appears as though it may have been independently discovered by several people, including at least Thierry Coquand. Does anyone else have more information?) The HoTT Book proves these facts using J in Lemmas 3.11.8 and 2.3.1, respectively.

I attach a short note proving not only that (1) + (2) implies J, but that definitional computation rules for (1) and (2) allow one to derive the definitional computation rule for J. My note is several months old, but this result has come up several times recently, so I thought I’d post it online:

Contractibility + transport \(\Leftrightarrow\) J.

Homotopical Patch Theory

Last week, I gave a talk at ICFP 2014 on:

Homotopical Patch Theory
Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper

Homotopy type theory is an extension of Martin-Löf type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type becomes proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches—syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.

A video of my talk is available on YouTube.

Homotopy Type Theory: Univalent Foundations of Mathematics

I spent this spring semester at the Institute for Advanced Study, where I participated in the Special Year on Univalent Foundations of Mathematics. It was an incredibly stimulating experience to work feverishly toward understanding a brand-new area, surrounded by a couple dozen world experts of fields we all hope to unify.

The news of the day is that we at the Univalent Foundations project are pleased to announce the first version of our book, Homotopy Type Theory: Univalent Foundations of Mathematics. (Available as a PDF, or in print from Lulu. See also the announcements on the HoTT blog, the n-Category Café, and Andrej Bauer’s blog.)

I can’t do much justice to homotopy type theory (HoTT) in a short blog post. The book’s introduction nicely summarizes HoTT’s origins, motivations, and basics. There have also been a number of recent survey articles, as well as introductory blog posts by Bob Harper, Dan Licata, and the prolific Mike Shulman, among others.

I know many mathematicians and computer scientists who are not category theorists, homotopy theorists, dependent type theorists, or logicians, but who would still like to understand what it is that HoTT is all about. And while the book’s introduction is for everybody, I think it could use some extra context. Consider this the introduction to the introduction, as well as (in the last section) the introduction to the extra appendix we forgot to write.

The title is sufficiently imposing that I’ll focus on explaining each of its components. Here we go!

Foundations of Mathematics

The foundations of mathematics are a touchy subject, and the book’s boldest claim is that HoTT might one day take its place as a new, so-called univalent foundation of mathematics. (More on the U-word later.)

Our modern understanding of mathematical foundations dates back to the “foundational crisis” of the early 20th century, spurred in part by the discovery of Russell’s paradox—that it would be contradictory to construct a set whose members are all sets \(S\) such that \(S\not\in S\). (Is this set a member of itself?)

Since we want mathematics to be consistent (non-contradictory), we must somehow rule out this construction, which was legal in the set theory of the time. On the other hand, since mathematics is about ideas, not painstaking manipulation of logical formulas, we would like to be careful without drowning in a sea of rigor.

There is much story to tell here, and the question of foundations is more complex than I have made it out to be. But in the end, the path forward was set by a group of French mathematicians who called themselves Nicolas Bourbaki, publishing a set of volumes unifying mathematics under the banner of modern set theory (using a variant of today’s gold standard, Zermelo–Fraenkel set theory with the axiom of choice). These volumes successfully encoded much of mathematics in ZFC, while doing so in a rigorous but manageable expository style.

The Bourbakian bargain of mathematics is our adoption of a standard style of mathematical prose which allows all our work to be, in principle, elaborated into ZFC; but of course, buying into this system means buying into ZFC as a satisfactory foundation. ZFC has successfully steered mathematics away from the frightful crises of yore, so why do we claim HoTT might deserve to take its place as a foundation of mathematics?

That’s a hard question. In large part, we wrote the book to help bolster that claim, and to develop and demonstrate a new style of mathematical prose in which all our work can be, in principle, elaborated into HoTT. I think this aspect of the project was a huge success—the book is able to go from explaining the very basics of type theory (in Chapter 1) to computing higher homotopy groups of spheres (\(\pi_n(S^n)\simeq\mathbb{Z}\), in Chapter 8) in 250 pages, a dazzling feat.

Certainly there are tradeoffs. ZFC and HoTT are fundamentally quite different, so the reasoning we employ will be somewhat unusual to a post-Bourbakian mathematician. And while we are able to define real numbers (Chapter 11), analysis in HoTT would be rather different from standard analysis, as HoTT is based on a constructive logic.

Univalent Foundations of Mathematics

As I’ve previously discussed, category theory and type theory provide robust, representation-independent notions of abstraction which are advantageous for doing mathematics.

In type theory, the proposition that two objects \(a,a’\) of type \(A\) are equal, is itself a type, \(a=_A a’\). In the past, as one might expect, we said that two objects are equal exactly when they are completely identical (up to computation; in this sense, \(1+1\) and \(2\) are completely identical).

Homotopy type theory arises from the observation that it is consistent to add more equations. (Of course, we can’t equate terms willy-nilly: \(0=1\) is inconsistent, since we can prove that \(0\neq 1\).) These do not affect the behavior of equality; for example, it’s still the case that functions take equal arguments to equal results—if \(f:A\to B\) and \(a=_A a’\), then \(f(a)=_B f(a’)\).

Moreover, because \(a=_A a’\) is itself a type, it may contain two proofs of equality \(p,q\), and these proofs might themselves be equal or not, giving rise to a type of equalities between equalities, \(p=_{(a=_A a’)}q\). These generalized equalities behave like paths in the sense of homotopy theory; just as homotopy theory studies the structure of paths in interesting topological spaces, HoTT analyzes the equality types of higher inductive types corresponding to these spaces.

The other cornerstone of HoTT is the univalence axiom, which I will explain by way of analogy.

Consider a large C program with many different data structures. These data structures are coded in separate files, and expose APIs which are not dependent on specific implementation details. These tasteful choices were made by a wise programmer to simplify reasoning about the program, and to allow each data structure to be easily used in other programs, or even swapped with another implementation of the same API.

Emboldened, this programmer claims that their two implementations of dictionaries can be silently swapped in any program at all! Of course, this is not the case—in C, one can bypass any API and read data directly out of a pointer, detecting even the slightest difference in representation. Certainly, doing so is (generally) bad practice, and is easily noticed in otherwise safe code, but it is nevertheless quite possible.

While good mathematics, like good programming, is about developing and reasoning about useful abstractions, set theory, like C, fails to prevent users from breaking these abstractions. It is, by and large, irrelevant whether pairs \((a,b)\) are defined to be \(\{\{a\},\{a,b\}\}\) or \(\{\{0,a\},\{1,b\}\}\), but since everything is a set, one can distinguish the two by asking whether \(\{a\}\in (a,b)\).

This may all seem rather pedantic, but my point is that in type theory, unlike set theory or C, such a guarantee is possible, and its codification is the univalence axiom. Univalence says that the type of equalities between two types is the type of isomorphisms between them. (Technically it’s the type of equivalences, a notion of isomorphism compatible with path structure.)

Because everything in type theory respects equality, if two types \(A,B\) are isomorphic, then any structure on \(A\) exists also on \(B\): any function \(A\to A\) gives rise to a function \(B\to B\). If \(A\) is a group, so is \(B\). In fact, any theorem about \(A\) must be true of \(B\). In this sense, univalence is an incredibly powerful extensionality principle not possible in ZFC, and is one of HoTT’s biggest selling points. It’s more than extensionality, too—we make heavy use of the fact that different isomorphisms give rise to different proofs of equality.

Homotopy Type Theory

As the title suggests, our book is, first and foremost, about mathematics in HoTT: how mathematical prose might look in a HoTT world, what we’ve proven in HoTT, and why HoTT is advantageous. But we have neglected many topics of interest to the type theorist, partly to minimize our alienation of mathematicians, and partly because we don’t yet understand the type-theoretic ramifications of HoTT very well. (I guess we’ll just have to write another book, huh?)

To close off this post, I’d like to sketch the problems that we type theorists are grappling with, and why they are relevant even to mathematics in HoTT. (If you are already familiar with dependent type theory, sections A.2–A.3 of the appendix are a natural deduction presentation of the current incarnation of HoTT. If you are not familiar with dependent type theory but want to be, Chapter 1 is an excellent introduction.)

Set theory consists of two kinds of objects: sets, and propositions about those sets. A proposition is either true or false, and classical logic specifies ways to show which. For example, to show \(A\land B\), it suffices to prove both \(A\) and \(B\).

Type theory, in contrast, has only one kind of object: types. Propositions correspond to mathematical objects—to show a proposition is true, one must construct an element of that object; to show it is false, one must show that it would be contradictory for such an element to exist. To prove \(A\land B\) is to construct an element of the product type \(A\times B\), e.g., to give a pair \((a,b)\) where \(a:A\) and \(b:B\). Given a proof of \(A\land B\), we can prove both \(A\) and \(B\) by projecting out the two proofs which make up our original proofs—\(\pi_1(a,b) = a\) and \(\pi_2(a,b) = b\).

This identification of propositions with mathematical objects results in a strikingly different logic. There are as many different proofs of \(A\) as there are elements of \(A\), and these proofs are themselves mathematical objects about which we can directly reason.

Moreover, because type theory is a constructive logic, these proofs are also terminating algorithms which specify an element of the proven proposition. (Any computer scientists still reading? Good.) So when we say that there exists a number satisfying some condition, we can point to a specific numeral along with a proof of the proposition at that number. (In classical logic, we might instead prove that such a number exists by showing that it’s impossible for no number to satisfy the condition. This proof certainly does not produce a specific numeral.)

This computational nature of type theory relies on the fact that each type’s elements all have the same shape, after computation. I said that pairing is one way to construct elements of \(A\times B\), but it’s actually the only way, in some sense. Sure, we could also construct such an element by applying a function \(\mathbb{N}\to (A\times B)\) to \(0\). This is a function application, not a pair, but it is guaranteed to yield a literal pair after computation.

This property is called canonicity, and is usually stated: “Every element of \(\mathbb{N}\) computes to a numeral.” Although it only refers to \(\mathbb{N}\), this theorem takes care of all types’ shapes at once, for the following reason.

If we had an element \(\mathsf{stuck}:A\times B\) which didn’t compute to a pair, then its projection \(\pi_1(\mathsf{stuck})\) would be an element of \(A\) which didn’t have the usual shape of such elements (since \(\pi_1\) can only compute on a literal pair). So \(A\) and \(B\) also have elements of the wrong shape. If we define a function \(f:A\to\mathbb{N}\) which examines the form of its argument, it will not be able to compute on \(\pi_1(\mathsf{stuck})\), and so we will have an element \(f(\pi_1(\mathsf{stuck}))\) of \(\mathbb{N}\) which cannot compute to a numeral.

If we are concerned only with provability, not computation, then it’s alright to add any consistent fact as a stuck term as above. We can even postulate that we have a function which decides whether a Turing machine halts, although doing so causes every type to lose its computational properties.

Right now, we’re augmenting type theory with univalence by simply adding it as a postulated term. We know it’s consistent for metatheoretic reasons, so HoTT is perfectly sound as a foundation with all the benefits I described above. But it can’t be considered a programming language yet. I and others are hoping to solve this problem by figuring out how univalence computes, but we don’t have an answer yet.

Okay, but say you don’t care about programming. Indeed, although we have ideas for how HoTT can be useful to programmers, we don’t yet have “killer apps” like we do for math. Unfortunately for you, computation is still important for doing math in HoTT!

Whenever we appeal to the univalence axiom in constructing some element, that element does not reduce properly. The more we do with that element, the more things get stuck around the univalence term, and whenever we want to prove a property of that element, we’re forced to reason about a very large term.

We can prove lemmas about how univalence acts on certain things; for example, if we use univalence with an equivalence between \(A\) and \(B\) to transport an element of \(A\) to an element of \(B\), this amounts to applying the \(A\to B\) direction of the supplied equivalence. But these two quantities are only equal in the sense of being homotopic, so to prove some property of the univalence-containing term, we must prove that property for the simpler term, and explicitly wrap it with this lemma.

As the occurrences of univalence get buried further into a term, we need to apply more and more narrow lemmas, which is time-consuming, verbose, and difficult to understand later. Worse yet, these large irreducible terms and lemmas take up lots of memory in our proof assistants, making their verification slower! Failure of canonicity is bad for both humans and computers.

I hope this has helped contextualize the HoTT project. Take a look at our book, and please feel free to leave any questions or comments here, and to open a GitHub issue if you find any bugs in the book.

Research heartbeat

If you’re wondering what I’ve been up to lately, and type theory doesn’t scare you away: I’ve been working on the homotopy type theory project, which is approximately an attempt to make sense of the higher-dimensional structure latent in Martin-Löf type theory, which is closely connected with ideas from higher category theory and homotopy theory.

In particular, I just posted on the Homotopy Type Theory blog this thing I’ve been working on. I also have some posts (for this site) in the pipeline, so stay tuned.