## 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 $x$ such that $P(x)$”, then there is some particular $t$ such that $P(t)$ is provable.
• The disjunction property: if “$P$ or $Q$” is provable, then either $P$ is provable or $Q$ 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 $N$, then prove that if it holds for $A$ and $B$ then it holds for derived types such as $A\times B$, $A+B$, and $A\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 $T$, we can build a category $Syn_T$ whose objects are, roughly, the types in the theory, and whose morphisms are terms with free variables. That is, a morphism $A\to B$ is a term of type $B$ involving a free variable of type $A$. Some more details, and a few examples, can be found at the nLab page on syntactic categories.

Now whatever structure our type theory $T$ had, it is usually visible as some categorical property of the syntactic category $Syn_T$. For instance, if $T$ had product types, then $Syn_T$ has categorical products. If $T$ also had function types, then $Syn_T$ is cartesian closed. And so on. Moreover, $Syn_T$ is the initial such category: for any other category $C$ with the appropriate categorical structure, there is an essentially unique functor $Syn_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 $C$ (or perhaps more than one) so that the existence of a structure-preserving functor $Syn_T \to C$ tells us something about $T$. Thus, the construction of $C$ will have to involve $T$ somehow—but $C$ must also be different from $Syn_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 $C$. 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 $C$ 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 $N$, 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 $X$ equipped with morphisms $z:1\to X$ and $s:X\to X$, there is supposed to be a unique morphism $N\to X$ respecting this structure.

Inside of type theory, the existence of such a morphism $N\to X$ is easy to specify: it’s called recursion and is the natural “elimination rule” for the type $N$. 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 $X$ come with a morphism out of $N$, every such $X$ over $N$ comes with a section. This turns out to be equivalent to asking $N$ to be initial. For if $N$ is initial, then when $X$ is over $N$, the map $N\to X$ must be a section (by uniqueness of the composite $N\to X \to N$); and conversely, for any two morphisms $N\;\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 $f$ being a section of $p$ means that $p 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_T$, we might look for a structured category $C$ over $Syn_T$, for which it would be interesting to have a section. Moreover, we might expect the functor $C\to Syn_T$ to be some sort of category-theoretic fibration.

Now how can we build an interesting fibration over $Syn_T$, without knowing much about $Syn_T$ itself? Well, if we had a functor $\Gamma:Syn_T\to D$ for some other category $D$, and some other functor $G:E\to D$, then we could build the comma category of $\Gamma$ over or under $G$. The most obvious choice of $G$, of course, would be the identity functor of $D$. But what sort of functor $\Gamma:Syn_T\to D$ can we build without knowing much about $Syn_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_T\to Set$. And finally, what’s the most canonical object $x\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 $C$ is the scone of $Syn_T$: the comma category of $Id_{Set}$ over the global sections functor $\Gamma = hom(1,-):Syn_T\to Set$. Explicitly, an object of $C = scn(Syn_T)$ consists of an object $A\in Syn_T$ together with a function $A'\to \Gamma A$. Elements of $\Gamma A = hom(1,A)$ are called global sections of $A$, so we can view $A'$ as a family of sets indexed by the global sections of $A$. Similarly, a morphism from $(A,A')$ to $(B,B')$ consists of a morphism $f:A\to B$ in $Syn_T$ together with a function $f':A'\to B'$ making the evident square commute. The projection $scn(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:S\to Set$, we can think of the scone as a “concretization” of $S$: its objects are “sets equipped with $S$-structure”. It’s at least interesting to ponder this in our current situation: the objects of $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_T$ to get a functor $R:Syn_T \to scn(Syn_T)$, we’ll need to know that $scn(Syn_T)$ inherits all the categorical structure that $Syn_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 $R$ exists and is a section of the projection. That last means that for $A\in Syn_T$, $R(A)$ is the object $A$ itself equipped with a family of its global sections. Thus, what $R$ does is just to equip every object of $Syn_T$ with a family of sets indexed by its global sections—that is, a map $R'(A) \to A$—in a way which is functorial and structure-preserving.

In particular, insofar as the maps $R'(A) \to A$ are injective (as often happens), what $R$ 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 $A$ in $Syn_T$ in just a “closed term” of type $A$ (meaning a term involving no free variables). Thus, in general we may think of the elements of $R'(A)$ over $a:A$ as “witnesses” or “proofs” that some relation “$R(a)$” holds.

Finally, if we look “under the hood” into the actual construction of $R$, we see that it’s built inductively over the structure of types (since this is how we prove the universal property of $Syn_T$). Thus, these unary relations $R'(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_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 $R'$ should look like: it’s determined by the corresponding categorical structure in $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)$ inherits structure from $Syn_T$ and from $Set$, in a way that is preserved by the forgetful functor $scn(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)$ is $1\to 1 \cong \Gamma(1)$.

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

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

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

• If $T$ includes (“truncated”) existential quantification, so that $Syn_T$ is a regular category, then $(f,f')$ is a regular epi just when both $f$ and $f'$ are so.

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

• If $T$ includes a type $N$ of natural numbers, then the natural numbers object of $scn(Syn_T)$ is $\mathbb{N} \to \Gamma(N)$, where $\mathbb{N}$ is the ordinary set of natural numbers and the function sends each $n$ to the numeral $\underline{n}$. In other words, a witness of $t:N$ is a natural number $n$ such that $t$ is equal to the numeral $\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 $1\to 0$ in $Syn_T$. But then $R$ would take this to a morphism $R(1) \to R(0)$. Since $R$ preserves all the categorical structure, $R(1)$ is the terminal object $1\to \Gamma(1)$ and $R(0)$ is the initial object $\emptyset \to \Gamma(0)$. But then we would have a morphism $1\to \emptyset$ in $Set$, which is impossible. (Of course, this is a relative consistency result, as always – if our axioms for $Set$ were inconsistent, then there would be a morphism $1\to\emptyset$.)

For the existence property, suppose we can prove $\exists (x:A) . P(x)$. That means exactly that the composite $P\hookrightarrow A \to 1$ in $Syn_T$ is a regular epi. Since $R$ preserves the relevant categorical structure in all cases, in this case it preserves regular epis. It follows that $(P,R'(P)) \to (1,R'(1))$ is regular epi, and in particular $R'(P) \to R'(1)$ is a surjective function. But $R$ also preserves the terminal object, so $R'(1)=1$, and hence $R'(P)$ must be nonempty. Therefore, $\Gamma(P)$ is nonempty, so $P$ has a global element in $\Syn_T$. In other words, there is a closed term $t:A$ such that $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:N$ is a term of natural-number type, hence a global section $t:1\to N$ in $Syn_T$. Then $R(t)$ is a morphism $(1,1) \to (N,\mathbb{N})$ in $scn(Syn_T)$, since $R$ preserves the terminal object and the natural numbers object. But $\mathbb{N}$ is the usual set of natural numbers, so this means that $t$ must be equal to some numeral (namely, the primed part of $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)$. Of course, they must be preserved by the forgetful functor, so the underlying $Syn_T$-object of $(B,B')^{(A,A')}$ is the exponential $B^A$ in $Syn_T$. But now the elements of the set $(B^A)'$ which lie over $f:1\to B^A$ must be equivalent to maps $1\to (B,B')^{(A,A')}$ in $scn(Syn_T)$ lying over $f:1\to B^A$ in $Syn_T$, and hence equivalently to maps $(A,A') \to (B,B')$ lying over $f:A\to B$. In other words, if $f:A\to B$ is a morphism in $Syn_T$, hence a global element of $B^A$, then the fiber of $(B^A)' \to (B^A)$ over $f$ consists of all functions $A'\to B'$ lifting $\Gamma(f)$.

In particular, if $A'\to\Gamma(A)$ and $B'\to \Gamma(B)$ are monic, hence merely predicates on the global sections of $A$ and $B$ respectively, then $(B^A)'$ is also a predicate on global sections of $B^A$, which holds of $f:A\to B$ precisely when $\Gamma(f)$ maps $A'$ into $B'$. In other words, a witness of a function $f$ is a function exhibiting the fact that $f$ preserves witnesses. (This isn’t a proof that $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 $Type$ is a type of (small) types, giving a universe object in $Syn_T$. In particular, we have the type $\widetilde{Type} = \sum_{X:Type} X$ of pointed types, with the first projection $\widetilde{Type}\to Type$ being the “universal fibration” in $Syn_T$. That is, for any type $A$, dependent types over $A$ are classified by maps $A\to Type$, with the resulting display map $B\to A$ being the corresponding pullback of $\widetilde{Type}\to Type$.

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

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

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

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

Finally, we’re ready for parametricity. Consider the type $\prod_{X:Type} (X\to X)$, an inhabitant of which is a function assigning to every (small) type $X$ an endomorphism of $X$. 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 $X$ 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 $X$ is: e.g. we can’t say “if $X$ 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 $X$.) And if you just have an arbitrary $X$, without knowing anything about it, then as Tom would say, what’s the only function $X\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 $\prod_{X:Type} (X\to X)$ is built as the local exponential $(\widetilde{Type}\to Type)^{(\widetilde{Type}\to Type)}$ in the slice category of $Syn_T$ over $Type$, followed by the dependent product from this slice category to $Syn_T$ itself. And all these constructions must be preserved by $R$. Unraveling this, the first step gives us an object of $scn(Syn_T)$ over $(Type,Type')$, whose component in $Syn_T$ is the dependent type $(X:Type) \vdash (X\to X) : Type$. The additional data assigned by $R$ consists of

• for every $A:Type$ (this is a global section of $Type$ in $Syn_T$), and
• for every choice of a lift $A'\to \Gamma(A)$ of $A$ to $scn(Syn_T)$ (this is a witness of $A:Type$), and
• for every term $f:A\to A$ (this is a global section of $(\widetilde{Type}\to Type)^{(\widetilde{Type}\to Type)}$ lying over the classifying map of $A$),

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

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

Finally, any actual term $g:\prod_{X:Type}(X\to X)$ yields a global section $1\to \prod_{X:Type}(X\to X)$ in $Syn_T$, hence a global section of $R(\prod_{X:Type}(X\to X))$, and hence a witness of $g$ in the above sense. This is a precise form of the first parametricity theorem: any term of type $\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 $R$ as you go. The definition for function types is not too surprising, if you think about the unary relation $R$ 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 $R$ 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 “$\prod_{X:Type} (X\to X)$” but which are not literally dependent products over any type “$Type$”. Then you basically have to make up the combined rule for defining $R$ on these types as above: $g:\prod_{X:Type}(X\to X)$ is reducible if for every type $A$, the function $\Gamma(g_A)$ preserves every unary relation on $\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 $F$ and $G$, any term of type $\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_T$, we consider the category whose objects consist of an $A\in Syn_T$, a set $A'$, and a function $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^{op}\to Cat$, where $I$ is an inverse category. If $I$ is the interval category $1\to 0$ and $C$ picks out $\Gamma:Syn_T \to Set$, then this colax limit is the scone. If $I$ is the parallel pair $1 \rightrightarrows 0$ and $C$ picks out $\Gamma$ twice, then this colax limit is the place for binary relations I mentioned above. We obviously have $n$-ary relations for all $n$, and also potentially “higher” logical relations. (Are there any uses for those?)

The assumption that $I$ 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^{op}\to Cat$ — which is the same as categories of diagrams over $I$ in some fixed category $C$. 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 $\infty Gpd$). However, it seems hard to obtain a strict functor of this sort. We do have global sections functors into $Set$ or $Gpd$, and since $Set$ and $Gpd$ 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

### Re: Scones, Logical Relations, and Parametricity

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

• John Mitchell and Andrew Scedrov, Notes on Sconing and Relators

It explains the basic setup of logical relations from a categorical pov, for simple types.

• Realizability and PER models are basically defined using logical relations, and so many of the same ideas carry over. They also make the fact that the witness to reducibility of a type is an arbitrary relation seem rather natural, at least to me.

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

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

in the case of homotopy type theories? An equivalence of $(\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 $(\infty,1)$-categories. What we can say so far is that any locally presentable locally cartesian closed $(\infty,1)$-category provides semantics for HoTT, i.e. we have the functor $Lang$. I don’t think anyone has yet checked that the functor $Cont$ takes HoTT to a LCCC $(\infty,1)$-category.

• When we add the univalence axiom and higher inductive types, that should correspond to a notion of “elementary $(\infty,1)$-topos” (not yet defined). But again, we have the functor $Lang$ for Grothendieck $(\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 $n$-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 $n$-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 […$n$-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 $n$-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?

… 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_1\to W_2$ in a (pre)sheaf model with a span $W_1 \leftarrow R \to W_2$, with $R$ the witnesses of “counterpartness” between pairs of individuals in $W_1$ and $W_2$.

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

### Re: n-fold relations?

Well, a span $A \leftarrow C \to B$ is (under reinterpretation as a fibration) just a doubly dependent type $C: A\to B\to Type$, and similarly a 2-span from this to $A \leftarrow D \to B$ is is a quadruply dependent 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

### Re: Scones, Logical Relations, and Parametricity

It’s at least interesting to ponder this in our current situation: the objects of $scn(Syn T)$ are “sets equipped with the structure of a type”. I’m not really sure what that means, but it sounds profound.

Maybe we might twist it arround and say “objects of $scn(Syn T)$ are Types equipped with the stuff of a set”?

Posted by: Jesse C. McKeown on December 17, 2014 3:17 AM | Permalink | Reply to this

### Re: Scones, Logical Relations, and Parametricity

Yes, we could; we could do that for any scone or gluing construction. I guess that way it’s more obvious what it means, although it doesn’t fit the general picture of “concreteness” I was trying to present.

Posted by: Mike Shulman on December 18, 2014 12:28 AM | Permalink | Reply to this

Post a New Comment