Map Colorings in Type Theory

Type Operators

Consider a type operator $Foo : \rset \x \rset \to \rset$. What are some things it can be? It could be, for example \[ Foo = \lambda (A, B) . A + A + A + B + B \] or \[ Foo = \lambda (A, B) . B \] or \[ Foo = \lambda (A, B) . 1 \] or \[ Foo = \lambda (A, B) . A \x B + A + 3 \] or lots of other things. I'm going to restrict my attention to examples more like the first two, and depict them in the following way:


$ Foo = \lambda (A, B) . A + A + A + B + B $	$ Foo = \lambda (A, B) . B $

The intuition behind these pictures is this: $A$ and $B$ are knobs that we can turn. We can set them to a type that has any number of elements we like. We can replace every occurrence of the $A$ and $B$ in the diagram with a copy of the input type, and we'll get a picture of the type the type operator outputs. For example, if we set $A$ to 2 and $B$ to 3, we get


$2 + 2 + 2 + 3 + 3 $	$ 3 $

Higher Type Operators

We can get even fancier if we allow type operators to build their output using higher inductive types from homotopy type theory. For example, we might write the type $ Foo = \lambda(A, B) . A + A + A + B + B$ in pseudo-Agda as

    data Foo (A B : Set) : Set where
        injA1 injA2 injA3 : A → Foo A B
        injB1 injB2 : B → Foo A B

but beyond that we could imagine adding equations between elements, perhaps a different type

    data Bar (A B : Set) : Set where
        injA1 injA2 injA3 : A → Bar A B
        injB1 injB2 : B → Bar A B
        path1 : (a : A) → injA1 a ≡ injA2 a
        path2 : (a : A) (b : B) → injA3 a ≡ injB2 b

and we might visualize this as

If we can introduce equations, we can make the blobs in the picture "adjacent" to one another.

More Inputs

Let's look at a couple examples of some type-operators that take three inputs.

data Line (A B C : Set) : Set where
    injA : A → Line A B C
    injB : B → Line A B C
    injC : C → Line A B C

    pathAB : (a : A) (b : B) → injA a ≡ injB b
    pathBC : (b : B) (c : C) → injB b ≡ injC c

data Tri (A B C : Set) : Set where
    injA : A → Tri A B C
    injB : B → Tri A B C
    injC : C → Tri A B C

    pathAB : (a : A) (b : B) → injA a ≡ injB b
    pathBC : (b : B) (c : C) → injB b ≡ injC c
    pathAC : (a : A) (c : C) → injA a ≡ injC c

    higher-path : (a : A) (b : B) (c : C) →
        pathAB a b • pathBC b c ≡ pathAC a c

We have constructed the type Line as three blobs connected to one another in a line. The set $A$ might have any number of elements, and the set $B$ might have any number of elements, but any pair of them has a path equating the $a$ and the $b$. Likewise any $b$ and any $c$. It might seem like any $a$ and any $c$ have to be equal, by the fact that we can compose any two paths in HoTT, but this conclusion is premature --- we don't actually know that our input $B$ will have any inhabitants! So the topology of the type operator Line is revealed by the fact that although \[\mathrm {Line}\ 1\ 1\ 1 \equiv 1\] — that is, the line is just one contractible blob isomorphic to the unit type if all of the arguments $A, B, C$ are the unit type — we have nonetheless that \[\mathrm {Line}\ 1\ 0\ 1 \equiv 2\] If we set $B$ to the empty type, then the result is the type with two elements.

On the other hand, we have \[\mathrm {Tri}\ 1\ 1\ 1 \equiv 1\] and also \[\mathrm {Tri}\ 1\ 0\ 1 \equiv 1\] ! So at least we know that $\mathrm{Tri}$ and $\mathrm{Line}$ are different, even if you don't believe my diagrams.

More General Maps

We can now see how, in a univalent universe, a type operator $F : \rset^n \to \rset$ could contain the data of not just "how many times" its arguments are summed, but also a lot of topological information about how they're glued to one another — it's something like, a map (in the sense of "all planar maps are 4-colorable") with $n$ countries in it. Quite possibly some kind of further regularity/parametricity constraints need to be imposed to actually require planarity or to exclude pathological cases, but let's say provisionally that for any index set $I$ that

A map with countries indexed by $I$ is a functor \[ \mu : (I \to \rset) \to \rset \] such that $\mu(\lambda j . i \equiv j)$ is a contractible type for every $i : I$.

The idea is that the $I$-indexed set of type $(I \to \rset)$ generalizes our ability to "turn on" and "turn off" the presence of any particular country, and "read off" how many connected components there are (actually: read off the homotopy equivalence class of just those countries) in the resulting sub-map.

For example, our map might be a functor \[\mu : (\{A,B,\ldots, M,N,O\} \to \rset) \to \rset \] depicted by

and if we plugged in a specific family of sets \[\mathbf F : (\{A,B,\ldots, M,N,O\} \to \rset)\] where \[ \F(A) = \F(B) = \F(C) = \F(E) = \F(F) = \F(G) = \F(M) = \F(N) = 1\] and $\F(x) = 0$ otherwise, we would find that $\mu(\F)$ would be the type $S^1 + 2$:

The condition that $\mu(\lambda j . i \equiv j)$ is saying that if we "enable"/"turn on" a single country by setting its type input to 1 and every other type's input to 0 (at least this is what is happening if the indexing type $I$ is a mere set!) then the "area that the country takes up on the map" is actually a contractible region.

Map Colorings

The set $I$ is essentially the set of "names" of the countries in a map. A coloring of a map is a function $k : I \to C$ from country names to a set $C$ of colors, such that no two adjacent countries have the same color. It came as a surprise to me that there's a very slick HoTT-flavored way of expressing this constraint.

Suppose we have an $I$-map $\mu : (I \to \rset) \to \rset$ and a color assignment $k : I \to C$. Notice that there is a fairly evident way of building a value of type \[ I \to \sum_{c: C} \mu(\lambda j . c \equiv k(j))\] What will this map do? It takes a country name as an input. It's going to generate a value in the $k(i)$ branch of the $\sum$ over $c : C$. So it's going to generate a dependent pair — whose first component we just said was $k(i)$, and whose second component must be of type \[ \mu(\lambda j . k(i) \equiv k(j)) \] But here's a fact: we know that $\mu(\lambda j . i \equiv j)$ is inhabited, because in fact $\mu$ being a map means it's contractible. And $\mu$ is a functor, and we can certainly get from $i \equiv j$ to $k i\equiv k j$, (because we can apply functions to paths), so we can get from $\mu(\lambda j . i \equiv j)$ to $\mu(\lambda j . ki \equiv kj)$. This finishes the argument that there is a reasonable function of type \[ I \to \sum_{c: C} \mu(\lambda j . c \equiv k(j))\] What is this function expressing? It's the map from the set of country names into a type that is constructed by considering each color in turn, and adding in a type that consists of what you get when you "enable"/"turn on" all the countries that have that color. But any countries in this process that are adjacent to one another and which have the same color in the coloring will be "glued together"! So we make the definition:

A coloring of an $I$-country map $\mu$ with colors from $C$ is a map $k : I \to C$ such that the evident induced function \[ I \to \sum_{c: C} \mu(\lambda j . c \equiv k(j))\] is an equivalence.

We can see in the non-example of a coloring

that it fails to be a coloring because $A, B \in I$ map to the same point in \[\sum_{c: C} \mu(\lambda j . c \equiv k(j))\]

Planarity

I'd love to be able to make a clever "synthetic" restatement of the four-color theorem at this point, but I'm not quite sure how to enforce that maps are planar! However tempting it is to lean on the HoTT interpretation of the 2-sphere, I'm pretty sure it's not good enough to say

A map $\mu$ is planar iff $\mu(\lambda \underline{\ }.1)$ is equivalent to the type $S^2$.

What's happening here is I'm trying to express the idea of erasing country labels, and recovering the underlying space the map is taking place on by setting all the countries' "multiplicity" to 1 — that is, by passing the function $\lambda \underline{\ }.1$ to the map $\mu$. Now for sure a planar map should have this property, but I think it's insufficient — I think you could layer countries "on top of" other countries, leading to more adjacencies than a planar map should allow, while still retaining the property that the "erased" map still has the homotopy type of $S^2$.

However! I think doing this would require a higher inductive type with clauses that postulate the existence of paths-of-paths-of-paths to adequately "glue together" these extra illegal countries made up only of airspace. And this seems like an intrinsically "3-dimensional" thing to do. So maybe we can forbid it?

Conjecture Template: Suppose $\mu$ is a sufficiently well-behaved functor of type $(I \to \rset) \to \rset$, and $I$ is a finite mere set. "Well-behaved" includes at least that

$\mu$ is a map
$\mu$ is built up inductively only from injections, paths between injections, and paths-between-paths-between-injections, in some suitable sense.
$\mu(\lambda \underline{\ }.1) \cong S^2$
Then there exists a coloring $I \to 4$ of $\mu$.