What is Artin gluing, and how is it useful in proving meta-theoretic properties?

Question

I came across this notion in several places, especially in recent papers that establish important meta-theoretic properties of type theories like CuTT. The entry in nLab focuses on the geometric aspect of it, and although I can follow at the level of topological spaces and maybe locales, I lack sufficient background to understand the following discussions, and fail to see how it relates to type theories.

This link describes a "gluing construction". Is this related to the Artin gluing construction? If so, how?

Answer 1

Here is my attempt at a bird's eye view of what gluing is about. I will not go into the details of the actual gluing construction, and instead refer to the various surveys for this.

Proving meta-theoretical properties of type theories is quite a delicate matter, and everything starts with how you define your type theory.

The syntactical approach

In the approach that is commonly taught to CS students, you start by defining a syntax for contexts, types and terms, and then you devise typing judgments and rules on this untyped syntax.

Now if you want to prove a given property (let's say normalization) for every well-typed term, you have to reason by induction on judgment derivations. In sufficiently complex cases, you will need to heavily reformulate your property so that the induction goes through, and the induction hypothesis you obtain usually involves some binary relations — these are called logical relations and are the traditional way of proving meta-theoretical properties.

The algebraic approach

Category theorists don't like to reason about syntax too much, so when they are studying properties of a given type theory they will usually prefer to shift the focus to a carefully designed category of models for the type theory under scrutiny (such as categories with families or contextual categories). Since the models are usually described as algebras for a sophisticated algebraic theory, general theorems provide you with an initial model $\mathcal{M}_0$ whose objects are generated from the operations and quotiented by the equations of the algebraic theory.

Now it is relatively easier to reason about this initial model compared to the syntax since it has all this algebraic structure. Say you want to prove a property $P$ for the objects in $\mathcal{M}_0$. If you manage to design a model $\mathcal{M}_P$ whose objects are objects of $\mathcal{M}_0$ decorated with a proof of $P$, then you obtain:

• a projection $\pi : \mathcal{M}_P \to \mathcal{M}_0$ that discards the proofs of $P$,
• a morphism $\iota : \mathcal{M}_0 \to \mathcal{M}_P$ from the initiality of $\mathcal{M}_0$, which sends an object $t$ to an object $u$ equipped with a proof of $P(u)$, and
• a proof that $\pi \circ \iota = \mathrm{id}$ from the uniqueness part of the initiality property, which assures you that $t = u$.

Which does provide you with a proof of $P$ for every object in $\mathcal{M}_0$. Of course, a priori the design of $P$ seems to also require some complex reformulation of the property you wanted to prove initially in order for the model construction to go through. But in the case where your models are toposes, it turns out that an already existing categorical construction (that was first studied by geometers) called Artin Gluing allows you to produce such good properties with minimal effort.

The process is described in detail by Michael Shulman on the nCategory café.

The construction can be generalized to very general kinds of models, and retains the name gluing construction in the literature, despite having departed from the original geometric meaning quite a bit. It is basically the functorial version of logical relations.

Relating the two approaches

While the additional structure in the algebraic approach makes some definitions more natural, you should keep in mind that you are in fact reasoning about a different object: the initial model is generated by the operations and equations that define your category of models. Relating this initial model to the one you can construct using well-typed proof terms quotiented by definitional equality is called the initiality conjecture, and is far from trivial.

Answer 2

I would like to post an example that I hope will be illuminating to understanding some concepts in topos theory, and especially Artin gluing. This is a translation and polishing of my own answer a few days ago here. This would include some category basics. I will try to explain some of them, but obviously I can't turn this into a category theory introduction. Nonetheless, the answer will certainly be overly wordy to those who are proficient in category theory, so please do bear with me!

Consider the category $\mathsf{Graph}$, of directed graphs, possibly with self-loops and repeated edges.^[1] The morphisms are graph morphisms, which preserves the incidence relation between vertices and edges. Let's explore the structures in it first. Skip this section if you can do this yourself.

The initial object $0$ is certainly the empty graph. The terminal object is, instead of the one-point graph, a graph with one point and a self loop. Coproducts are easy, by putting two graphs side by side. Products are also standard. The vertex set of $F \times G$ is the cartesian product of the vertex sets of $F$ and $G$. An edge from $(f_1, g_1)$ to $(f_2, g_2)$ corresponds to a pair of edges from $f_1$ to $f_2$ and from $g_1$ to $g_2$, respectively. A good warm up exercise is to verify all these constructions.

The exponential object requires a little bit of thought. I'll give the construction first. The vertices of $F^G$ are graph morphisms from $G$ to $F$, i.e. $\mathrm{Hom}_{\mathsf{Graph}}(G, F)$. The edges are slightly complicated. Let $I = \bullet \! \to \! \bullet$ be a graph with two vertices $\{\mathrm{left, right}\}$ and one edge. The edges of $F^G$ are exactly the set $\mathrm{Hom}_{\mathsf{Graph}}(G \times I, F)$. Each edge $e$ connects the vertices (which are graph morphisms) $e(-, \mathrm{left})$ and $e(-, \mathrm{right})$. The reader is invited to play with this definition and verify that it is indeed the exponential, so as to gain some intuition.^[2]

What would a subobject be? Recall the definition of a subobject of $G$: it's a monomorphism $X \hookrightarrow G$ into $G$, considered up to isomorphism. A subobject in $\mathsf{Graph}$ simply selects some vertices and edges from a graph, but it is required that once you select an edge, you must select its endpoints as well.

Next up, subobject classifiers. To a non-category-oriented person it might sound scary. But the idea is simple: In the category $\mathsf{Set}$ of sets and functions^[3], every subobject (a.k.a. subset) $X \subseteq Y$ is equivalently a function $\chi_X : Y \to \{\mathrm{true}, \mathrm{false}\}$, where $\chi_X(x) = \mathrm{true}$ if and only if $x \in X$. So it classifies elements of the superset according to whether it is included in the subset. How should we describe it in category speak? We need an object $\Omega$ in the place of $\{\mathrm{true}, \mathrm{false}\}$, and we need a morphism $1 \to \Omega$ to "pinpoint" the $\mathrm{true}$. This would create a pullback diagram:

If you are not familiar with this, I strongly suggest you verify my statements. Note that $\Omega = 1 + 1$ in the category of sets. This is the internal principle of excluded middle.

What happens in the context of graphs? It certainly looks strange:

Here, the $\mathrm{true} : 1 \to \Omega$ selects one of the self-loop on the right (let's say on the top-right). Why would it be like that? A subobject classifier classifies the "elements" of the superobject according to whether it is included in the subobject, so there you go:

• If a vertex is not in the subgraph, it corresponds to the point on the left.
• If a vertex is in the subgraph, it corresponds to the point on the right.
• If neither of the two endpoints of an edge is in the subgraph, then this edge is not in the subgraph either. It corresponds to the self-loop on the left.
• If the source endpoint is in the subgraph but the target endpoint is not, then the edge corresponds to the edge from right to left.
• If the target endpoint is in the subgraph but the source endpoint is not, then the edge corresponds to the edge from left to right.
• If both the endpoints are in the subgraph, the edge may also be in the subgraph. If so, it corresponds to the self-loop on the top-right.
• If the edge is not in the subgraph, it corresponds to the self-loop on the bottom-right.

Note that $\Omega \ne 1 + 1$ here.

Next, we finally start to get our hands on topos theory. We define an open to be a subobject $\phi : X \hookrightarrow 1$. This of course induces $\chi_\phi : 1 \to \Omega$. This name comes from geometric intuitions. You can skip this part if you don't know the mathematics.

---

Take the category of sheaves on the real $\mathrm{Sh}(\mathbb R)$. Note that individual sheaves such as all the smooth functions $C^\infty(-)$ constitute the objects of this category. The terminal sheaf assigns every open set the singleton: $1(S) = \{\star\}$. A subobject $\mathcal X$ of this would then assign every open set either the singleton or the empty set. But you can't just take arbitrary assignments. You have to observe the two laws.

• Restriction morphisms (think, a continuous function is still continuous when restricted to a smaller domain). This means if $\mathcal X(A) = \{\star\}$, for all open subsets $B \subseteq A$ we would also have $\mathcal X(B) = \{\star\}$ as well.
• Patching (if you define a continuous function on multiple domains, and prove that these definitions are compatible on intersections, then you can get a big continuous function on the union of these domains). For any open sets $A_\alpha$ such that $\mathcal X(A_\alpha) = \{\star\}$ we have $\mathcal X\left(\bigcup_\alpha A_\alpha\right) = \{\star\}$.

These two laws ensure that there is a largest open set $A$ such that $\mathcal X(A) = \{\star\}$. Therefore the subobjects of $1$ correspond exactly to open sets on $\mathbb R$.

---

Back to our business. What opens are there in $\mathsf{Graph}$? Exactly three: the empty one, the single-point one, and the point-with-self-loop one. The first is $0$, the last is $1$. And we shall study the middle one, dub it $¶$.

Given an open $¶$, since it is a subobject $¶ \to 1$, we can form a morphism between exponential objects $E^1 \to E^¶$ for any $E$. If this morphism is in fact an isomorphism, then we call $E$ to be $¶$-modal. If you read the part about sheaves, you should see that $¶$-modal sheaves are exactly those that are "ignorant" outside the open set $¶$: $\mathcal X(A) = \mathcal X(A \cap ¶)$. Therefore, the $¶$-modal objects in $\mathrm{Sh}(\mathbb R)$ makes up the sheaf on the open subset $¶$. This is why we call it the open subtopos $\mathrm{Sh}(\mathbb R)_{¶}$.

Since we have defined exponential graphs above, let's plug in the definition and see! $E^¶$ is the graph with all the vertices in $E$, but there is exactly one edge between every pair of endpoints. So to have $E \cong E^¶$, $E$ needs to already be such a graph. This means that $\mathsf{Graph}_¶$ is made up of complete graphs.

The acute reader may have notice that no matter what $E$ is, $E^¶$ would have to be isomorphic to $(E^¶)^¶$. This (among other reasons) is why we call it a modality. And we should use a notation that suggests a modality: $⚪E$.

Now that we have an open subtopos, is there a closed subtopos? Of course. We have the projection $E \times ¶ \to ¶$. And if this is an isomorphism, we call $E$ to be $¶$-connected. (Exercise: work out what this means in $\mathrm{Sh}(\mathbb R)$.) In the category of graphs, $E \times ¶$ simply removes all the edges. And the projection maps all the vertices onto the one point $¶$. So in order for this to be an isomorphism, we need that $E$ only has one point in the first place already. So this makes a subtopos consisting of single-point graphs, $\mathsf{Graph}_{\backslash ¶}$.

Is there a corresponding modality $⚫E$ for the closed subtopos? Yes. Appearently we need to "pinch" all the points of a graph together. What operations in category theory pinches together stuff? Well, more or less, coequalizers and pushouts. And these two are more or less equivalent. Since we want to pinch together the points, we first fetch all the points by taking the product $E \times ¶$. Then by taking the pushout $⚫E = E +_{E \times ¶} ¶$, we achieve our goal.

---

There are actually intricate relationships between the two modalities if we try to compose them. For an arbitrary graph, $⚪⚫E$ means to (1) pinch together all the points, and (2) connect each pair of points with exactly one edge. This turns every $E$ into the terminal graph $1$. So our first neat result: $⚪⚫E \cong 1$.

What about composing the other way? $⚫⚪E$ first (1) connects each pair of points with exactly one edge, and (2) pinches together all the points. So this would get us $n^2$ edges on one point. This retains a certain amount of information. But the cool thing is, we have a property called fracture so you can actually recover the whole graph $E$! Consider the pullback

If you forgot what pullbacks are, a quick reminder in the category $\mathsf{Set}$: the pullback of $A \xrightarrow f C \xleftarrow g B$ is $\{(a,b):f(a)=g(b)\}$, or equivalently $\bigcup_{c \in C}f^{-1}(c) \times g^{-1}(c)$. You can try to calculate the upper-left corner, and it would be exactly $E$. Here I'm not going through that. Rather, I would like to give some intuition: $⚫E$^[4] keeps the information about what edges are there, but ignores which vertices are being connected. Conversely, $⚪E$ remembers which vertices are where but forgets about the edges. So the pullback interpolates, or synthesizes the information, reproducing the whole graph.

---

Since for each individual graph, we can recover it from the two modalities, we should expect to be able to recover the whole $\mathsf{Graph}$ topos from the two subtopos $\color{red}{\mathsf{Graph}_¶}$ and $\color{blue}{\mathsf{Graph}_{\backslash ¶}}$. (Sorry for those reading in black and white... But the colors makes the argument much clearer.)

Suppose we are given some random $\color{red}{O} \in \color{red}{\mathsf{Graph}_¶}$ and $\color{blue}{C}\in\color{blue}{\mathsf{Graph}_{\backslash ¶}}$, we can try our best to form a "pullback square":

But of course we need more information. From the diagram it is clear that we at least need a functor $\color{blue}\Phi : \color{red}{\mathsf{Graph}_¶} \to \color{blue}{\mathsf{Graph}_{\backslash ¶}}$, which is intended to be $⚫$, restricted on $\color{red}{\mathsf{Graph}_¶}$. This provides the crucial information of how the two subtopoi "glues" together. ^[5]

We can already form a good candidate category! We define the objects of the Artin gluing $\color{purple}{\mathbf{Gl}}(\Phi)$ to be triples $(\color{red}{O}, \color{blue}{C}, \color{blue}{C \xrightarrow f \Phi(O)})$. The morphisms are the natural ones:

We just need to choose $(\color{red}\theta, \color{blue}\delta)$ so that the parallelogram commutes.

I will not prove that $\color{purple}{\mathbf{Gl}}(\Phi) \cong \mathsf{Graph}$ here. But let's just do a sanity check. Since it's a "gluing" of topoi, we at least need to find out where did the subtopoi go, right? Since $E = ⚪E$ for $¶$-modal objects, the pullback diagram for $E$ in the open subtopos becomes:

where the arrow on the right is actually $\mathrm{id}$. So we found the open subtopoi: The full subcategory with objects of the form $(\color{red}{E}, \color{blue}{\Phi(E)}, \color{blue}{\Phi(E) \xrightarrow {\mathrm{id}} \Phi(E)})$.

Similarly we draw the diagram for $¶$-connected objects:

This suggests that the closed subtopos contains the objects $(\color{red}{1}, \color{blue}{E}, \color{blue}{E \xrightarrow {!} 1})$^[6].

---

So we went through three steps here:

1. We defined the open/closed subtopoi of an open.
2. We reconstructed the original topos, through Artin gluing.
3. We found the two subtopoi in the glued topos.

The interested reader can go on to prove $\color{purple}{\mathbf{Gl}}(\Phi) \cong \mathsf{Graph}$. Further reading here.

Now for some more geometry! As pointed out in the footnotes, $\mathsf{Graph} \cong \mathrm{Psh}(\bullet \rightrightarrows \bullet)$ is a simple presheaf category, which is a special case of sheaves (with a trivial Grothendieck topology). We can take all the sheaves together^[7] and form a category. What should our morphisms be? A geometric morphism is a functor $F : \mathcal C \to \mathcal D$ that preserves all the finite limits and all colimits. (Does that remind you of something? In pointset topology, we have that "finite intersections and all unions" condition on open sets, right?) If that is the case, then by abuse of notation we say $F$ is a geometric morphism from the topos $\mathcal D$ to $\mathcal C$. Note the reversal! In topology, a continuous function $f : X \to Y$ is one that maps the open sets of $Y$ to $X$. So there's a similar reversal here. To emphasize our shift of perspective from categories to topoi, we sometimes write the category $\mathcal C$ as $\mathsf{Set}_{\mathbb C}$, and when it's considered as a topos, we write it as $\mathbb C$.

The terminal topos $\mathbb 1$ is --- considered as a category --- $\mathrm{Psh}(1)$, which is just $\mathsf{Set}$.

Another important topos is the Sierpiński topos $\mathbb S$, such that $\mathsf{Set}_{\mathbb S} = \mathsf{Set}^{\to}$, whose objects are arrows in $\mathsf{Set}$, and morphisms are commutative squares. This name comes from the Sierpiński topology, which is a topology on a two-point space $\{\bullet, \circ\}$, where $\{\circ\}$ is open, and $\{\bullet\}$ is closed. As an exercise, find out about the topos-theoretic opens in $\mathbb S$. (In case you've forgotten, an open is defined to be a subobject of the terminal object.)

Since $\mathsf{Set}_{\mathbb S}$ consists of arrows, we have a functor $\mathsf{dom} : \mathsf{Set}_{\mathbb S} \to \mathsf{Set}$ that takes the domain of the arrows. You can verify that it preserves all colimits and finite limits,^[8] and similarly for $\mathsf{cod}$ This means we have geometric morphisms $\mathbb 1 \stackrel{\circ, \bullet}\rightrightarrows \mathbb S$, which looks exactly the same as our Sierpiński topological space. We can then throw in the topoi that we want to glue:

I shall leave the question of why this is the Artin gluing as I previously defined as an exercise. (Hint: rewrite everything as categories instead of topoi, remember the reversal.)

Footnotes

1. This would make the category $\mathsf{Graph} \cong \mathrm{Psh}(\bullet \rightrightarrows \bullet)$ a special case of a presheaf category.

2. Where does this weird definition come from? As pointed out in the previous footnote, we have a presheaf category, and so we can reason that the exponential object $E$ (if exists) must satisfy $E(c) \cong \mathrm{Hom}(よ(c), E) \cong \mathrm{Hom}(よ(c)\times X, Y)$, taking $よ$ to be the Yoneda embedding.

3. I'm assuming the law of excluded middle for the sake of presentation.

4. Actually, $⚫E$ together with the morphism $⚫E \to ⚫⚪E$, same for $⚪E$.

5. Not every $\Phi$ works, it needs to be left exact, i.e. preserving the terminal object and pullbacks. This actually means that $\Phi$ preserves all finite limits. The name "exact" is used in commutative algebra, so no need to be worried about it.

6. Here left exactness is used.

7. Modulo conditions that prevent the Russel's paradox here and there. I won't mention them below, but keep in mind that they are very necessary!

8. A quick way to confirm this is to find an adjoint. In fact, there's a chain $\mathsf{cod} \dashv \mathrm{id_{(-)}} \dashv \mathsf{dom}$.