« Home

Person. Rafaël Bocquet [rafaëlbocquet]

Eötvös Loránd University
https://rafaelbocquet.gitlab.io/

Backlinks

Disentangling unification and implicit coercion [01JQ]

January 27, 2026
Jon Sterling

It’s well known that unification and subtyping don’t play well together, even in the setting of bidirectional elaboration; the problem, as Amélia Liao very helpfully outlined is scheduling. The problem is essentially that we cannot resolve a coercion problem $\gamma \colon \alpha \lhd A$ by solving $\alpha :\equiv A, \gamma :\equiv 1_A$ because this is not the most general solution: it is in fact the least general solution, considering that $(A,1_A)$ is the terminal object of $\mathbf {Type}/A$ . When you start choosing non-general solutions to things, the process becomes sensitive to the order in which things were solved, which leads to unpredictable and therefore unreliable behaviour for the user.

What do we currently do?

January 27, 2026
Jon Sterling

In a usable proof assistant, nonetheless, it is table stakes to have both unification (for filling in implicit arguments) and some kind of implicit coercion mechanism (for handling universe cumulativity, as well as forgetful coercion between algebraic structures). These are two of the most difficult aspects of a proof assistant to get right, and we don’t actually have any prior art for a dependently typed system getting both right at the same time:

Rocq’s coercion mechanism is very predictable but its unification is not.
Both Lean and Agda have somewhat dodgy unification and coercion.

Even worse, this is one situation where even if a system had both reliable unification and reliable implicit coercion at the same time, the combination of the two would invariably be unreliable for the reason I stated. What can be done about this?

What can we do?

January 27, 2026
Jon Sterling

I believe the problem cannot be solved without changing the language. The issue is that computing canonical coercions and solving unification problems are actually different processes that have different invariants, but nonetheless interact with each other: making progress on a unification problem can unlock a postponed coercion problem, and resolving a coercion can unlock a postponed unification problem. The results of the combined process is very sensitive to the order in which these operations are performed. In such a situation, there is no choice but to put the matter in front of the user.

First, get the unifier in order

January 27, 2026
Jon Sterling

My proposal is to first treat unification properly. We do the standard bidirectional elaboration where the mode shift calls the unifier; our unifier could do anything, but in recognition of the importance of reliability we will emit only most general unifiers within a predictable fragment of the language. For the unifier, I am eagerly following the very interesting recent work of András Kovács and his collaborators:

András Kovács and Rafaël Bocquet proposed nested pattern unification a few years back, elegantly improving Miller’s pattern unification to interact better with record types.
Very recently, András Kovács has given a very interesting proposal to use ideas from Observational Type Theory to handle postponed unification problems.

Second, embrace casts!

January 27, 2026
Jon Sterling

With the unifier in place, we now add a single construct to the language: cast M. The rule for cast M is a variation on the mode shift that calls the implicit coercion resolver instead of the unifier. The user doesn’t have to write the types involved in the cast, but the user does have to indicate that they intend a cast to be employed. The impact on users is that the “dream code” results in a type error:

bad : _ -> Monoid * Semigroup
bad X := (X, X)
// Error: expected Monoid == Semigroup

But if you add an explicit cast, the code works:

good : _ -> Monoid * Semigroup
good X := (X, cast X)

With my proposal, the user is in control of how unification and coercion interact. The user is in some sense intentionally orchestrating unification problems whose solution will unlock the coercions they want to fire. Because the unifier and the coercion preorder are individually well-behaved, the composite system is well-behaved with respect to user intentions.

There is a final very interesting wrinkle: the coercion mechanism can actually call the unifier. This is because the appropriate canonical coercion between theory refinements is a downcast, i.e. a cast that involves checking an equation:

downcast : (X : Monoid) -> {Semigroup | car => _}
downcast X := cast X

In the above, the placeholder _ gets elaborated to a metavariable ?0:Type, and the implicit coercion mechanism chooses the forgetful coercion from monoids to semigroups and emits the unification constraint ?0 ~ X.car.

Is it good enough?

January 27, 2026
Jon Sterling

Obviously it’s not the dream code we were hoping for, but I think that under the circumstances it is not so bad to have to write the word cast once in a while. We can probably also even come up with a more succinct notation for it (I’m open to ideas!).

That‘s all for tonight! Thanks to András Kovács, Carlo Angiuli, and Amélia Liao for acting as sounding boards at times.

Shall we strictify some homotopy propositions? [01I6]

October 7, 2025
Jon Sterling

Definitional proof-irrelevance is all the rage these days. Unfortunately, I think the present state of affairs is not so good. Most systems that implement some form of definitional proof irrelevance do so by means of a separate universe, which I will call sProp, whose types all have the property of being definitionally proof-irrelevant. From there, different systems have chosen different trade-offs.

Choose one: expressive enough or syntactically well-behaved [01I8]

October 7, 2025
Jon Sterling

In Lean, the definitionally proof-irrelevant propositions are made extremely expressive. This includes not only impredicative quantification, but also inductively defined sProp-valued predicates that additionally satisfy large eliminations with the associated computation rules. Although definitional proof-irrelevance is convenient, including these kinds of computation rules is highly destructive to the syntax of the type theory; in particular, it destroys the decidabiltiy of type checking in ways that are not only theoretical but actually noticeable to users.

On the other hand, Rocq and Agda both implement a more restricted version of sProp that ensures the good syntactic properties of the system are preserved. Unfortunately, I have come to believe that these restrictions render sProp quite a bit less useful than expected, except as a low-level tool for constructing amazingly coherent definitions under the hood (such as Pédrot’s strict encoding of presheaves). There are many angles to this problem (which can make it difficult to discuss), but one aspect is the lack of a unique choice principle that allows you to get out from under a “strict squash type” when it is semantically justified to do so. The lack of unique choice means that the notion of image, crucial for everyday mathematics, is going to be extremely badly behaved. Either way, the restrictions employed in Rocq and Agda’s versions of sProp make it a very poor fit for encoding the mathematical concept of a truth value, not only for classical mathematics, but also for both predicative and impredicative constructive mathematics.

There was a great thread by Amélia Liao on this topic from the point of view of univalent foundations, which I link to here, but I would like to emphasise that the problems with the restrictive version of sProp are not specific to univalent foundations.

As Amélia says, the best-behaved notion of proposition is the homotopy proposition, i.e. a type whose elements can all be proved equal. This fact is not at all specific to univalent foundations: even in non-univalent settings (such as those satisfying UIP), the homotopy propositions are the real propositions, and if you are going to have a separate syntactically-defined universe of propositions like sProp and you want it to be usable for general purpose mathematics, it needs to be (weakly) equivalent to the collection of homotopy propositions (it is OK if there is some stratification in size, for the predicativists in the room). This important relationship between sProp and homotopy propositions does hold in Lean, but it does not hold in Rocq or Agda.

Why is definitional proof irrelevance still useful? [01I7]

October 7, 2025
Jon Sterling

My sad story above might lead you to believe that I don’t recognise the utility of definitional proof irrelevance, but I really do. I think the main point of definitional proof irrelevance is that if you are comparing structures with laws (e.g. monoids or categories), you never have to worry about two “almost equal” structures being off by a proof of an axiom.

A down-to-earth example that comes up frequently is when programming and proving with subset types; it is not at all difficult to get into a scenario where you have two elements of $\{x:A\mid P[x]\}$ whose $A$ components are definitionally equal but whose proof components are not. I have this happen with some frequency when formalising mathematics in univalent foundations.

Now, in univalent foundations it often happens that proofs of propositions can contain important computational content. But sometimes (as in the case of monoid laws), they definitely don’t. It would be nice to be able to pick and choose which things to treat proof-relevantly as an engineering practice, but it is necessary that these choices do not have unintended semantic consequences (as they currently do in Rocq and Agda).

Two proposals for well-adapted proof-irrelevance in UF [01I9]

October 7, 2025
Jon Sterling

I will offer two proposals for a well-adapted version of definitional proof irrelevance that can be incorporated into univalent foundations. The definition of “well-adapted”, for me, is that it must not introduce a new kind of proposition that is not equivalent to homotopy propositions. As soon as you do that, you have to start being forced to make bad but highly consequential choices between whether something should be a strict proposition or a homotopy proposition, and I believe that only a system in which the two are identified (up to even a very weak notion of equivalence) is practical for general mathematics.

My two proposals both have trade-offs. The first one is very strong and relies on an unproven conservativity conjecture, but if that conjecture is proved, formalised proofs in the resulting system would imply results in even the future elementary higher toposes. The second notion is a little less expressive, but can already be interpreted into any Grothendieck $\infty$ -topos over $\mathcal {S}$ , the $\infty$ -topos of spaces.

Proposal. An equivalence between `sProp` and `hProp` [01IA]

October 7, 2025
Jon Sterling

This one was suggested to me half a decade ago by Ulrik Buchholtz. The idea is to freely extend homotopy type theory with an abstract universe sProp together with an equivalence from sProp to hProp, such that every P: sProp is definitionally proof irrelevant.

(This system is distinct from the one that simply asserts that every P: hProp is definitionally proof-irrelevant. This latter theory is far stronger and actually derives UIP (and in some formulations, equality reflection!), and is therefore inconsistent with univalence.)

The status of the proposed theory is that it is very likely conservative over Homotopy Type Theory. Rafaël Bocquet has conjectured as much, and has spent several years developing the semantic machinery that would make it possible to prove this result. But today it remains a conjecture.

Proposal. An operation to strictify any given homotopy proposition [01IB]

October 7, 2025
Jon Sterling

An alternative approach occurred to me last night. Instead of asking for a universe of strict propositions that is equivalent to hProp, we could instead ask for a “strict replacement” operation on homotopy propositions that takes a homotopy proposition $P$ and truncates it to an equivalent strict proposition $[P]$ .

I am grateful to Daniel Gratzer for pointing out to me that this strict replacement operation can be intepreted in any Grothendieck $\infty$ -topos model of HoTT, and the proof works by adapting Mike Shulman’s proof of propositional resizing in type theoretic model toposes. In Proposition 11.3 of op. cit., Mike shows that in a suitable model $\mathcal {E}$ , any $-1$ -truncated fibration $X\to Y$ can factored as a weak equivalence followed by a monic fibration. In our specific case, we will consider the projection fibration $\mathsf {hProp}_\bullet \xrightarrow {\pi } \mathsf {hProp}$ that corresponds to the type family $P : \mathsf {hProp} \vdash \pi _1(P)\ \mathit {type}$ . So we have the following factorisation:

\mathsf {hProp}_\bullet \xrightarrow {\sim } \mathsf {hProp}_\circ \xhookrightarrow {} \mathsf {hProp}

We now consider the scenario in which we have a homotopy proposition $\Gamma \vdash P:\mathsf {hProp}$ ; in particular, we construct the following pullbacks:

Evidently the upper right-hand map is a fibration, which means that we actually obtain an honest type $\Gamma \vdash [P]\ \mathit {type}$ . The left-hand factor of the upstairs map corresponds to a squashing map $P\to [P]$ over $\Gamma$ , and we want this map to be an equivalence. Daniel Gratzer was kind enough to point out an argument due to André Joyal, reported by Mike Shulman in Lemma 7.2 of Univalence for Inverse EI Diagrams, that will do the trick (with a small adaptation).

Proof.

October 7, 2025
Jon Sterling

We consider the general scenario:

We wish to show that if $i$ is a weak equivalence, then so is $j$ . The map $p$ factors as a trivial cofibration followed by a fibration. Therefore, by the pullback pasting lemma, it suffices to prove the implication when $p$ is a trivial cofibration, and when $p$ is a fibration.

For the latter, if $p$ is a fibration, then so is $q$ . By the Frobenius condition for right proper model categories, the pullback of a weak equivalence along a fibration is a weak equivalence. Therefore $j$ is a weak equivalence.

Now, if $p$ is a trivial cofibration, then so are $q$ and $r$ , and thus $ir = qj\colon X\to B$ is a weak equivalence. By the three-for-two property of weak equivalences, we conclude that $j$ is a weak equivalence.

To summarise, we have an operation $P:\mathsf {hProp}\vdash [P]\ \mathit {type}$ that sends any homotopy proposition to an equivalent definitionally proof-irrelevant type. In terms of universes, rather than introducing an entirely new universe of strict propositions, we instead provide a new decoding family to $\mathsf {hProp}$ .

Implications for Project Pterodactyl [01IC]

October 7, 2025
Jon Sterling

In the proposals above, we obtain an axiomatic way to strictify homotopy propositions; this operation does not satisfy any definitional laws beyond what is implied by definition. As a result, it is not the case that the round-trip $P\to [P] \to P$ is definitionally equal to the identity function; in some sense, avoiding this definitional equality is precisely the thing that gets us out of the kind of trouble faced by Lean. This is the trade-off: sufficient expressivity demands a map $[P]\to P$ , but this map cannot satisfy any interesting definitional equalities under pain of destroying the reliability of all other definitional properties of the language.

The second proposal is attractive to me because I can interpret it today in any Grothendieck $\infty$ -topos model of HoTT, but I do not know how to interpret it in non-Grothendieck models (which are only just emerging now). On the other hand, the first proposal is far stronger but there is a pretty good chance that it will be shown to be conservative. That would certainly satisfy my design constraints.

What would we do with it? I think it would be good to explore a new variation on abstraction boundaries in proof assistants. In traditional systems, you can make a definition abstract, which means that it has no identity other than its name. We often do this when we have a complicated proof that we will never want to look at again, and when we know that if we ever need to identify it with some other proof of the same type, it will be better to deduce that from its type than from the specifics of the proof. It is possible in cases like this that we might prefer to use strictification as a kind of proof-irrelevant sealing, in which we not only ensure that we never can look at the proof again, but we also ensure that it will be definitionally equal to any other sealed proof.

Such a facility must be used with care. There is, however, an interesting opportunity here for improving the usability of homotopy type theory and univalent foundations without trading away literally every other advantage in return.

Acknowledgements

October 7, 2025
Jon Sterling

My sincere thanks to Carlo Angiuli, Rafaël Bocquet, Daniel Gratzer, and Cameron Zwarich for helpful conversations in the past few weeks on these topics.

Proposal. Shall we strictify some homotopy propositions? › Two proposals for well-adapted proof-irrelevance in UF › An equivalence between `sProp` and `hProp` [01IA]

October 7, 2025
Jon Sterling

This one was suggested to me half a decade ago by Ulrik Buchholtz. The idea is to freely extend homotopy type theory with an abstract universe sProp together with an equivalence from sProp to hProp, such that every P: sProp is definitionally proof irrelevant.

(This system is distinct from the one that simply asserts that every P: hProp is definitionally proof-irrelevant. This latter theory is far stronger and actually derives UIP (and in some formulations, equality reflection!), and is therefore inconsistent with univalence.)

The status of the proposed theory is that it is very likely conservative over Homotopy Type Theory. Rafaël Bocquet has conjectured as much, and has spent several years developing the semantic machinery that would make it possible to prove this result. But today it remains a conjecture.