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.

## Re: Stack Semantics

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

geometricinformation 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.