Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

April 17, 2013

Scones, Logical Relations, and Parametricity

Posted by Mike Shulman

Consider a formal system, such as logic, type theory, or some programming language. Suppose you want to prove some “meta-theoretic property” of this system, such as the following.

  • Consistency: There is no proof of false. This is obviously a desirable property of a formal system.
  • The existence property: if it is provable that “there exists an xx such that P(x)P(x)”, then there is some particular tt such that P(t)P(t) is provable.
  • The disjunction property: if “PP or QQ” is provable, then either PP is provable or QQ is provable. The existence and disjunction properties are not true of all formal systems: they are characteristic of constructive logics. (Excluded middle obviously violates the disjunction property, while the axiom of choice obviously violates the existence property.) In fact, arguably they are a defining feature of constructive logics, where proving that something exists ought to involve “constructing” a particular such thing.
  • Canonicity: any term of natural-number type evaluates to (or, is provably equal to) some numeral (and various similar statements). This is an important property for any system that can function as a programming language: we want our programs to compute results!
  • Parametricity: I’ll explain this later on.

How might you go about proving properties like this? If you’re a syntactically minded type theorist, you might try to use induction over types. That is, you first prove something for “base types” such as the natural numbers NN, then prove that if it holds for AA and BB then it holds for derived types such as A×BA\times B, A+BA+B, and ABA\to B, etc. After a lot of work reformulating the thing you’re trying to prove as a sufficiently general statement for such an induction to go through, you finally make it all work and write QED. Then, because the reformulation you ended up with involves assigning “relations” (sometimes unary, sometimes binary) to types in an inductive way, you call the method logical relations.

I’ve gathered that this sort of thing is perfectly intuitive to a type theorist. However, when I first encountered it, being a category theorist, I had a very hard time understanding it. Certain steps seemed extremely unmotivated, and I didn’t see any principled reason for what was going on. I think I understand the type theorists’ point of view a little better now — but fortunately there’s another way to structure the whole argument, which I think makes much more sense to a category theorist.

As category theorists, we like to use universal properties to avoid doing work. (Or, more precisely, we like to use them to package up work into an easily reusable theorem, so that we only have to do the work once.) Fortunately, the syntax of type theory has a nice universal property: it constructs free categories with specified structure.

A little more precisely, from any type theory TT, we can build a category Syn TSyn_T whose objects are, roughly, the types in the theory, and whose morphisms are terms with free variables. That is, a morphism ABA\to B is a term of type BB involving a free variable of type AA. Some more details, and a few examples, can be found at the nLab page on syntactic categories.

Now whatever structure our type theory TT had, it is usually visible as some categorical property of the syntactic category Syn TSyn_T. For instance, if TT had product types, then Syn TSyn_T has categorical products. If TT also had function types, then Syn TSyn_T is cartesian closed. And so on. Moreover, Syn TSyn_T is the initial such category: for any other category CC with the appropriate categorical structure, there is an essentially unique functor Syn TCSyn_T \to C preserving that structure. (I’m sweeping a lot of details under the rug here, having to do with weakness and coherence and strictification and what categorical level this universal property lives at, but the basic idea is the important thing.)

Now the question becomes, how can we use this universal property to prove meta-theoretic properties of the type theory? Clearly, we are going to have to cook up some particular structured category CC (or perhaps more than one) so that the existence of a structure-preserving functor Syn TCSyn_T \to C tells us something about TT. Thus, the construction of CC will have to involve TT somehow—but CC must also be different from Syn TSyn_T. Moreover, we should expect to have to use the uniqueness aspect of the universal property too.

When I first wrote the above paragraph, I said that we were going to have to cleverly cook up some category CC. Then I felt embarrassed, because I remembered Tom’s comment that “if cleverness is the first quality that comes to mind, then it suggests to me that something is insufficiently understood.” So I thought for a bit, and now I can say more about where this CC comes from. (I can actually say even more than I’m about to right now, but the rest will have to wait for another post.)

Let’s take a clue from type theory itself. Consider a type like NN, the natural numbers type. Semantically, we want to think of this as a natural numbers object, which is an initial object in some category. More specifically, for any XX equipped with morphisms z:1Xz:1\to X and s:XXs:X\to X, there is supposed to be a unique morphism NXN\to X respecting this structure.

Inside of type theory, the existence of such a morphism NXN\to X is easy to specify: it’s called recursion and is the natural “elimination rule” for the type NN. But uniqueness of that morphism is not as natural, type-theoretically: it would be asserting an equality, which is less “computational”. Instead, we generalize the recursion rule to say that not only does every such XX come with a morphism out of NN, every such XX over NN comes with a section. This turns out to be equivalent to asking NN to be initial. For if NN is initial, then when XX is over NN, the map NXN\to X must be a section (by uniqueness of the composite NXNN\to X \to N); and conversely, for any two morphisms NXN\;\rightrightarrows\; X, if their equalizer admits a section, then they are equal. A homotopical version of this equivalence was proven recently by Awodey, Gambino, and Sojakova.

(You may wonder whether talking about “sections” is any better than talking about equality, since ff being a section of pp means that pf=1p f = 1. However, dependent type theory has a way to talk about sections of particular kinds of maps—called “display maps” or “dependent projections” or “fibrations”—without referring explicitly to any kind of equality.)

This suggests that to use the uniqueness as well as the existence part of the universal property of Syn TSyn_T, we might look for a structured category CC over Syn TSyn_T, for which it would be interesting to have a section. Moreover, we might expect the functor CSyn TC\to Syn_T to be some sort of category-theoretic fibration.

Now how can we build an interesting fibration over Syn TSyn_T, without knowing much about Syn TSyn_T itself? Well, if we had a functor Γ:Syn TD\Gamma:Syn_T\to D for some other category DD, and some other functor G:EDG:E\to D, then we could build the comma category of Γ\Gamma over or under GG. The most obvious choice of GG, of course, would be the identity functor of DD. But what sort of functor Γ:Syn TD\Gamma:Syn_T\to D can we build without knowing much about Syn TSyn_T? Well, as Tom also reminded us last year, about the only functors out of an arbitrary category that we can even mention are the representables, hom(x,):Syn TSethom(x,-):Syn_T\to Set. And finally, what’s the most canonical object xSyn Tx\in Syn_T? One very canonical object is the terminal one.

There are still a few choices that we might make differently, but I hope I’ve convinced you that at least one reasonable possibility to consider for CC is the scone of Syn TSyn_T: the comma category of Id SetId_{Set} over the global sections functor Γ=hom(1,):Syn TSet\Gamma = hom(1,-):Syn_T\to Set. Explicitly, an object of C=scn(Syn T)C = scn(Syn_T) consists of an object ASyn TA\in Syn_T together with a function AΓAA'\to \Gamma A. Elements of ΓA=hom(1,A)\Gamma A = hom(1,A) are called global sections of AA, so we can view AA' as a family of sets indexed by the global sections of AA. Similarly, a morphism from (A,A)(A,A') to (B,B)(B,B') consists of a morphism f:ABf:A\to B in Syn TSyn_T together with a function f:ABf':A'\to B' making the evident square commute. The projection scn(Syn T)Syn Tscn(Syn_T) \to Syn_T simply forgets the primed data.

Over a year ago, I talked about scones from a “geometric” point of view. At that time, I said that given a “forgetful functor” U:SSetU:S\to Set, we can think of the scone as a “concretization” of SS: its objects are “sets equipped with SS-structure”. It’s at least interesting to ponder this in our current situation: the objects of scn(Syn T)scn(Syn_T) are “sets equipped with the structure of a type”. I’m not really sure what that means, but it sounds profound.

Anyway, in order to apply the universal property of Syn TSyn_T to get a functor R:Syn Tscn(Syn T)R:Syn_T \to scn(Syn_T), we’ll need to know that scn(Syn T)scn(Syn_T) inherits all the categorical structure that Syn TSyn_T has. And to conclude that this map is a section of the projection, we’ll need to know that the projection also preserves all this structure. But suppose we take these two facts as given for a moment, so that RR exists and is a section of the projection. That last means that for ASyn TA\in Syn_T, R(A)R(A) is the object AA itself equipped with a family of its global sections. Thus, what RR does is just to equip every object of Syn TSyn_T with a family of sets indexed by its global sections—that is, a map R(A)AR'(A) \to A—in a way which is functorial and structure-preserving.

In particular, insofar as the maps R(A)AR'(A) \to A are injective (as often happens), what RR does is assign to each type a predicate—that is, a unary relation—on its set of global sections. And a global section of a type AA in Syn TSyn_T in just a “closed term” of type AA (meaning a term involving no free variables). Thus, in general we may think of the elements of R(A)R'(A) over a:Aa:A as “witnesses” or “proofs” that some relation “R(a)R(a)” holds.

Finally, if we look “under the hood” into the actual construction of RR, we see that it’s built inductively over the structure of types (since this is how we prove the universal property of Syn TSyn_T). Thus, these unary relations R(A)AR'(A)\hookrightarrow A are precisely the syntactically-minded type theorist’s “logical relations”. What category theory does for us is (1) fold all inductions over the structure of types into the single statement that Syn TSyn_T is initial in some category, so that we only have to do it once; and even more importantly, (2) tell us automatically what each inductive step in the construction of RR' should look like: it’s determined by the corresponding categorical structure in scn(Syn T)scn(Syn_T), which in turn is characterized by a universal property.

In order to get any mileage out of this, of course, we need an explicit description of how scn(Syn T)scn(Syn_T) inherits structure from Syn TSyn_T and from SetSet, in a way that is preserved by the forgetful functor scn(Syn T)Syn Tscn(Syn_T) \to Syn_T. This is basically always completely straightforward. Here are some easy examples that you can check for yourself:

  • The terminal object of scn(Syn T)scn(Syn_T) is 11Γ(1)1\to 1 \cong \Gamma(1).

  • The initial object of scn(Syn T)scn(Syn_T) is Γ(0)\emptyset \to \Gamma(0).

  • The product of AΓ(A)A'\to \Gamma(A) and BΓ(B)B' \to \Gamma(B) is A×BΓ(A)×Γ(B)Γ(A×B)A'\times B' \to \Gamma(A) \times \Gamma(B) \cong \Gamma(A\times B). In other words, a witness of (a,b):A×B(a,b):A\times B is just a witness of a:Aa:A together with a witness of b:Bb:B.

  • A morphism (f,f):(A,A)(B,B)(f,f'):(A,A') \to (B,B') is a monomorphism just when both ff and ff' are so. In particular, a subobject of AΓ(A)A'\to \Gamma(A) is given by a subobject m:BAm:B\hookrightarrow A in Syn T\Syn_T, together with for each bΓ(B)b\in \Gamma(B), a subset B(b)A(m(b))B'(b) \subseteq A'(m(b)).

  • If TT includes (“truncated”) existential quantification, so that Syn TSyn_T is a regular category, then (f,f)(f,f') is a regular epi just when both ff and ff' are so.

  • If TT includes binary unions of subobjects, then the union of (B,B)(A,A)(B,B') \hookrightarrow (A,A') and (C,C)(A,A)(C,C') \hookrightarrow (A,A') is (BC,BC)(B\cup C, B'\cup C').

  • If TT includes a type NN of natural numbers, then the natural numbers object of scn(Syn T)scn(Syn_T) is Γ(N)\mathbb{N} \to \Gamma(N), where \mathbb{N} is the ordinary set of natural numbers and the function sends each nn to the numeral n̲\underline{n}. In other words, a witness of t:Nt:N is a natural number nn such that tt is equal to the numeral n̲\underline{n}.

This is enough to prove consistency, canonicity, and the disjunction and existence properties! Consistency is the easiest: if there were a term of type false, it would be a morphism 101\to 0 in Syn TSyn_T. But then RR would take this to a morphism R(1)R(0)R(1) \to R(0). Since RR preserves all the categorical structure, R(1)R(1) is the terminal object 1Γ(1)1\to \Gamma(1) and R(0)R(0) is the initial object Γ(0)\emptyset \to \Gamma(0). But then we would have a morphism 11\to \emptyset in SetSet, which is impossible. (Of course, this is a relative consistency result, as always – if our axioms for SetSet were inconsistent, then there would be a morphism 11\to\emptyset.)

For the existence property, suppose we can prove (x:A).P(x)\exists (x:A) . P(x). That means exactly that the composite PA1P\hookrightarrow A \to 1 in Syn TSyn_T is a regular epi. Since RR preserves the relevant categorical structure in all cases, in this case it preserves regular epis. It follows that (P,R(P))(1,R(1))(P,R'(P)) \to (1,R'(1)) is regular epi, and in particular R(P)R(1)R'(P) \to R'(1) is a surjective function. But RR also preserves the terminal object, so R(1)=1R'(1)=1, and hence R(P)R'(P) must be nonempty. Therefore, Γ(P)\Gamma(P) is nonempty, so PP has a global element in Syn T\Syn_T. In other words, there is a closed term t:At:A such that P(t)P(t) is provable. The argument for the disjunction property is similar; I’ll leave it as an exercise. (I think Peter Freyd was the first to prove these two properties categorically in this way.)

Finally, for canonicity, suppose t:Nt:N is a term of natural-number type, hence a global section t:1Nt:1\to N in Syn TSyn_T. Then R(t)R(t) is a morphism (1,1)(N,)(1,1) \to (N,\mathbb{N}) in scn(Syn T)scn(Syn_T), since RR preserves the terminal object and the natural numbers object. But \mathbb{N} is the usual set of natural numbers, so this means that tt must be equal to some numeral (namely, the primed part of R(t)R(t)).

I think this much is already pretty awesome, but now we get to parametricity. For this we need to know, first of all, what exponentials look like in scn(Syn T)scn(Syn_T). Of course, they must be preserved by the forgetful functor, so the underlying Syn TSyn_T-object of (B,B) (A,A)(B,B')^{(A,A')} is the exponential B AB^A in Syn TSyn_T. But now the elements of the set (B A)(B^A)' which lie over f:1B Af:1\to B^A must be equivalent to maps 1(B,B) (A,A)1\to (B,B')^{(A,A')} in scn(Syn T)scn(Syn_T) lying over f:1B Af:1\to B^A in Syn TSyn_T, and hence equivalently to maps (A,A)(B,B)(A,A') \to (B,B') lying over f:ABf:A\to B. In other words, if f:ABf:A\to B is a morphism in Syn TSyn_T, hence a global element of B AB^A, then the fiber of (B A)(B A)(B^A)' \to (B^A) over ff consists of all functions ABA'\to B' lifting Γ(f)\Gamma(f).

In particular, if AΓ(A)A'\to\Gamma(A) and BΓ(B)B'\to \Gamma(B) are monic, hence merely predicates on the global sections of AA and BB respectively, then (B A)(B^A)' is also a predicate on global sections of B AB^A, which holds of f:ABf:A\to B precisely when Γ(f)\Gamma(f) maps AA' into BB'. In other words, a witness of a function ff is a function exhibiting the fact that ff preserves witnesses. (This isn’t a proof that scn(Syn T)scn(Syn_T) has exponentials, of course, only a characterization of what they must be if they exist. But as usual with this sort of thing, it’s easy to prove that this definition works.)

More generally, we’ll need local exponentials (exponentials in slice categories) and dependent products, but these work in essentially the same way: to every “function term” we assign the set of “liftings” of it to witnesses.

The other thing we need to know about is universe objects. Thus, suppose TypeType is a type of (small) types, giving a universe object in Syn TSyn_T. In particular, we have the type Type˜= X:TypeX\widetilde{Type} = \sum_{X:Type} X of pointed types, with the first projection Type˜Type\widetilde{Type}\to Type being the “universal fibration” in Syn TSyn_T. That is, for any type AA, dependent types over AA are classified by maps ATypeA\to Type, with the resulting display map BAB\to A being the corresponding pullback of Type˜Type\widetilde{Type}\to Type.

Now the first thing we need is a family of sets TypeΓ(Type)Type' \to \Gamma(Type) indexed by the global sections of TypeType. Of course, a global section of TypeType is just a type dependent over 11, which is to say a type defined in the empty context. Now given such an AA, a witness of AA must correspond to a map (1,1)(Type,Type)(1,1)\to (Type,Type') in scn(Syn T)scn(Syn_T) lifting A:1TypeA:1\to Type in Syn TSyn_T. But if (Type,Type)(Type,Type') is to be a universe object, such maps must be equivalent to objects of scn(Syn T)scn(Syn_T) lying over AA. In other words, a witness of a type A:TypeA:Type is any lifting of AA to an object of scn(Syn T)scn(Syn_T). Any lifting at all.

In particular, since R:Syn Tscn(Syn T)R:Syn_T \to scn(Syn_T) must preserve all structure, we must have R(Type)=(Type,Type)R(Type) = (Type,Type'). Note that this is not merely a unary relation on Γ(Type)\Gamma(Type): a given type has many witnesses.

We also need the universal fibration (Type˜,Type˜)(Type,Type)(\widetilde{Type}, \widetilde{Type}')\to (Type,Type'). But this is likewise easy: suppose AΓ(A)A'\to \Gamma(A) is an object of scn(Syn T)scn(Syn_T), hence a global element of (Type,Type)(Type,Type'), and suppose also that a:1Aa:1\to A is a global section of AA. Then we must have a commutative square of sets Type˜ Γ(Type˜) Type Γ(Type). \array{ \widetilde{Type}' & \to & \Gamma(\widetilde{Type}) \\ \downarrow & & \downarrow \\ Type' & \to & \Gamma(Type)}. Elements of Type˜\widetilde{Type}' lying over (A,a)Type× Γ(Type)Γ(Type˜)(A',a) \in Type' \times_{\Gamma(Type)} \Gamma(\widetilde{Type}) should be the same as liftings of (A,A):1(Type,Type)(A,A'): 1 \to (Type,Type') to (Type˜,Type˜)(\widetilde{Type}, \widetilde{Type}') which agree with a:1Aa:1\to A. But since the object (A,A)(A,A') must be the pullback of (Type˜,Type˜)(\widetilde{Type}, \widetilde{Type}') along its classifying map 1(Type,Type)1 \to (Type,Type'), this means precisely to give an element of AA' lying over aΓ(A)a\in\Gamma(A).

That is, for a type A:TypeA:Type with a witness AΓ(A)A'\to\Gamma(A), a witness of a:Aa:A is just an element of AA' over aΓ(A)a\in\Gamma(A), i.e. a witness of a:Aa:A in the ordinary sense defined above.

Finally, we’re ready for parametricity. Consider the type X:Type(XX)\prod_{X:Type} (X\to X), an inhabitant of which is a function assigning to every (small) type XX an endomorphism of XX. In classical mathematics, there are lots and lots of such functions. However, in constructive type theory, there’s essentially only one such function: the one which assigns to each XX its identity function! The point is that without some additional assumption such as excluded middle or AC, we can’t write down such a function that behaves differently depending on what XX is: e.g. we can’t say “if XX has exactly 2 elements, then swap them, otherwise, …”. (I believe this is the origin of the word “parametricity” — we say the function has to be defined parametrically in XX.) And if you just have an arbitrary XX, without knowing anything about it, then as Tom would say, what’s the only function XXX\to X that you can even mention? The identity function.

Of course, you can throw other garbage into the definition of such a function, but it won’t be able to change the fact that what comes out at the end of the day acts like the identity function. This is the theorem that we can now prove using the scone.

Categorically, the type X:Type(XX)\prod_{X:Type} (X\to X) is built as the local exponential (Type˜Type) (Type˜Type)(\widetilde{Type}\to Type)^{(\widetilde{Type}\to Type)} in the slice category of Syn TSyn_T over TypeType, followed by the dependent product from this slice category to Syn TSyn_T itself. And all these constructions must be preserved by RR. Unraveling this, the first step gives us an object of scn(Syn T)scn(Syn_T) over (Type,Type)(Type,Type'), whose component in Syn TSyn_T is the dependent type (X:Type)(XX):Type(X:Type) \vdash (X\to X) : Type. The additional data assigned by RR consists of

  • for every A:TypeA:Type (this is a global section of TypeType in Syn TSyn_T), and
  • for every choice of a lift AΓ(A)A'\to \Gamma(A) of AA to scn(Syn T)scn(Syn_T) (this is a witness of A:TypeA:Type), and
  • for every term f:AAf:A\to A (this is a global section of (Type˜Type) (Type˜Type)(\widetilde{Type}\to Type)^{(\widetilde{Type}\to Type)} lying over the classifying map of AA),

the set of liftings of ff to witnesses. Note that these witnesses are precisely given by the specified AΓ(A)A'\to \Gamma(A) above. If we think only about relations, then at this stage, RR is recording, for every term f:AAf:A\to A, whether it preserves each unary relation on Γ(A)\Gamma(A).

Now at the second step, we consider the liftings of each g: X:Type(XX)g:\prod_{X:Type}(X\to X) to the witnesses defined above. In other words, a witness of such a gg consists of, for every A:TypeA:Type and every AΓ(A)A'\to \Gamma(A), a lifting of g A:AAg_A:A\to A to these witnesses. In particular, this means that the function Γ(g A):Γ(A)Γ(A)\Gamma(g_A):\Gamma(A)\to \Gamma(A) preserves every unary relation on the set Γ(A)\Gamma(A). Clearly this is only possible if Γ(g A)\Gamma(g_A) is the identity function (consider the characteristic relations of singletons).

Finally, any actual term g: X:Type(XX)g:\prod_{X:Type}(X\to X) yields a global section 1 X:Type(XX)1\to \prod_{X:Type}(X\to X) in Syn TSyn_T, hence a global section of R( X:Type(XX))R(\prod_{X:Type}(X\to X)), and hence a witness of gg in the above sense. This is a precise form of the first parametricity theorem: any term of type X:Type(XX)\prod_{X:Type} (X\to X) behaves like the identity function when applied to terms in the empty context.

What is the point of all this? I think the example of universe objects is where the category-theoretic point of view really shines. When you do “logical relations” from the syntactic type-theory point of view, you basically have to make up each inductive clause of the definition of the logical relation RR as you go. The definition for function types is not too surprising, if you think about the unary relation RR as a sort of “well-behavedness”: it’s not unreasonable to say that a function is well-behaved if it maps well-behaved inputs to well-behaved outputs. (I believe the usual word for “well-behaved” in this context is “reducible”.) But I think the definition for a universe is pretty opaque from this point of view: a witness to reducibility of a type is any relation on its global elements at all?

Moreover, if you insist on thinking of RR as merely a relation on global elements, then you can’t even phrase it like this. Basic presentations of parametricity don’t actually include a universe object; instead they work in a “polymorphic type theory”, where you can form types that behave like “ X:Type(XX)\prod_{X:Type} (X\to X)” but which are not literally dependent products over any type “TypeType”. Then you basically have to make up the combined rule for defining RR on these types as above: g: X:Type(XX)g:\prod_{X:Type}(X\to X) is reducible if for every type AA, the function Γ(g A)\Gamma(g_A) preserves every unary relation on Γ(A)\Gamma(A).

Let me end with a few words about generalizations. There are lots of other “parametricity” theorems – have a look at this classic paper. For instance, for any definable functors FF and GG, any term of type X:Type(F(X)G(X))\prod_{X:Type} (F(X)\to G(X)) must be a natural transformation. To prove this, you need not just unary logical relations but binary logical relations. But these is easy to do categorically too: instead of the scone of Syn TSyn_T, we consider the category whose objects consist of an ASyn TA\in Syn_T, a set AA', and a function AΓ(A)×Γ(A)A' \to \Gamma(A) \times \Gamma(A). This category inherits all the relevant structure in essentially the same way.

The most general context that I know of in which to do this is the colax limit of a (pseudo)functor C:I opCatC:I^{op}\to Cat, where II is an inverse category. If II is the interval category 101\to 0 and CC picks out Γ:Syn TSet\Gamma:Syn_T \to Set, then this colax limit is the scone. If II is the parallel pair 101 \rightrightarrows 0 and CC picks out Γ\Gamma twice, then this colax limit is the place for binary relations I mentioned above. We obviously have nn-ary relations for all nn, and also potentially “higher” logical relations. (Are there any uses for those?)

The assumption that II is inverse is what gives things like exponentials and universe objects such a nice form in the colax limit. I made use of that same fact in this paper, focusing mainly on the special case of colax limits of constant functors C:I opCatC:I^{op}\to Cat — which is the same as categories of diagrams over II in some fixed category CC. But I recently realized that the same techniques work for non-constant functors, so that the scones work homotopically as well (up to a point), and in particular, inherit things like the univalence axiom.

In principle, this means that we can extend all the above theorems to type theory with univalence. Canonicity in the presence of univalence, in particular, has been an important open question since its introduction: does the univalence axiom introduce new closed terms of natural number type whose numeric value isn’t determined? Dan Licata and Bob Harper showed that the answer is essentially no in the 1-truncated case, by adding definitional equality rules to make the type theory 1-truncated, and then giving a logical relations argument to show canonicity. The gluing approach, on the other hand, doesn’t modify the underlying type theory, but yields instead a homotopical answer: every term of natural number type is homotopic to a numeral. (That this is true was conjectured by Voevodsky when he introduced the univalence axiom.)

Unfortunately, the gluing approach also suffers from a coherence problem. In a homotopical setting, we’d like to glue along a “global sections” functor valued in simplicial sets (or some other model for Gpd\infty Gpd). However, it seems hard to obtain a strict functor of this sort. We do have global sections functors into SetSet or GpdGpd, and since SetSet and GpdGpd contain one and two univalent universes, respectively, we can derive homotopy canonicity for 1-truncated type theory (in which all types are 1-types) with one or two univalent universes. (The groupoid scone was also considered, without univalence, in this paper by Hofstra and Warren.) The new version of my paper (posted today) describes this; it’s an open question how any of these results could be extended to type theories without a truncation axiom, and with arbitrarily many univalent universes.

Acknowledgments: this post owes a lot to Bob Harper, from whom I first learned about logical relations at OPLSS; to Peter Lumsdaine, who first tried to tell me what they had to do with scones; and to Thierry Coquand, whose talk at IAS last term about regarding setoids as truncated semi-simplicial types finally crystallized for me the relation between inverse diagrams and logical relations.

Posted at April 17, 2013 5:19 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2613

10 Comments & 0 Trackbacks

Re: Scones, Logical Relations, and Parametricity

Here are a couple more more papers which go into the categorical end of the connection:

Posted by: Neel Krishnaswami on April 18, 2013 9:18 AM | Permalink | Reply to this

Re: Scones, Logical Relations, and Parametricity

Thanks!

Realizability and PER models… also make the fact that the witness to reducibility of a type is an arbitrary relation seem rather natural, at least to me.

Can you explain? The only interpretation I’ve been able to attach to that statement yields essentially the same explanation that the gluing perspective does, namely that you want the universe in the scone (or whatever category) to classify objects of that category.

Posted by: Mike Shulman on April 18, 2013 1:28 PM | Permalink | Reply to this

Re: Scones, Logical Relations, and Parametricity

I suspect I can’t mean anything very formal, since PER models are logical relations. However, since you build them over sets of untyped realizers (e.g., Goedel numbers), you have fewer choices of how to give the interpretation of types. If you Goedel codes as your realizers, you don’t have many choices except to interpret types with equivalence relations on subsets of \mathbb{N}, and then interpreting a polymorphic type as something that respects arbitrary PERs is clearly the only thing you could do.

I have to admit that I’ve never used the gluing perspective in anger, though, since to date I’ve mostly worked with type theories simple enough to cook up the logical relations by hand, as it were. This has recently started to change, though. Derek Dreyer and I have started looking at parametricity in dependent type theory (for example, to give induction principles for Church numerals, thereby making them internally a natural numbers object), and the models are getting complex enough that I’m starting to feel the need for more categorical structure, to make sure I’m not leaving out side-conditions.

Posted by: Neel Krishnaswami on April 18, 2013 9:59 PM | Permalink | Reply to this

Re: Scones, Logical Relations, and Parametricity

What’s supposed to be the analogue for the equivalence of 2-categories

DependentTypeTheoriesContLangLocallyCartesianClosedCategories, DependentTypeTheories \stackrel{\overset{Lang}{\leftarrow}}{\underset{Cont}{\to}} LocallyCartesianClosedCategories \,,

in the case of homotopy type theories? An equivalence of (,2)(\infty, 2)-categories? There’s a blank space there at the moment.

Posted by: David Corfield on April 18, 2013 1:21 PM | Permalink | Reply to this

Re: Scones, Logical Relations, and Parametricity

Ohh, that’s potentially confusing. I don’t think we should use “dependent type theories” to mean “dependent type theories with Id-types, Π\Pi-types, and Σ\Sigma-types” without further explanation. I’ve tried to fix it quickly by saying “Martin-Lof dependent type theory” instead, but there may be a better way.

Anyway, I think the answer to your question is “yes, ideally”. The titles of the empty sections should give away what we expect the answers to be:

  • HoTT with Id-types, Π\Pi-types, and Σ\Sigma-types should be connected to locally cartesian closed (,1)(\infty,1)-categories. What we can say so far is that any locally presentable locally cartesian closed (,1)(\infty,1)-category provides semantics for HoTT, i.e. we have the functor LangLang. I don’t think anyone has yet checked that the functor ContCont takes HoTT to a LCCC (,1)(\infty,1)-category.

  • When we add the univalence axiom and higher inductive types, that should correspond to a notion of “elementary (,1)(\infty,1)-topos” (not yet defined). But again, we have the functor LangLang for Grothendieck (,1)(\infty,1)-toposes (modulo some coherence issues).

Posted by: Mike Shulman on April 18, 2013 1:37 PM | Permalink | Reply to this

Re: Scones, Logical Relations, and Parametricity

Nice post. Following up on Neel’s remark, Section 8.6 of Mitchell’s book “Foundations for Programming Languages” is about sconing and logical relations in the setting of simple types. He makes some remarks about extending to polymorphic types as well, but doesn’t seem to develop it further there.

There is also the paper by Ma Qing Ming and John Reynolds on a categorial treatment of parametricity from about 20 years ago. I don’t have the citation to hand, but it should not be hard to find.

Posted by: Bob Harper on April 18, 2013 8:44 PM | Permalink | Reply to this

Re: Scones, Logical Relations, and Parametricity

Your

… every term of natural number type is homotopic to a numeral

put me in mind of Joyal’s (TWF102)

really we should call the sphere spectrum the ‘true integers’.

Posted by: David Corfield on April 19, 2013 8:55 AM | Permalink | Reply to this

n-fold relations?

A vague and only vaguely related question:

might there be a nice homotopy-type-theoretic home for the notion that in higher category theory we’d call the (∞,n)-category of n-fold spans inside the ambient \infty-topos, something like the context of nn-fold (“logical”?) relations in HoTT?

For suppose I have been happily translating the constructions in higher topos theory that I care about into logical/h-type theoretic language, but now I feel I need to play a lot with nn-fold spans inside my \infty-topos. Would there or should there be a way to say “Sure, from the perspective of type theory this just means doing xyz, which we have been doing all along already, under the name […nn-fold relations…, or similar, or so…] “.

I am hoping you will be able to see the point of the question behind the vagueness (which I can’t help). I mean: it is clear that one can consider nn-fold relations, the question is maybe if its so natural a construction that it should be thought of as part of the fundamental (homotopy-)type theoy lore anyway, instead of being just any old construction that one can consider.

Posted by: Urs Schreiber on April 26, 2013 2:55 PM | Permalink | Reply to this

Re: n-fold relations?

As modal logic is

… a logic of sets and relations, in the same spirit as first-order predicate logic is a logic of sets and functions,

I’ll be listening to the answer.

Hmm, didn’t you just tell me something about spans and modality? Ah, yes

If you want individuals to have non-unique counterparts in a neighboring world, then you could replace the morphism W 1W 2W_1\to W_2 in a (pre)sheaf model with a span W 1RW 2W_1 \leftarrow R \to W_2, with RR the witnesses of “counterpartness” between pairs of individuals in W 1W_1 and W 2W_2.

Posted by: David Corfield on April 26, 2013 4:43 PM | Permalink | Reply to this

Re: n-fold relations?

Well, a span ACBA \leftarrow C \to B is (under reinterpretation as a fibration) just a doubly dependent type C:ABTypeC: A\to B\to Type, and similarly a 2-span from this to ADBA \leftarrow D \to B is is a quadruply dependent type E: a:A b:BC(a,b)D(a,b)Type.E : \prod_{a:A} \prod_{b:B} C(a,b) \to D(a,b)\to Type. Is that not what you’re looking for?

Posted by: Mike Shulman on April 28, 2013 5:34 AM | Permalink | Reply to this

Post a New Comment