What is realignment and is it useful in non-univalent theories?

Question

From my rough understanding, an (external/internal) realignment property says that given a type $A$, a proposition $p : \Omega$, and a partial isomorph $B : p \to \sum_{A'} A' \cong A$, we can extend it to a total one, such that it is strictly equal to $B$ given that $p$ is true.

Sterling et al. used this technique when building models for cubical type theories. However, in Sterling's thesis, he also extensively used realignment to adjust various definitions when setting up Tait's computibility for MLTT.

I cannot (yet) fully appreciate the power of realignment. It seems to resemble the cubical gluing operation, so I'd expect it to be useful there. But is it necessary (or to put it another way, does it greatly simplify various arguments) for non-univalent type theories?

More specifically, even if assuming the realignment property holds in some topos helps, we still need to prove this property when actually instantiating a concrete topos, right? I cannot locate such a proof anywhere in Sterling's thesis, perhaps there's something that I overlooked? Any help is appreciated!

Answer 1

This is a very good question.

What is realignment for?

One application of realignment that is particularly useful is to construct a cumulative hierarchy of universes; what cumulativity means in the "objective" sense is that you have a hierarchy U1 >-> U2 >-> U3 ... where each coercion is injective, and you have a choice of type operations at each level i like Pi_i x:A. B(x) such that the coercion from Ui to Uj commutes with the chosen type operations. It is semantically very hard to get this to happen!

Realignment is, however, much stronger than cumulativity; so if you have a hierarchy of universes linked by injective coercions but you have chosen type operations that do not commute with these operations, realignment can be used to replace all these type operations with ones that do commute with the coercions.

The cumulativity example is nice --- since if you have realignment in a sheaf topos (which we, in fact, do have in every sheaf topos as I will explain in the second half of my answer) then we have a strict interpretation of full MLTT with cumulative universes. Thus we can use a very naive denotational semantics to prove a variety of independence results for MLTT quite easily. This contradicts almost a decade of regrettable misinformation and confusion on the topic of universes in sheaf topoi.

In addition to cumulativity, realignment is, as you point out, the critical ingredient for constructing univalent universes in models of homotopy type theory. It is also useful for synthetic Tait computability, as you mention. Can we find uses for it in "ordinary" work-a-day type theory? My work recently has focused on finding applications for the modalities of synthetic Tait computability that have nothing to do with Tait computability --- for instance, the cost aware logical framework and my recent account of type based security/information flow control with Bob Harper. In these cases, we can imagine a type theory where realignment would play some useful role internally --- i.e. a new "glue" connective that lets you make a type that restricts up to definitional equality to some other type underneath a certain security level or phase, etc. It's unclear how useful this will be, but it could be useful.

What models of realignment do we have?

Your other question about whether you can in fact validate realignment in semantic models is also excellent. The state of play is that so long as your ambient mathematical universe is boolean (as $\mathbf{Set}$ is), then any Grothendieck topos has a hierarchy of universes satisfying realignment. This is proved by Daniel Gratzer, Mike Shulman, and myself in our recent manuscript Strict universes for Grothendieck topoi --- the results were complete at the time that I claimed "realignment is fine in topoi" in my thesis, but the paper was not ready to be released unfortunately.

There are a number of open questions remaining.

1. Hofmann and Streicher give a simple construction of universes in any presheaf topos, and this is perfectly constructive. However Andrew Swan has proved that this particular universe construction cannot satisfy realignment for all monomorphisms unless the ambient mathematical universe is boolean. Meanwhile Gratzer, Shulman and Sterling have given a different construction of universes that applies in any Grothendieck topos, but their construction is very classical and employs both LEM and AC. Is there a modification of the GSS construction that works constructively and hence over a non-boolean base topos? We expect that the base topos will nonetheless need to satisfy a weak / constructively acceptable choice principle such as WISC.

2. A less ambitious but also reasonable question is whether there is a universe construction specifically for realizability topoi that satisfies realignment, assuming perhaps that we are looking at $\mathbf{RT}(\mathbb{A})$ for a pca $\mathbb{A}$ internal to a boolean topos like $\mathbf{Set}$.

As far as I am aware, both of these questions are open. Daniel and Mike and I tried really hard to find a constructive version of our work, but got stuck.