Thoughts on the Coherence Problem

The coherence problem is one of the most frustrating aspects of homotopy type theory. Our types can have higher homotopical structure in arbitrary dimension, but to control that structure can require a seemingly inexpressible infinite tower of coherence conditions. An important example of this problem is the definition of \(\infty,1\)-category, in which the coherence conditions are associahedra of endlessly growing dimension.

As of 2025, it is an open problem to determine whether or not these towers of coherences are expressible in standard homotopy type theory. The most effective solution has been to work around the problem, designing related type theories which do suffice to express these coherences. But these type theories are always more complicated than HoTT, so it's not a fully satisfying answer.

I've thrown a few attempts at the problem myself, and learned some things in the process. Here are my thoughts.

An Intermediate Problem

Typical examples of the coherence problem are semisimplicial types or \(\infty,1\)-categories. These are the hardest examples; solving them would solve the full problem. They're "coherence-hard", to stretch the terminology.

But what are the easiest examples? What's the simplest thing that doesn't seem to be possible?

Functors from \(\omega_1\) to sets.

Functors \(\omega \to \mathbf{Set}\) are easy. \[(A : \mathbb{N} \to \mathbf{Set}) \times ((n : \mathbb{N}) \to A n \to A(n+1))\] Functors from countable ordinals can be defined in terms of functors from \(\omega\), at least given enough choice. But when we reach the first uncountable ordinal, we seem to be out of luck.

So, if we're trying to prove the coherence problem is unsolvable, this would be a good place to look for a counterexample.

The appearance of \(\omega_1\) sparks an idea. If types are like spaces, and equations are like paths, what would the "long line" type be like? Could we somehow build a model that gets "confused" about the nature of this space once we add semisimplicial types, thereby proving HoTT doesn't support them?

Type Theory in Type Theory

As this blog post describes, one way to attack the coherence problem would to implement homotopy type theory in itself, along with its standard model.

The blog post makes a big deal of requiring untyped syntax as input. I think this is a red herring.

Suppose we had a reasonable typed syntax for homotopy type theory. Then, we would be able to:

• Interpret it in \(\mathrm{Type}\).
• Interpret it in the arrow category, \((A : \mathrm{Type}) \times (B : \mathrm{Type}) \times (A \to B)\).
• By internalizing the above construction, transform an interpretation into any category into an interpretation into the corresponding arrow category.
• Iterate transfinitely.

The result is a type of coherent infinite cubes of sets and functions. This has a complicated coherence structure which I don't have a way to produce otherwise.

The blog post discusses untyped syntax. But even typed syntax leads to complicated coherence structures, so the untyped-to-typed translation is less important than the post makes it out to be.

One other point worthy of note: it's absolutely possible to implement nonstandard models of HoTT in HoTT. If the metatheory has induction-recursion, and the inner theory doesn't have HITs, it's actually pretty easy. This does not solve the coherence problem, but it gave me false hope for a while.