The n-Category Café

I am intrigued by the role the self-indexing stack $X \mapsto S/X$ (on slide 30) plays.

Do you see a role for the under-self-indexing $X \mapsto X/S$? Elsewhere the claim is that a tremendous amount of interesting geometric information is encoded in the objectwise stabilized/abelianized self-under-indexing of a higher “category of spaces” $S$. This must have a logical counterpart, I suppose.

Well, I haven’t finished writing my response to the paper as you sent it by email (but I like it, I like it!). However, since you asked specifically for terminological advice, here is mine:

• On ‘autological’: I’m wary of any terms derived from ‘separation’, since this is liable to conflict with unrelated topological terminology. The only meaning of ‘autological’ that I know of is in relation to the Grelling–Nelson paradox, where it refers to a self-describing adjective. If you’re happy with invoking that idea, then go for it.

• On ‘well-pointed’: I honestly don’t know why one wouldn’t simply use ‘well-pointed’ period. Is there any literature that studies topos theory from an externally constructive perspective that uses that term in the weaker (but classically equivalent) sense? If so, then sure, say ‘constructively well-pointed’ to clarify (and in any case, say ‘classically well-pointed’ for the weaker notion when comparing them). But if not, then use the standard term for what that term really should mean (and already does mean, even if one usually simplifies the definition classically).

I’m very happy to see you are developing “2-logic”, and I’m sure David Corfield will be happy too.

But what exactly do you mean by this:

I prefer to say: Sets are already analogous to truth values in a 1-topos, via Curry-Howard.

It seems like something I should understand and like, but somehow I don’t get the reference to Curry-Howard.

Are you saying sets are to the topos Set as truth values are to the set {F,T}? Or what?

Or are you saying that characteristic functions of sets are valued in truth values?

I note you have slides for category theorists who don’t know a lot about categorial logic, and there seem to be plenty of papers/notes etc running in this direction. However there is precious little running in the opposite direction - ie stuff for people who are happy with logic and/or material set theory who need to acquire enough category theory to understand categorial logic.

Meanwhile I am finding your paper very interesting so far (but, as yet I am only on page 4).

Slide on page 7: do you really mean that BZ only reaches up to $\aleph_\omega$ or up to $V_{\omega+\omega}$. I suppose what I am asking is: how do you know that $\aleph_\omega$ is in $V_{\omega+\omega}$?

Isn’t your counting of “$n$-types” curiously off by one, as here, on slide 21?

An ordinary type should be a 1-type, not a 0-type, no?

Generally I suppose in an $(\infty,1)$-topos we want to say that an object is an $n$-type (in the categorical semantics of the topos) precisely if it is $(n-1)$-truncated.

Is that right (up to a different opinion on where to start counting, possibly)?

Here is a simple type theory, which we may call the equational theory of a group.

A word of warning before I begin: This is so simple that people might hesitate to actually call it a ‘type theory’ at all. The reason is that the types are all fixed in advance; there is no theory of how to build new types out of old. For that reason, people might prefer to call it a ‘typed theory’ (a theory with types) than a ‘type theory’ (a theory about types). In fact, not only are all of the types fixed in advance; there is only one type! So people might prefer to call it an ‘untyped theory’ (this is an example of the [[red herring principle]]: an untyped theory is actually a typed theory in which there is exactly one type). I start with this such a simple example because it is one that you should already know, so it will help you to learn the language and notation.

We define everything recursively, so to tell you what (for example) a context is, I simply define what data you might use to build a context, and then give notation for that context. In fact, I will define through mutually recursive definitions what a context is, what a term in a context is, and what an equational identity in a context is; as a technical device, I will also define the number of free variables (which will always be a natural number) in a context.

One normally uses uppercase Greek letters for contexts. To indicate that $a$ is a term in the context $\Gamma$, we write $\Gamma \vdash a\colon G$. (The ‘$\colon G$’ indicates that $G$ is the type of the term $a$; since there is only one type in this theory, that bit is superflous. But I include it so that we can generalise later.) An equational identity in a context will always be a pair of terms in that context; to indicate $\Gamma \vdash a\colon G$ and $\Gamma \vdash b\colon G$ constitute such a pair, we write $\Gamma \vdash a = b\colon G$. Finally, to indicate the number of free variables in $\Gamma$, we write ${|\Gamma|}$.

So: a context in the equational theory of a group may be constructed in any of three ways:

• There exists a context, called the empty context and denoted $\epsilon$.
• For every context $\Gamma$, there exists another context, called the extension of $\Gamma$ by a new variable and denoted $\Gamma, \mathrm{x}_n\colon G$, where $n$ is the number of free variables in $\Gamma$.
• For every context $\Gamma$, every term $a$ in $\Gamma$, and every term $b$ in $\Gamma$, there exists a context, called the extension of $\Gamma$ by the equation of $a$ and $b$ and denoted $\Gamma, a = b\colon G$.

The notation for these recursively built contexts mirrors the notation for terms and equational identities in a context, which is no coincidence. However, notice that we have commas here, not ‘${\vdash}$’.

Since the only way to begin constructing a context is with the empty context, we usually leave out ‘$\epsilon$’ and the first comma: thus, $\epsilon, \mathrm{x}_0\colon G, \mathrm{x}_1\colon G$, for example, becomes $\mathrm{x}_0\colon G, \mathrm{x}_1\colon G$. Similarly, we abbreviate ‘$\epsilon \vdash \cdots$’ to simply ‘$\vdash \cdots$’.

Since contexts are constructed recursively, I may define the number of free variables in a context recursively:

• The number of free variables in the empty context is $0$.
• For every context $\Gamma$, the number of free variables in the extension of $\Gamma$ by a new variable is $n + 1$, where $n$ is the number of free variables in $\Gamma$.
• For every context $\Gamma$, the number of free variables in the extension of $\Gamma$ by any equation is the same as the number of free variables in $\Gamma$.

So every time we extend a context by a new variable, we get one more free variable.

Next, a term in a context in the equational theory of a group may be constructed in any of four ways.

• For every context $\Gamma$ and every natural number $i \lt {|\Gamma|}$, there is a term in $\Gamma$, called the $i$th variable of $\Gamma$ and denoted $\mathrm{x}_i$.
• For every context $\Gamma$, there is a term in $\Gamma$, called the identity element and denoted $1$.
• For every context $\Gamma$ and term $a$ in $\Gamma$, there is a term in $\Gamma$, called the inverse of $a$ and denoted $a'$.
• For every context $\Gamma$ and terms $a$ and $b$ in $\Gamma$, there is a term in $\Gamma$, called the product of $a$ and $b$ and denoted $(a b)$.

As always in algebra, we tend to omit the outer pair of parentheses for a term constructed as a product, although we need to keep those parentheses if we continue to construct a new term out of it.

Finally, an equational identity in a context $\Gamma$ in the equational theory of a group is any pair of terms in $\Gamma$ that may be obtained in any of the following ways.

• For every context $\Gamma$ and term $a$ in $\Gamma$, we have the equational identity $\Gamma\vdash a = a\colon G$, by reflexivity at $a$.
• For every context $\Gamma$, terms $a$ and $b$ in $\Gamma$, and equational identity $\Gamma \vdash a = b\colon G$, we have $\Gamma \vdash b = a\colon G$, by symmetry at $a$ and $b$.
• For every $\Gamma \vdash a = b\colon G$ and $\Gamma\vdash b = c\colon G$, we have $\Gamma \vdash a = c\colon G$, by transitivity at $a$, $b$, and $c$.
• For every $\Gamma \vdash a = b\colon G$, we have $\Gamma \vdash a' = b'\colon G$, called substitution into an inverse at $a$ and $b$.
• For every $\Gamma \vdash a = b\colon G$ and $\Gamma \vdash c\colon G$, we have $\Gamma \vdash a c = b c\colon G$, called left substitution into a product at $a$, $b$, and $c$.
• For every $\Gamma \vdash a\colon G$ and $\Gamma \vdash b = c\colon G$, we have $\Gamma \vdash a b = a c\colon G$, called right substitution into a product at $a$, $b$, and $c$.
• For every term $\Gamma \vdash a\colon G$ in context, we have $\Gamma \vdash 1 a = a\colon G$, called the left unit law at $a$.
• For every term $\Gamma \vdash a\colon G$ in context, we have $\Gamma \vdash a 1 = a\colon G$, called the right unit law at $a$.
• For every term $\Gamma \vdash a\colon G$ in context, we have $\Gamma \vdash a' a = 1\colon G$, called the left inverse law at $a$.
• For every term $\Gamma \vdash a\colon G$ in context, we have $\Gamma \vdash a a' = 1\colon G$, called the right inverse law at $a$.
• For every $\Gamma \vdash a\colon G$, $\Gamma \vdash b\colon G$, and $\Gamma \vdash c\colon G$, we have $\Gamma \vdash (a b) c = a (b c)$, called associativity at $a$, $b$, and $c$.

That's it!

There are many variations that we can introduce for the rules handling variables. Here I've adopted the practice of numbering the variables; as you can see if you start building up a few contexts using the first two rules, the variables are simply numbered in order. Thus a typical context is $\mathrm{x}_0\colon G, \mathrm{x}_1\colon G, \mathrm{x}_0' = \mathrm{x}_1$, which has $2$ free variables. It is more common in practice to allow one to introduce arbitrary notation for the free variables; so this same context might be denoted $x\colon G, y\colon G, x' = y\colon G$ or $y\colon G, x\colon G, y' = x\colon G$ or $\alpha\colon G, \beta\colon G, \alpha' = \beta\colon G$, etc. It is possible to write down a formal definition that takes this into account and avoids the counting, but it is technically more complicated, because you have to keep track of which variable names are taken. (In particular, $x\colon G, x\colon G, x' = x$ is not allowed!) So for my purposes, all of the actual variable names are of the form ‘$\mathrm{x}_i$’ and anything else is an informal notation.

There are standard ways of symbolically stating all or most of the rules above. I'm not sure about how to put the rules for forming contexts or counting the number of free variables in a context; people would probably prefer to just say in words that a context is a list of variable declarations and equational hypotheses, leaving it to the reader to realise that you have to keep track of how many variables appear (or which variables appear, without repeating any) and that you can only insert an equation that goes between terms that are valid in the context so far. But the other rules may be written like this: $$\array { \frac {} {\Gamma \vdash 1} \\\\ \frac {\Gamma \vdash a\colon G\qquad \Gamma \vdash b\colon G} {\Gamma \vdash a b\colon G} \\\\ \frac {\Gamma \vdash a\colon G} {\Gamma \vdash a'\colon G} \\\\ \frac {\Gamma \vdash a\colon G} {\Gamma \vdash a = a\colon G} \\\\ \frac {\Gamma \vdash a = b\colon G} {\Gamma \vdash b = a\colon G} \\\\ \frac {\Gamma \vdash a = b\colon G \qquad \Gamma \vdash b = c\colon G} {\Gamma \vdash a = c\colon G} \\\\ \frac {\Gamma \vdash a = b\colon G} {\Gamma \vdash a' = b'\colon G} \\\\ \frac {\Gamma \vdash a = b\colon G \qquad \Gamma \vdash c\colon G} {\Gamma \vdash a c = b c\colon G} \\\\ \frac {\Gamma \vdash a\colon G \qquad \Gamma \vdash b = c\colon G} {\Gamma \vdash a b = a c\colon G} \\\\ \frac {\Gamma \vdash a\colon G} {\Gamma \vdash 1 a = a\colon G} \\\\ \frac {\Gamma \vdash a\colon G} {\Gamma \vdash a 1 = a\colon G} \\\\ \frac {\Gamma \vdash a\colon G} {\Gamma \vdash a' a = 1\colon G} \\\\ \frac {\Gamma \vdash a\colon G} {\Gamma \vdash a a' = 1\colon G} \\\\ \frac {\Gamma \vdash a\colon G \qquad \Gamma \vdash b\colon G \qquad \Gamma \vdash c\colon G} {\Gamma \vdash (a b) c = a (b c)\colon G} }$$ The idea is that if you have everything above a line, then you get the judgement below that line.

If you play around with this, you should find that you can start proving theorems in the equational theory of a group. For example, you can prove that the identity element is its own inverse as follows:

• As always, $\epsilon$ is a context (the empty context).
• As in any context, we have the term $\vdash 1\colon G$ (remember that this abbreviates $\epsilon \vdash 1\colon G$).
• Continuing, we have its inverse, the term $\vdash 1'\colon G$, and their product, the term $\vdash 1 1'\colon G$.
• By the right identity law at $1$, we have $\vdash 1 1' = 1\colon G$.
• By symmetry at $1 1'$ and $1$, we have $\vdash 1 = 1 1'\colon G$.
• By the left unit law at $1'$, we have $\epsilon \vdash 1 1' = 1'\colon G$.
• Finally, by transitivity at $1$, $1 1'$, and $1'$, we have $\vdash 1 = 1'\colon G$.

This formalises the equational proof $$1 = 1 1' = 1' ,$$ only noting explicitly where the properties of equality and the group axioms are used.

I carried out this proof in the empty context, but I could just as well have done it in an arbitrary context $\Gamma$. Sometimes it's nice to do that explicitly; just write ‘$\Gamma$’ before every ‘$\vdash$’ in the explicit proof above. But also, there is a metatheorem that any equational identity in the empty context is valid in every context; more generally, any equational identity valid in some context $\Gamma$ is also valid in any context that is built from $\Gamma$ by any number of extensions. This metatheorem can be proved by structural induction on the ways in which equational identities (and hence terms and contexts) are constructed.

Here is another theorem, that the inverse of a product is the product of the inverses in the opposite order. I will formalise this argument:

$$(x y)' = (x y)' 1 = (x y)' (x x') = ((x y)' x) x' = (((x y)' x) 1) x' = (((x y)' x) (y y')) x' = ((((x y)' x) y) y') x' = (((x y)' (x y)) y') x' = (1 y') x' = y' x' .$$

• As always, $\epsilon$ is a context.
• Extending by a new variable twice, we have the context $\mathrm{x}_0\colon G, \mathrm{x}_1\colon G$; but I'll write this $x\colon G, y\colon G$ instead.
• Since ${|\epsilon|} = 0$, we have ${|x\colon G|} = 1$ and ${|x\colon G, y\colon G|} = 2$, so we have the terms $\mathrm{x}_0$ and $\mathrm{x}_1$ in the last context. But again, I'm writing these differently, so it comes out like this: $x\colon G, y \colon G \vdash x\colon G$ and $x\colon G, y \colon G \vdash y\colon G$.
• Now I can also build more terms:
  • $x\colon G, y\colon G \vdash x y\colon G$;
  • $x\colon G, y\colon G \vdash (x y)'\colon G$;
  • $x\colon G, y\colon G \vdash 1\colon G$;
  • $x\colon G, y\colon G \vdash (x y)' 1\colon G$;
  • etc, ultimately building all of the terms that appear in the long equation above.
• Then I start building the equational identities:
  • $x\colon G, y\colon G \vdash (x y)' = (x y)' 1$ by the left unit law;
  • $x\colon G, y\colon G \vdash x x' = 1$ by the right inverse law;
  • $x\colon G, y\colon G \vdash 1 = x x'$ by symmetry;
  • $x\colon G, y\colon G \vdash (x y)' 1 = (x y)' (x x')$ by right substitution into a product;
  • etc, etc, etc, finishing with $8$ applications of transitivity.

But we could also formalise this by working in an arbitrary context $\Gamma$ and using any two arbitrary terms (not necessarily variables!) $\Gamma \vdash x\colon G$ and $\Gamma \vdash y\colon G$. Then the same argument works, only writing $\Gamma$ in place of the context $x\colon G, y\colon G$ (and skipping the beginning where I derive that $x$ and $y$ are terms in that context). Once again, there is a metatheorem that anything that can proved one way can also be proved the other way.

Finally, consider the theorem that the inverse of a commutative product is the product of the inverses in the same order. That is, if $x y = y x$, then $(x y)' = x' y'$. The argument is $$(x y)' = (y x)' = \cdots = x' y' ,$$ where the dots are filled in the same way as in the previous argument (only with $x$ and $y$ swapped). To formalise this, we work in the context $x\colon G, y\colon G, x y = y x$; that is, our context now consists of two free variables and an equation stating that they commute. Alternatively, we formalise the argument in an arbitrary context $\Gamma$ with arbitrary terms $\Gamma \vdash x\colon G$ and $\Gamma \vdash y\colon G$, such that $\Gamma \vdash x y = y x\colon G$ is valid.

Of course, having just proved $x\colon G, y\colon G \vdash (x y)' = y' x'\colon G$, it's silly to go through the entire proof of $x\colon G, y\colon G, x y = y x\colon G \vdash (x y)' = x' y'\colon G$. Instead, we should use the previous result in the course of proving this new one. We actually cannot do so directly, since $(x y)' = y' x'$ is irrelevant; it's $(y x)' = x' y'$ that we need. However, suppose that we take the broader view, in which we have proved that $\Gamma \vdash (x y)' = y' x'$ is valid in any context and any two terms in that context. Then we are OK: if we take $\Gamma$ to be $x\colon G, y\colon G, x y = y x\colon G$, take $x$ to be $y$, and take $y$ to be $x$, then we have $x\colon G, y\colon G, x y = y x\colon G \vdash (y x)' = x' y'\colon G$, and a single application of transitivity gives us the new theorem.

In fact, we can think of the arbitrary-context versions of these three theorems as derived rules: $$\array { \frac {} {\Gamma \vdash 1 = 1'\colon G} \\\\ \frac {\Gamma \vdash a\colon G \qquad \Gamma \vdash b\colon G} {\Gamma \vdash (a b)' = b' a'\colon G} \\\\ \frac {\Gamma \vdash a\colon G \qquad \Gamma \vdash b\colon G \qquad \Gamma \vdash a b = b a\colon G} {\Gamma \vdash (a b)' = a' b'} }$$ Then we use the second derived rule in the proof of the third; more generally, we can use a derived rule to shorten any later proofs.

Well, this is all very long and tedious, but that is not really the fault of type theory as such, but rather of formal logic. Any way of making completely formal the equational reasoning of elementary group theory would be just as long and tedious. One reason that people don't ever write down anything so long and tedious when describing group theory is that they take basic logic for granted. Here I have spelt out that logic — and it is only a very weak logic! (In my next post, I hope to go beyond the equational theory of a group to describe the first-order theory of a group, spelling out a more powerful logic that allows us to state things such as ‘Only the identity equals its inverse.’ as a hypothesis and prove consequences of it. You can't do that in the equational theory.)

The benefit of taking logic for granted is obvious. But the benefit of spelling it out in so much detail is flexibility. The equational theory of a group can be interpreted in any category with finite products, after all, while first-order logic requires more. And you can even take completely different approaches to logic, as with propositions as types or Mike's $2$-logic.