Shall we strictify some homotopy propositions? [01I6]

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.

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

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.

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

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).

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

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 3.1. An equivalence between sProp and hProp [01IA]

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 3.2. An operation to strictify any given homotopy proposition [01IB]

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. 

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}\).

4. Implications for Project Pterodactyl [01IC]

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.

5. Acknowledgements

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.

References

    Reference. All (∞,1)-toposes have strict univalent universes [shulman-2019]

    We prove the conjecture that any Grothendieck (\(\infty \),1)-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to (\(\infty \),1)-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.

    Reference. Univalence for Inverse EI Diagrams [shulman-2017]

    Context

      Jon’s Pterodactyl Worklog [01HC]

      This is a blog in which I will post regularly about my ongoing work to build Project Pterodactyl; I am working in public, but not all of this will make sense to the public. I am thinking about blogging as a decentralised medium of collaboration and communication among contributors. Other contributors to Pterodactyl should start their own worklogs and we can all subscribe to each other’s Atom/RSS feeds. Subscribe to the atom feed for this page.

      Primitive identity types and proof-relevant unification [01LB]

      I’ve been thinking about the Elimination with a Motive transformation as modernised in terms of type theoretic equivalences. One thing that is striking me right away is that this is going to lead to a pretty scary code blow-up. For instance, if we only consider the basic analysis and the solution rule, a simple construction like the pasting of identifications is going to result in a really large term involving four calls to based path induction, each themselves with increasingly complicated motives. Doing this systematically in the form of unifiers-as-equivalences would result in some even more complicated terms.

      Agda gets around this by not actually constructing the equivalences; Cubical Agda and Mikan, however, need the left-inverse part of the equivalence, and even this quickly blows up when types have more than a couple indices, as the Mikan team have recently noted. Project Pterodactyl would likewise need the left-inverse part as well.

      I was thinking that perhaps one way to deal with this problem would be to use a bit of a hybrid approach. The extreme position is to elaborate everything in sight to eliminators, but a middle ground might be to extend the core language with a schema for the various unification rules and their left inverses with the appropriate computational behaviour. Every time a proof-relevant unification rule used in the elaboration process, a new abstract top-level declaration is inserted that has (by fiat) the correct reduction rules. Because the operator cannot write these terms, we can make them very compact and probably even avoid annotating them with motives.

      Doesn’t this beat the point of eliminating dependent pattern matching? I don’t think so. In Elimination with a Motive, eliminators are playing two distinct roles:

      1. User-land pattern matching and recursion are reduced to core eliminators.
      2. Specialisation of motives against targets is achieved internally using a built-in identity type and its eliminator.

      What I am proposing is that the specialisation step might be achieved using any computationally well-behaved primitives that the built-in identity type comes equipped with. Even if something can be reduced to a very complicated instance of based path induction, we don’t necessarily need to do so. Moreover, doing so may introduce usability problems (where two things that ought not be definitionally equal from the operator’s point of view become equal by coincidence).

      Maybe another way to put it is: it is a coincidence that the user-facing identity type is the same as the identity type used to eliminate dependent pattern matching. If the operator defines their own user-land identity type, then pattern matching definitions defined in terms of it will be reduced to the user-land based path induction principle, but in order to achieve specialisation against the elimination target, the internal identity type (and its rules, whatsoever they are!) will also be used.

      Strengthening by unification [01KT]

      In my last post, I commented that an important component of a reliable implementation of Epigram-style eliminator-refinement is strengthening. The goal of strengthening is to determine whether a term in a given context is equal to a weakened term, coming from a smaller context.

      Can’t we look at free variables? [01KU]

      People who, shall we say, have no idea what they are doing tend to think that strengthening is an easy problem to solve: just calculate the set of free variables! (Go grep your favourite proof assistant’s implementation for free variable checks; I’ll wait.)

      The problem with this approach is that it is not stable under definitional equivalence: in the simplest case, a dependency can be removed by \(\beta \)-reduction. That’s not hard to deal with, of course, but there are still \(\eta \)-laws to contend with. You might think that you could contend with the latter by filtering the set of free variables to remove those that are definitional singletons (like the Unit type, or powers thereof). That will also not work, because you need to consider the way the variable is used: for example, x : Unit * Nat is not irrelevant, but it is used irrelevantly in x.pi1.

      In the end, if you insist on computing free variable sets for whatever misguided or confused reason, the only non-broken way to do so is to compute it only on the \(\beta \)-short \(\eta \)-long normal form. But we all know that nobody is doing this…

      Maybe we already solved this problem… [01KV]

      I think there may be a simpler way to deal with strengthening that takes advantage of all the hard work I put into implementing higher-order nested pattern unification in Project Pterodactyl. Suppose we have a term in context x : A, y : B |- t : T and we want to see if this term can be strengthened into the context x:A. Of course, for this to make any sense, we need to see if the type T can be strengthened away from y : B.

      To that end, create a global metavariable ?S : (x : A) -> Type. Now attempt to unify ?S x == T in the current context. If there is a solution, then that solution is the strengthening of T away from y. Once we have done this, we may then create a global metavariable ?s : (x : A) -> ?S x and unify ?s x == t. (Of course, if the first unification resulted in any postponements, we must block or insert a coercion.)

      Because higher-order nested pattern unification natively respects \(\eta \)-equivalence and definitional singletons, it seems to me that it is the ideal solution to the strengthening problem.

      Warming up on eliminator refinement [01KS]

      Now that higher-order goal matching is in reasonably good shape, it is possible for me to begin considering the implementation of Epigram-style eliminator refinement. The goal would to be able to write code like this:

      paste (A : Type) (u v w : A) (p : u = v) (q : v = w) : u = w where
  paste A u v w p q <= elim p
  paste A u u w refl q => q

      This would elaborate to something very complicated involving a severely generalised induction motive, cut down to size in the methods by several uses of based path induction. For the first version, I do not plan to support the full elimination of dependent pattern matching, and I will be focusing only the solution rule. To undersatnd what this rule does, let us walk through how paste should be elaborated to an instance of the J eliminator. Conor Mc Bride’s “basic analysis” of elim p in this scenario leads to the following identification induction motive:

      x0 : A, x1 : A, x01 : x0 = x1 |-
  (u v w : A) (p : u = v) (q : v = w)
  -> (x0, x1, x01) =* (u, v, p)
  -> <paste A u v w p q : u = w>

      In the above, =* is short for telescopic identity, which unravels to something very complicated involving a lot of transports. If we apply the J eliminator targeting (u,v,w) with such a generalised motive, we can further instantiate the result by A, u, v, w, p, q, (refl, refl, refl).

      In the base case for this induction, we must solve the following goal:

      x : A |-
  (u v w : A) (p : u = v) (q : v = w)
  -> (x, x, refl) = (u, v, p)
  -> <paste A u v w p q : u = w>

      It is at this point that McBride’s rules simplification rules come into play (or, to be precise, the proof-relevant ones described by Jesper Cockx). In the above, the variables A,u,v,w,p,q are considered “flexible” and we want to successively apply elimination rules to the components of the telescopic identification (x, x, refl) = (u, v, p). Although it is not easy to write out the full expansion of this telescopic identification, we know that its first component is an identification hu : x = u. If we proceed by identification induction on hu, then the telescopic identification that remains is (hv : x = v) (hp : transport (x =_) hv refl = p). If we do identification induction on hv, then what remains is (hp : refl = p), which we may dispatch finally using identification induction. All that remains of the goal is the following, which the user-written match clause explains how to solve: 

      x : A |- (w : A) (q : x = w) -> <paste A x x w refl q : x = w>

      Of course, the explanation above in some sense misses the hard part: identification induction can only really reduce the telescope when we have a segment like (u : A) (p : t = u), where the flexible variable is directly adjacent to its defining path. This means we must somehow re-order the telescope, but that requires strengthening, which is notoriously difficult to handle in a way that respects definitional equality (if you see a call to freeVars, they blew it!). I can’t say for sure, but I do see that Agda’s implementation is looking at the free variables set, and this must account for at least some user-facing unreliability or instability.

      In a subsequent post, I will suggest what I think is a reasonable way to handle strengthening in a semantic way, taking advantage of other infrastructure I have built.

      Higher-order goal matching is working [01KR]

      Last week, I blogged about my ongoing struggles with the design of Project Pterodactyl definitional mechanism. Since then, I have managed to get things to a reasonable point, where a user may write code like the following:

      nonChoice
  (I : Type) (A : I -> Type) (B : (i : _) -> A i -> Type)
  (f : (i : _) -> record {pi1 : A i; pi2 : B _ pi1})
  : record {pi1 : (i : _) -> A i; pi2 : (i : I) -> B _ (pi1 i)}
  where
    nonChoice I A B (\i => {f;g}) => {_; g}


nonChoiceInverse
  (I : Type) (A : I -> Type) (B : (i : I) -> A i -> Type)
  (u : record {pi1 : (i : _) -> A i; pi2 : (i : I) -> B _ (pi1 i)})
  : (i : _) -> record {pi1 : A i; pi2 : B _ pi1}
  where
    nonChoiceInverse I A B _ <= intro
    nonChoiceInverse J A B {f;g} i => {_; g _}

      In each clause, the goal is unified via higher-order dynamic nested pattern unification with the user-written left-hand-side. The goal is then adjusted as follows depending on the results of the unification:

      1. When a variable has been simply renamed (as I is renamed to J in the final clause above), this renaming is applied directly in the goal. To reliably detect opportunities for direct renamings, we must use a safe version of \(\eta \)-contraction.
      2. In other cases, such as the binding {f,g}, the context is extended with new definitional bindings f := u .pi1 and h := g .pi2.

      This was a pretty painful trek, mostly due to various wrong turns, but now I am reasonably satisfied with how it works. There of course no doubt remain bugs that I have not yet exorcised. With this in hand, I think it is now possible to begin to proceed to the simplest-possible version of eliminator refinement in the style of Epigram; as I will outline in a future post, this is considerably more difficult than expected in an environment where stability under definitional equality is a requirement.

      There are still some open questions about the design. Right now, when a pattern metavariable is bound underneath a binder on the left-hand side, as in the definition of nonChoice, it is automatically abstracted before being bound on the right-hand side. Another design would require the pattern variables to be explicitly applied to whatever they are going to be abstracted under, so that a pattern like \i => {f;g} would actually only match against constant f,g. I am currently not decided on this point, but I may revisit it later. What I’ve done currently is the simplest thing that can possibly work but I acknowledge that it may be useful to provide more fine-grained control of depenency later on.

      Churning in Pterodactyl’s definitional mechanism [01KN]

      For the past month, I have been working on Pterodactyl’s definitional mechanism, by which I mean that way that you make top-level definitions in the system. As I said from the start, I want to support Epigram-style definitions with pattern-matched left-hand-sides. I made several false starts and I finally arrived at something that works, but this too is not quite what I will need.

      What I currently have is the ability to write definitions like the following example of the “type theoretic principle of non-choice”, i.e. the distributivity of products over sums:

      nonChoice
  (I : Type) (A : I -> Type) (B : (i : _) -> A i -> Type) 
  (h : (i : _) -> record {pi1 : A i; pi2 : B _ pi1})
  : record {pi1 : (i : _) -> A i; pi2 : (i : I) -> B _ (pi1 i)}
  where 
    nonChoice I A B (\_ => {f; g}) => {_; g}

      The above illustrates how the pattern variables in left-hand side of the clause above are resolved using higher-order dynamic nested pattern unification. It took an immense amount of work to get this set up, because the unification algorithm is brand new (due to András Kovács) and very intricate. The example above exercises the machinery quite a lot: in addition to supporting a deep match underneath a binder on the left (this is the nested part of nested pattern unification), the underscores in non-pattern positions are placeholder that are filled in by the unifier as well.

      All that is very good and exciting. Where I have gone wrong is in how I create the environment against which the right-hand side is elaborate. My thinking was that I would want a “clean” environment in the pattern metas on the left become the local variables on the right; this is what I, at long last, have managed to implement. Unfortunately, that is not adequate for what will come next (the introduction of Epigram-style eliminator refinement). For that, it will be important to not wholesale replace the ambient environment, but rather to simply rename and possibly extend it.

      There is a trade-off: when we do nested patterns on the left, we may bind pattern metavariables in such a way that the resulting names do not lead (even up to \(\beta {}/\eta \)-equivalence) a complete renaming of the local variables. For example, in the example above, the destination of the ambient variable h is not another variable, but a nested pattern that names two additional variables f,g which are solved as f := \i => h i .pi1 and g := \i => h i .pi2.

      The “benefit” of my existing approach is that I get a totally clean new local context that doesn’t mention h at all and simply takes f,g as the primitive local variables. Unfortunately, I believe I will have to go for a middle ground where I instead keep the local context, rename whatever can be renamed directly, and then add new local definitional bindings for things like f,g. This means that the goal may still mention old ambient local variables (which will now be in scope). In return for this, I will be able to deal with the hidden hypotheses that are not mentioned in the program/goal label (lhs), including things like induction hypotheses.

      Anyway, this past few weeks has been an example of stepping on the diagonal: we are making forward progress, but somewhat slewed.

      Higher-order pattern unification and…patterns [01KL]

      In the implementation of dependently typed proof assistants and programming languages, “pattern unification” can mean two different things.

      1. Higher-order pattern unification is used to resolve implicit parameters, etc. This kind of pattern unification is always up to judgemental equality.
      2. A version of first-order unification is used to refine the motives of elimination problems. This kind of unification is (at times) involving constraints up to propositional equality.

      Although the two notions of unification are almost entirely different, in an Epigram-like system they may be related to each other. In Epigram, the left-hand side of a definition is actually a core language term that serves as the index to a phantom type. Definitions actually proceed by matching a user-written left-hand-side against the actual core-language left-hand side, whose variables are (naturally) already bound. It seems particularly a nice idea to do this matching using full higher-order pattern unification, because we would be able to write programs like the following, as suggested by Conor Mc Bride:

      def uncurry (f : A -> B -> C) : (A*B -> C) where
  uncurry (\x y => h (x, y)) => h

      The thing about this that is actually surprisingly difficult is not really specifically the pattern unification itself, but the interpretation and presentation of code with user-chosen names. In the above, it is easy enough for the elaborator to know that h should be read as \u => f u.1 u.2 where f is the internal name for the argument to uncurry, but it is much more difficult for the elaborator to know that it should print f in any diagnostics as \u => h (u.1, u.2). Prior to going off on my pattern unification tangent this week, I had written about some preliminary ideas for dealing with this last week.

      I now want to think about how we might combine the two ideas to make this work properly. Maybe the user-written left-hand-side should be elaborated so that every unbound variable it mentions is emitted as a metavariable which is then solved by unification. When the metavariable ?0 is emitted corresponding to the user-pattern-variable h, we should record in the elaboration environment’s “dub table” that the term resulting from applying this meta to all local variables should be dubbed h.

      Now, there is a real subtlety here. Consider the following example:

      def swap (u : A*B) : B*A where
  swap (x,y) => (y,x)

      In this case, we would have dubbed the core term u.1 as x and u.2 as y. Therefore, if the distiller/printer encounters u.1 it will print x, but unfortunately if it encounters just u it will not know what to print!

      I am not sure how to deal with this problem. Some ideas involving \(\eta \)-laws present themselves, but I don’t see how to do this efficiently. I increasingly feel that I have taken a wrong turn… But it does occur to me that similar ideas to those of Nested Pattern Unification might also be used to boil down the dubbings to something useful.

      Patterns and dubbing [01KK]

      As I mentioned in my previous post (Reworking Pterodactyl’s program elaboration), I wish to handle the elaboration of program trees in Project Pterodactyl very similarly to how it is done in Figure 6 of the paper Elaborating Inductive Definitions. In this paper, the elaboration is described in a precise but informal fashion that is abstracted away from the difference between “internal” names and user-provided names. A lower-level specification of the elaboration must carefully distinguish these things.

      This is actually non-trivial in the case of elaborating the left-hand sides to Epigram-style programs. In the versions of Epigram that I actually have the source code to, this was handled by first abstracting all the variables of the expected lhs (using internal names) and then walking through the user's provided pattern to accumulate a relabelling, and then unbinding all local variables and rebinding them with the new names. This is very complicated and error-prone, and probably did not respect \(\eta \)-equality of core terms…

      One suggestion of Conor Mc Bride (which appears not to have been implemented in the version of Epigram I have) is to keep track of user-chosen names and their mapping to core terms. These associations are referred to dubbings. This is more ambitious than simply keeping track of the names assigned to each variable in the context, because in principle you can map a name to a complex term. This is actually important because the core programming label may include an argument in \(\eta \)-expanded form, which we should not be able to syntactically distinguish from a variable!

      This is enough for mapping user-written syntax into the core language, but it poses some difficulties for going the other direction—which is needed for the display of goals, error messages, etc. In the vast majority of cases, the mapping will indeed relate names to actual variables, and here it is easy; but when you end up mapping a name to a complex term like \(\texttt {a} \mapsto \lambda x.\alpha (x)\), it is not easy to determine how to print the core name \(\alpha \) for the user, even though we know it ought to be printed as \(\texttt {a}\). My quick-and-dirty solution for these edge cases is actually to walk through the naming context and check definitional equality until we find the appropriate name. This seems crazy, but it might not be too bad if we memoise it (keeping in mind that it is rare for a user to have more than 10-15 names in scope anyway).

      This solves one part of the problem, but I’m still hoping we can find a better solution that feels less like “putting toothpaste back into the tube”. The other part of the problem is the actual elaboration of patterns, and what this means judgementally. I believe that the following scheme will work: pattern-forms correspond to either canonical, definitionally injective term constructors, or they are dot-patterns (literal terms that bind no pattern variables). The judgemental structure of constructing pattern-forms is kind of interesting: I think that it is a form of judgement like \[ \Gamma \vdash M : A \lhd \mathtt {p} \leadsto \mathcal {D} \] in which \(M:A\) are core-language inputs, \(\mathtt {p}\) is a surface-language pattern subject, and \(\mathcal {D}\) is a sequence of induced dubbings. The rules for elaborating patterns then amount to deconstructing \(M\) in lockstep with \(\mathtt {p}\) whilst respecting the judgemental equality of \(M\), until you reach one of the following base cases:

      1. In the case of a dot-pattern \(.(\mathtt {e})\), we elaborate \(\mathtt {e}\) with type \(A\) and check that it is judgementally equal to \(M\).
      2. In the case of an identifier \(\mathtt {a}\) that is not yet the subject of a dubbing, we emit a new dubbing \(\mathtt {a} \mapsto M\).
      3. In the case of a wildcard pattern \(\mathtt {\_}\), we simply stop.

      It is a little bit annoying to have to implement this structure for all injective constructors in the language, when the structure is going to really be mirroring the existing rules for forming terms. There may be a way to consolidate this, but I am currently thinking that it may not be a good idea to do so. This is worth revisiting in the future.

      By the way, this machinery will make it really easy to implement a match goal with ... tactic.

      Reworking Pterodactyl’s program elaboration [01KJ]

      I thought I was being clever with my approach to elaborating Epigram-style program trees, but I am seeing that I really should have hewed more closely to the presentation of Elaborating Inductive Definitions. The “clever” thing I did was have the elaborator environment keep track of what amounts to a program label in the sense of Epigram, and append stack frames to it when entering the subgoals of negative introduction rules. This is a bit brittle, because it forces a coupling between the use of introduction rules and the shape of user-defined programming problems that is unlikely to hold true in the future. In particular, I think this approach will break down very quickly when I begin allowing things like goal generalisation, etc.

      I tentatively think that the elaborator should not keep track of the programming label as part of its local state, and the interaction with programming labels should be restricted to the specific refinement rules for program trees, just as in Figure 6 of Elaborating Inductive Definitions.

      Another place where I have probably erred is in treating each clause of a program tree as a separate declaration (a unit of incrementality). I think that instead these should be treated as a single hierarchical declaration. In the future it could be a good idea to incrementalise this, and I think it can be done on top of a simpler hierarchical declaration. Trying to do all this at once is flying too close to the sun.

      In short, I believe I should retreat a bit and implement almost exactly what is written in Elaborating Inductive Definitions.

      Project Pterodactyl’s layered architecture [01KF]

      I have made a great deal of progress with Pterodactyl in the past week. One thing I have been working on is modularising the system, which I resisted doing for a while because it was unclear which parts needed to depend on which. But now a reasonable architecture is emerging. Pterodactyl is split into several Swift libraries:

      1. PterodactylCore contains the core syntax, semantic domain, evaluator, and conversion checker. This library is completely indepenent from the rest of the system.
      2. PterodactylKernel contains the rules of Martin-Löf type theory, implemented as closure conditions on functions that produce core terms from an environment and a goal. I will discuss this more below. This depends only on PterodactylCore and is completely independent of concrete syntax. The kernel is trusted, and its outputs are (in LCF style) unforgeable.
      3. PterodactylSyntax contains the concrete syntax of the Pterodactyl, implemented with Roslyn-style homogeneous “green trees”. This library includes the layout lexer and the parser. This library is independent of the other parts of the system.
      4. PterodactylElaborator glues the kernel to the concrete syntax by means of a function inductively converting concrete syntax to calls to the kernel.
      5. PterodactylBuild contains what is usually called the “driver” of a proof assistant: the routine that processes entire modules and workspaces. Our driver is incrementalised at file-prefix granularity, using the swift-llbuild2 infrastructure. See also The CAS model of incremental build systems for previous discussion of this.
      6. PterodactylLanguageServer is the only executable at the moment, and it depends on all of the above—mainly via PterodactylBuild. The language server keeps track of the communication with the language client via RPC, keeping track of buffer state, calling the build system at appropriate times, and sending both diagnostics and subgoal displays to the language client.

      Kernel vs. Elaborator

      My separation of the kernel from the elaborator is unconventional for dependently typed systems: usually an elaborator a bit nest of mutually recursive functions that are trusted to produce valid core language terms. This coupling of surface syntax to the rules of the core type theory is totally unnecessary, as any inductive definition can obviously be translated into a collection of closure conditions. This makes the kernel testable independently of the concrete syntax, and (indeed) it can be run with many different concrete syntaxes if desired.

      The basic forms of judgement of (Pterodactyl’s version of) Martin-Löf type theory are represented in Swift as protocols with methods valued in an abstract type Trust<V>.

      public protocol ElabType {
  func elabType(
    _ env: Environment,
    size: Size<Value>?
  ) async throws(ElabError)
  -> Trust<Term.Type_>
}

// Checking mode
public protocol ElabTerm {
  func elabTerm(
    _ env: Environment,
    type: Value.Type_
  ) async throws(ElabError)
  -> Trust<Term>
}

// Synthesis mode
public protocol ElabTypedTerm {
  func elabTypedTerm(
    _ env: Environment
  ) async throws(ElabError)
  -> Trust<(Value.Type_, Term)>
}

      An example piece of trusted kernel code is the formation rule of dependent function types, as quoted below:

      public struct FunctionFormation: ElabType {
  let binder: TypedBinder
  let fam: ElabType

  public init(binder: TypedBinder, fam: ElabType) {
    self.binder = binder
    self.fam = fam
  }

  public init(dom: ElabType, cod: ElabType) {
    self.init(binder: TypedBinder(name: nil, type: dom), fam: cod)  // consider adding explicit weakening rule to use in 'fam' here
  }

  public func elabType(_ env: Environment, size: Size<Value>?) async throws(ElabError) -> Trust<Term.Type_> {
    let env_dom = env.extendingNamespace(.machine("dom"))
    let idom = try await binder.type.elabType(env_dom, size: size).value

    var env_fam = env
    env_fam.extendNamespace(.machine("fam"))
    let boundName = binder.name.map(Name.user(_:))
    await env_fam.bind(name: boundName, type: idom)
    let ifam = try await fam.elabType(env_fam, size: size).value
    return Trust(.funType(dom: idom, boundName: boundName, fam: ifam))
  }
}

      Finally, the elaborator converts concrete syntax into calls to the above. In the concrete syntax a dependent function type can appear in iterated form, so this must be folded up into multiple applications of the formation rule as below:

      extension SyntaxTreeCursor {
  var depFunTypes: ElabType? {
    guard case .depFunType = kind else { return nil }
    var binders: ArraySlice<TypedBinder> = []
    for (ix, subtree) in subtrees.enumerated() {
      if let binder = subtree.typedBinder {
        binders.append(binder)
      } else {
        guard ix == binders.endIndex else { return nil }
        binders.reversed().reduce(subtree) { partialResult, binder in
          FunctionFormation(binder: binder, fam: partialResult)
        }
      }
    }

    return nil
  }
}

      The query-based build system

      Our build system is query-based and, as I mentioned, incrementalised. Here is an example of a query that computes the top-level environment that results from elaborating a given source tree (an abstraction in CAS of a group of files):

      struct ToplevelEnvOfSourceTree: AsyncFXKey {
  enum ValueType: Codable, FXValue {
    case success(ToplevelEnv)
    case circularImport
  }

  let sourceTreeId: LLBDataID

  public static let versionDependencies: [any FXVersioning.Type] = [Keys.SourceTree.GetDependencyGraph.self, ElaborateUnit.self]

  func computeValue(_ fi: llbuild2fx.FXFunctionInterface<Self>, _ ctx: TSCUtility.Context) async throws -> ValueType {
    let graph = try await fi.request(Keys.SourceTree.GetDependencyGraph(sourceTreeId: sourceTreeId), ctx)
    guard let vertices: [UnitName] = graph.topologicalSort else { return .circularImport }

    var env = ToplevelEnv(decls: [:])
    for unit in vertices {
      let unitResult = try await fi.request(ElaborateUnit(sourceTreeId: sourceTreeId, unitName: unit), ctx)
      env.decls.merge(unitResult.newDecls) { _, new in new }
    }

    return .success(env)
  }
}

      When elaborating an actual source unit, we use the dependency graph to narrow the global source tree to just the parts that the unit is allowed to depend upon. Then we get compute the top-level environment for the narrowed source tree using the above, and proceed with elaboration. Here's a prefix of the unit elaboration query:

      public struct ElaborateUnit: AsyncFXKey {
  public struct ValueType: Codable, FXValue {
    public var newDecls: OrderedDictionary<QName, TypedDataID<GlobalDef>>
    public var feedbacks: [Feedback]
  }

  /// The global source tree
  public let sourceTreeId: LLBDataID
  public let unitName: UnitName

  public init(sourceTreeId: LLBDataID, unitName: UnitName) {
    self.sourceTreeId = sourceTreeId
    self.unitName = unitName
  }

  public static let versionDependencies: [any FXVersioning.Type] = [
    Keys.SourceTree.NarrowToUnit.self, ToplevelEnvOfSourceTree.self, Keys.SourceTree.GetUnitBlobId.self, Keys.Blob.ParseDocument.self, ElaborateDecl.self
  ]

  public func computeValue(_ fi: llbuild2fx.FXFunctionInterface<Self>, _ ctx: TSCUtility.Context) async throws -> ValueType {
    let narrowedSourceTreeId = try await fi.request(Keys.SourceTree.NarrowToUnit(sourceTreeId: sourceTreeId, unitName: unitName), ctx)
    let blobId = try await fi.request(Keys.SourceTree.GetUnitBlobId(sourceTreeId: sourceTreeId, unitName: unitName), ctx).blobId
    let tree = try await fi.request(Keys.Blob.ParseDocument(blobId: blobId), ctx).tree
    let cursor = SyntaxTreeCursor(tree: tree, utf16Offset: 0)

    switch try await fi.request(ToplevelEnvOfSourceTree(sourceTreeId: narrowedSourceTreeId), ctx) {
      // ...

      As you can see, queries are versioned. This is important because the function cache may be stored on disk! Versioning allows these caches to be invalidated when an incompatible version of Pterodactyl is being run.

      All the subrequests are, naturally, cached in the database which allows top-level environments to be rapidly reconstructed as-needed without re-elaborating anything. As I mentioned before, the granularity of incrementalisation is file prefixes: it might be nice to have declaration-level granularity, but I think that is not possible in any system with type classes, an implicit coercion graph, or any other feature that introduces implicit dependencies. Our incrementalisation is, however, insensitive to changes in position that do not lead to semantic differences.

      It remains to be seen if the build system will be performant: llbuild2 has never been used in this way, and there may be bottlenecks that we need to resolve, or mistaken aspects of the design that we must revisit. It will be difficult to tell until we can run Pterodactyl on a codebase of reasonable size, which is not currently possible because so little of the language is in place.

      Disentangling unification and implicit coercion [01JQ]

      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?

      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:

      1. Rocq’s coercion mechanism is very predictable but its unification is not.
      2. 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?

      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

      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:

      1. 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.
      2. 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!

      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?

      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.

      The CAS model of incremental build systems [01IP]

      I have continued on my quest to understand and compare different architectures for demand-based/query-based compilation and elaboration. This week I have been exploring the llbuild2fx library from Apple, which its authors describe as a fresh take on low-level build system API. I’m incredibly grateful to Nima Johari for taking the time to answer my many questions about it, and to Cameron Zwarich for some very useful discussions about the incrementalisation of elaboration.

      It seems that there are two major approaches to demand-based build systems. The first, which is better known, is incremental computation based on dirtying of inputs which ripple outward in the form of cache invalidations. To my knowledge, this style is represented in Adapton, Shake, Rock, Incremental, and Salsa. Incremental computation in this sense is built up from a network of pure functions operating on stateful inputs at the edges.

      A second approach, which is being explored by Apple’s build team, is completely stateless; rather than input nodes being subject to update and inducing cache invalidation, inputs are instead ingested into content-addressed storage (CAS). The entire input to a build process (the source tree and the configuration) is then referred to (via a content-address) in the query nodes. The CAS-based approach, therefore, is not really involving cache invalidation: instead the data of a query contains a stable reference to CAS that can be narrowed to smaller fragments of the CAS in subsequent queries. When input state changes, it is ingested into the CAS and new queries are made that refer to the new data; naturally, child queries will narrow their reference to CAS and this will result in cache hits when the scope has narrowed to something that has already been computed.

      There are trade-offs between the two approaches. The first (which I will call stateful incremental computation) is easier to use, because dependency on stateful edge nodes is dynamic and determined in the process of query evaluation automatically. In contrast, the stateless CAS approach requires you to think very carefully about how to narrow the CAS keys referenced in queries. On the other hand, the stateless approach is more flexible in terms of the execution models it supports, which includes distributed builds. (I have a feeling distributed builds are going to be very important for large mathematical libraries in the future, or maybe even in the present if you look at the resources needed to build Mathlib.)

      Apple uses (or aims to use) llbuild2fx to coordinate internal builds of their software and its complex dependencies, and I believe they also plan for this (or something like it) to eventually be used in Xcode and the Swift compiler. I am, however, apparently the first person to be attempting to use llbuild2fx on the interior of a compiler, which is of course a potential risk. But a fun risk that I expect to learn a lot from either way.

      Sending strict propositions to the Ripley cupboard [01IK]

      Please note: I am no longer confident in the conclusions of this post, and I believe that I have made some mistakes. When I have ironed out what is true and what is not true, I will write a follow-up and link to it from here.

      Conor Mc Bride likes to send hopeless ideas and design mistakes to their Ripley Cupboard, a reference to a scene in the highly underrated film Alien: Resurrection in which all the hopeless attempts to reconstruct Ellen Ripley from DNA are stored in a gruesome menagerie. I am afraid that in spite of their successful semantic rehabilitation, strict / definitionally proof-irrelevant propositions must nonetheless find their permanent residence in my own Ripley cupboard for syntactical reasons.

      One thing that I had noticed a couple nights ago was that there might be a problem finding a suitable generalisation of Miller’s pattern fragment for dependent type theory with strict propositions. I was not really precise about what my concern was, but thankfully Matthieu Sozeau managed to pin it down.

      In essence, the problem has to do with what syntacticians call “strengthening”. The thing that makes higher-order pattern unification work well is the ability to tell whether or not some term actually depends on a given variable up to definitional equality; this is important because if you can eliminate a syntactic dependency, two things might happen that could allow the unification process to proceed further (1) a blocked unification problem may suddenly fall into the pattern fragment, and (2) a failing “occurs check” may start to succeed.

      With definitional singleton types, this is all fine: we can reliably eliminate dependency on singletons in a number of different ways, but these ways all rely on the fact that singleton types are inhabited. For definitional subsingletons, i.e. strict propositions, it is another story. Imagine that you have a strict proposition \(P\) and a subterm \(M(x,y,z):P\) of a larger proof-relevant unification problem; in order to find out whether or not the whole problem depends on \(x,y,z\) you need to know whether or not a “shorter” proof of \(P\) is derivable, which is obviously an undecidable problem.

      The upshot is, as Matthieu put it, we are not going to be able to find most general unifiers in any fragment of the language that involves strict propositions. Completeness of unification within a well-defined fragment is, in my opinion, the mathematical shadow of a more important but intangible property of unification being reliable and predictable. Therefore, I think that this observation may imply that reliable and predictable unification is not compatible with having strict propositions in any form.

      The implication for Project Pterodactyl is that we will not be pursuing strict propositions in any form, including my recent proposal.

      (It would be very welcome if someone noticed a way to get around this apparent obstruction, but I am not optimistic. It seems pretty airtight to me at the moment.)

      Shall we strictify some homotopy propositions? [01I6]

      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]

      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]

      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]

      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]

      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]

      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. 

      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]

      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

      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.

      Fuss-free universe hierarchies [01HX]

      The thing about universe hierarchies is that they are both painful to implement properly, and punting on them leads to even more pain later on because introducing a hierarchy is an extremely disruptive change for both the system and its libraries. After going through this treadmill a few times, I’ve learned my lesson: universes are something we need to get right from day one. Let me clarify that it is a non-goal to have inferred universe levels; I instead want to make working with universe levels as simple as possible, and to minimise the number of places where they need to appear.

      The first thing people ask is whether we will use universes “à la Russell” or “à la Tarski”. This is a question laden with false ideology, because the only kind of universes that exist in an objective (i.e. generalised algebraic) sense are the latter. But there is a valid question lying under the surface, which is whether or not users will be expected to explicitly write the decodings and universe level coercions. To that, I answer that we have the elaboration technology today to reliably avoid these bureaucratic details cluttering the source language.

      So you want a coherent universe hierarchy… [01HY]

      Someone who wishes to deploy modern elaboration technology to achieve an implicit source language, however, must think very carefully about the algebraic formulation of the core language to ensure that it has enough equations to maintain predictable behaviour under the implicit Russell-style notation. For example, if the level coercions are not coherent enough, it is easy to create unacceptable error messages that appear to the user like “Could not unify A -> B with A -> B.” Unfortunately, strong enough core languages are very laborious to specify and implement; for example, you will need the following (or some variation):

      1. You need top-level type constructors for all type theoretic connectives.
      2. For each universe level i, a type U[i] : Type and a dependent type el[i] : U[i] -> Type and codes closing U[i] under all type theoretic connectives, including codes for U[j] with j<i. The el[i] operation needs to commute strictly with the type constructor codes.
      3. For universe levels i <= j, you need a lifting operation lift[i<=j]: U[i] -> U[j] that commutes with all type constructor codes and is, moreover, definitionally functorial in the level preorder.
      4. You need el to commute with lift. (Thanks to Meven Lennon-Bertrand for catching this!)
      5. You need both lift[i<=j] and el[i] to be definitionally injective.

      There could be ways to refactor the above; for example, you could get rid of the top level of types altogether and just have universes. This is sometimes referred to as “universes à la Coquand”. Although admirable for its parsimony, I no longer like this approach because I agree with Per Martin-Löf that types and their elements are different concepts. And, for engineering purposes, although it seems at first easiest to have only universes, I think there are subtle ways in which that choice can make other aspects of the implementation more complicated. I think the importance of a separate top-level notion of type is argued for very well in the recent paper of Bezem, Coquand, Dybjer and Escardó.

      Anyway, this is a lot to implement in the kernel of a proof assistant.

      A new idea: Working your way down from the top [01I0]

      About a year ago, I started to get the inkling of an idea that we should not program with respect to a universe at all if we don’t need it. Instead, we should do large things by default (just like in everyday mathematics) and then when we have a need to talk about small things, we should just specialise them as-needed. For example, let’s consider the generalised algebraic theory of a category as phrased in univalent foundations:

      1. We have a \(1\)-type of objects C.
      2. For every two x,y:C we have a \(0\)-type of arrows C(x,y).
      3. And a bunch of operations and axioms involving the above.

      There is nothing about this definition that requires any particular constraints on the size of C and of C(x,y). In fact, the proper definition would not require that C(x,y) have the same size as C(u,v)! From the point of view of (generalised) algebra, these are just sorts. In fact, you never need to constrain the size of these things until you wish to start talking about things like the (bi)category of categories, etc.

      In contrast, if you require all types mentioned in a theory to have a given size, you immediately create a lot of complexity. First of all, you will be automatically assuming that the category is locally small for some universe—by requiring that C(x,y) be V-small for all x,y; there can be times when this is an unnatural assumption. But maybe the bigger problem is that when you want to start developing the theory of functors and natural transformations and so on, you will end up having at a half-dozen universe levels annotating every definition. Implicit universe polymorphism is not a solution to this problem: implicitly resolving the levels does not remove the complexity, and any experienced mechaniser will know that you inevitably need to debug a universe constraint graph.

      Some dream code [01I1]

      What I would like is the best of both worlds: to be allowed to develop the theory with fully unconstrained sizes, and then specialise the theory to more specific sizes later. Consider the following dream code for the theory of categories:

      theory Category where
  ob: Type
  hom: ob -> ob -> Type
  // operations and axioms...

      There is no implicit polymorphism happening in this definition. It is literally a very large theory of large categories. We can develop the theory of functors and natural transformations at this level too:

      theory Functor where
  C: Category
  D: Category
  ob: C.ob -> D.ob
  hom: (x y: C.ob) -> C.hom x y -> D.hom (ob x) (ob y)
  // axioms...

theory NaturalTransformation where
  C: Category
  D: Category
  F: Functor / {C => C, D => D}
  G: Functor / {C => C, D => D}

  go: (x: C.ob) -> D.hom (F.ob x) (G.ob x)
  // naturality axiom...

      If we want to talk about small or locally small strict categories, this is going to be very easy, and we can reuse everything from the theory of functors and natural transformations by instantiation.

      theory LocallySmallCategory where
  V: Universe
  ob: Type
  hom: ob -> ob -> V

  inherit Category / {ob => ob, hom => hom}

theory SmallCategory where
  U: Universe
  ob: U
  inherit LocallySmallCategory / {V => U, ob => ob}

      The above registers implicit coercions SmallCategory >-> LocallySmallCategory >-> Category. So if we want to talk about functors between X: SmallCategory and Y: LocallySmallCategory, we can do so by specialisation with no fuss:

      Functor / {C => X, D => Y}

      We will also be able to define the large category of small categories, again with no fuss.

      theory SmallStrictCategory where
  inherit SmallCategory

  code: U
  code/is-set: is-set code

  encode: code -> ob
  encode/surjective: is-surjective encode

theory CategoryOfSmallStrictCategories where
  U: Universe

  scat: Category
  scat.ob => SmallStrictCategory / {U => U}
  scat.hom X Y => Functor / {C => X, D => Y}
  // ...

      The theoretical foundation [01I2]

      I am now going to describe a way to set up a coherent universe hierarchy so as to ensure a parsimonious interpretation. I would like to emphasise that the dream code above can be elaborated to a traditional coherent universe hierarchy with enough equations, and that my reformulation here is only aiming to make this easier.

      In essence the main idea is to think about the image of the universe decoding maps el[i]: U[i] -> Type. In the generalised algebraic theory, we have required that these encoding maps be injective; an easily overlooked consequence of the injectivity is that the image of the decoding map is a derivable sort in the generalised/essentially algebraic doctrine.

      From this observation, we might instead consider a reformulation where instead of axiomatising the type codes and decoding maps and lifting coercions at each level and all the equations they must satisfy, we might instead axiomatise the images of the decoding maps in Type. This corresponds syntactically to defining a smallness judgement on types, which has a particularly extrinsic feeling to it. In fact, we would define this judgment using a judgemental partial ordering of universe levels; one example rule is the following:

      \[ \frac {\Gamma \vdash i+1 \leq j}{\Gamma \vdash U_i\ \mathit {small}_{j}} \]

      (The real generalised algebraic theory would have a sort of smallness-proofs, but this sort is axiomatised as a proposition. The fact that coherence/proof-irrelevance is baked into the theory fully justifies a notation in which the proofs are omitted.)

      Now, we recover the codes and the level coercions in one fell swoop by means of the following simple rules:

      \[ \frac { \Gamma \vdash A\ \mathit {small}_i }{ \Gamma \vdash \lceil A\rceil _i : U_i } \quad \frac {\Gamma \vdash A:U_i}{ \Gamma \vdash \lfloor A\rfloor _i\ \mathit {type} } \quad \frac {\Gamma \vdash A:U_i}{\Gamma \vdash \lfloor A \rfloor _i\ \mathit {small}_i} \] \[ \frac { \Gamma \vdash A\ \mathit {type} \quad \Gamma \vdash A\ \mathit {small}_i }{ \Gamma \vdash \big \lfloor \lceil A \rceil _i \big \rfloor _i \equiv A\ \mathit {type} } \quad \frac { \Gamma \vdash \lfloor A\rfloor _i \equiv \lfloor B\rfloor _i\ \mathit {type} }{ \Gamma \vdash A \equiv B : U_i } \]

      Now, supposing that the smallness and level inequality judgements have been filled out sufficiently, we can derive codes for connectives at the lower levels from the corresponding top-level type connectives. For example, consider the dependent function space:

      \[ \frac { \displaystyle \frac { \Gamma \vdash A: U_i }{\Gamma \vdash \lfloor A \rfloor _i\ \mathit {type}} \quad \frac { \Gamma ,x:\lfloor A\rfloor _i \vdash B[x]: U_i }{\Gamma , x: \lfloor A\rfloor _i\vdash \lfloor B[x] \rfloor _i\ \mathit {type}} \quad \frac { (\cdots ) }{ \Gamma \vdash (x:\lfloor A\rfloor _i)\to \lfloor B[x]\rfloor _i \ \mathit {small}_i } }{ \Gamma \vdash \big \lceil (x:\lfloor A\rfloor _i)\to \lfloor B[x]\rfloor _i \big \rceil _i : U_i } \]

      Of course, the notation is a little noisy, but these operations are precisely the sorts of things that are easy for a bidirectional elaborator to insert (and then hide from the user). It works equally well for Agda-style hierarchies with joins:

      \[ \frac { \displaystyle \frac { \Gamma \vdash A: U_i }{\Gamma \vdash \lfloor A \rfloor _i\ \mathit {type}} \quad \frac { \Gamma ,x:\lfloor A\rfloor _i \vdash B[x]: U_j }{\Gamma , x: \lfloor A\rfloor _i\vdash \lfloor B[x] \rfloor _j\ \mathit {type}} \quad \frac { (\cdots ) }{ \Gamma \vdash (x:\lfloor A\rfloor _i)\to \lfloor B[x]\rfloor _j\ \mathit {small}_{i \sqcup j} } }{ \Gamma \vdash \big \lceil (x:\lfloor A\rfloor _i)\to \lfloor B[x]\rfloor _j \big \rceil _{i \sqcup j} : U_{i \sqcup j} } \]

      The beauty of this simple approach is that we cut by two-thirds the number of universe-related operations we must implement in the core language. In that sense, we have an equivalent reformulation of coherent universe hierarchies that is more friendly on the engineering side.

      What about universe polymorphism? [01HZ]

      There are a few directions that one might go for introducing universe polymorphism. I will outline a couple options, both of which can be built on top of the above.

      Explicit polymorphism with a sort or type of levels [01I5]

      In Agda, the levels themselves form a type; this simplifies some things, and makes other things more complicated; on the other hand, Bezem, Coquand, Dybjer, and Escardó have proposed a stratified system in which levels can be abstracted but are not organised into an actual type. The main comment I would like to make here is that the formulation of universe heirarchies that I have described above will work regardless of whether levels form a type. The main syntactical challenge is to implement the smallness and inequality judgements, but is easily done in the style of Allais, McBride, and Boutillier as recently reformulated by Corbyn et al.. Put in terms of the latter, the type of universe levels is the free semilattice with successor on the presheaf of neutral terms of level type; and it is easy to decide equality in free semilattices with successor.

      A semantic challenge for Agda-style levels is that the semilattice laws are very strict, and so an interpretation into a higher-topos model might be a problem; for example, we cannot rely on the natural numbers being strict in every model of HoTT, which means that the semilattice laws might not hold definitionally. But we can stratify things in such a way that the type of levels is not small for any universe; then the universe levels could be interpreted as the “exo-naturals” in the extensional outer-layer of two-level type theory, which is conservative over HoTT.

      McBride’s Crude but Effective Stratification [01I4]

      In 2012, Conor Mc Bride proposed what they called Crude but Effective Stratification. Their idea is to define everything at the lowest possible level where it can live, but then subject the entire type theory to a functoriality in displacement operations, which allows developments to be shunted upward in the hierarchy as-needed. One way to think about the simplest version of Crude but Effective Stratification is that every top-level definition is polymorphic in a secret universe level variable, which can be restricted along edges in the universe level preorder. For more advanced functionality, you instead think of the top-level definitions as being polymorphic in a displacement.

      Conor’s idea is very flexible. As Favonia, Angiuli, and Mullanix pointed out, you could also have a universe hierarchy indexed in integers, and then shunt the developments both upward and downward. This one is justified in syntactical way—a semantic model of the system would not have have negative universe levels, but would instead pass through the observation that a given piece of syntax can only use finitely many universe levels.

      Either way, the benefit of McBride’s universe displacements is that when you have an arrangement of universes that need to be in some linear relationship to each other, you can just pick the tightest possible instantiation (e.g. U, U+, U++), and then later use a displacement to create extra room between the universes.

      Anyway, I think this is a good idea for handling universe polymorphism, but that question is a orthogonal to the design of the hierarchy itself. If we want, we can implement Crude but Effective Stratification on top of our foundation. I don’t plan to do this on day one, because I first want to see what the usability limitations are before introducing general displacements.

      In Project Pterodactyl, I will start with a preference for the explicit polymorphism to keep things simple. I am open to revisiting this in the future. By the way, I have already implemented everything I have described in this post in my secret Pterodactyl kernel (minus the elaboration itself).

      Towards a specification of theory refinements [01HU]

      In my previous post, I discussed how to deal with coercions between refined theories. While trying to come up with sufficiently expressive rules for forming theory refinements, I realised that this can get very complicated if you do not first fix some prudent simplifying principles.

      Shallow refinements might be all you need? [01HV]

      One thing that users might expect to be able to do is form deep refinements like in ML modules, where instead of specialising a field of the top-level structure, you specialise a field of a substructure. For example, suppose we had defined rings in the following way:

      theory Ring where
  car: Set
  additive: AbGroup / {car => car}
  multiplicative: Monoid / {car => car}
  dist/left: // ...
  dist/right: // ...

      Then we might want to consider a ring structure on the integers in which the addition is given by integer addition, which makes us want to be able to write a theory refinement like Ring / {car => Int, additive.join => Int/add} or something. I would like to posit, if I can, that this is unnecessary.

      The issue is that in practice, a composite structure like that of rings ought to be flattened anyway. So we would instead really want something like:

      theory Ring where
  car: Set

  include additive: AbGroup / {car => car} renaming
    unit => zero
    join => add
    
  include multiplicative: Monoid / {car => car}
    join => mul
    unit => one

  // ... dist/left, dist/right

      Above I have introduced a few new construct: theory inclusion (distinct from inheritance) and theory renaming. What this should unravel to is something like the following:

      theory Ring where
  car: Set
  add: car -> car -> car
  zero: car
  // ... add/assoc, add/zero/left, add/zero/right, add/comm
  mul: car -> car -> car
  one: car
  // ... mul/assoc, mul/one/left, mul/one/right,
  // ... dist/left, dist/right
  additive: AbGroup / {join => add, unit => zero, ...}
  multiplicative: Monoid / {join => mul, unit => one, ...}

      Because we have named the substructures, the system would not emit any canonical inheritance coercions from Ring to AbGroup or Monoid, as these would not be coherent anyway. The additive and multiplicative components now serve mere “tokens” by which you can access the additive subgroup or the multiplicative monoid all at once, but these are singletons and therefore would not appear in the construction of a given ring.

      Coming back to our example, we see that we can obtain the theory of ring structures on integer addition by a shallow refinement Ring / {car => Int, add => Int/add}. I believe that by keeping hierarchies flat in the style of Mathematical Components, we will always be able to obtain the needful refinements shallowly.

      Preliminary thoughts on specifying shallow refinements [01HW]

      To a first approximation, a refinement of a theory with telescope \(\Phi \) is given by a prefix \(\Phi \) of \(\Psi \) together with an instantiation of \(\Phi \). This is a good first step, but it does not correctly handle the (very common) case where we wish to refine only certain fields that are not necessarly forming a contiguous prefix. In the simplest example, we might want to speak of pairs whose second component is fixed.

      These cases arise when one field’s type doesn’t depend on all of the prior fields. One approach to dealing with this would be to replace telescopes by directed acyclic graphs in which the edges represent dependency. I think this can be achieved, but I think it might very complicated, keeping in mind that as one field gets refined, the remainder of the DAG would need to reconfigure itself (in other words, substitution can cause dependencies to disappear).

      I have been thinking that a better way to deal with this would be instead to allow a refinement to start in the middle of the telescope, and have it be implicitly abstracted over all the previous fields. Skipping a field just abstracts over that field. Then by construction, the refinement is well-typed but we can still handle the mentioned examples. This is kind of what I did in my Lean prototype of Pterodactyl, but it is difficult to understand my code…

      One subtlety of this approach is to figure out appropriate syntactic conditions for these refinements to always correspond to a display map. The naïve version outlined above would allow a refinement by the diagonal, which is probably not what we want.

      Lifting coercions to theory refinements [01HN]

      Last time, I spoke about plans for handling multiple inheritance and implicit coercions in Pterodactyl’s theory preorder. Today it is time to talk about bundling and refinement, and the rules for constructing and coercing implementations of refined theories.

      Refining bundled theories [01HO]

      When you have a theory, like that of semigroups, you define it in a fully unbiased/bundled way:

      theory Semigroup where
  car: Set
  join: car -> car -> car
  join/assoc: (x y z : car) -> join (join x y) z = join x (join y z)

      Then we might define monoids in terms of semigroups:

      theory Monoid where
  inherit Semigroup

  unit: car
  join/unit/left: (x : car) -> join unit x = x
  join/unit/right: (x : car) -> join x unit = x

      Suppose we want to describe the assumptions to the Eckmann–Hilton argument, where you have a pair of monoids sharing the same carrier set and satisfying a distributive law. For that, we need a way to refine a theory by a partial instantiation of its fields. Here is how it might look:

      theory EckmannHilton where
  X: Set
  M, N: Monoid / {car => X}
  dist: (u v w x: X) -> M.join (N.join u v) (N.join w x) = N.mul (M.mul u w) (M.mul v x)

      Things like this are dealt with in the world of Rocq’s Mathematical Components by using a “mixin” pattern: for every structure you predict in advance what unbundlings you are going to need, and then define a bundled version by taking a sum over these. This works very well, though it is a bit cumbersome and inflexible. I would like to build this feature directly into the language, and do it in such a way that you don’t need to predict unbundlings in advance.

      Introduction rules for refined theories [01HP]

      “Semantically”, a theory expression denotes a telescope in Martin-Löf type theory, and the type corresponding to a given theory expression should be the corresponding dependent record type / \(\Sigma \)-type; a refined theory corresponds to a smaller telescope. But theories are also names onto which various operations can be attached, so we can’t just elaborate them directly to the record type, as we will lose information that we need to keep ahold of.

      My thinking is that any theory expression T should induce a telescope <<T>> that consists of the remaining fields. So Monoid / {car => Nat} would correspond to the following telescope <<Monoid / {car => Nat}>>:

      join: Nat -> Nat -> Nat)
join/assoc: (x y z : Nat) -> join (join x y) z = join x (join y z)
unit: Nat
join/unit/left: (x: Nat) -> join unit x = x
join/unit/right: (x: Nat) -> join x unit = x

      Then every theory expression \(T\) comes equipped with a constructor form 

      make: <<T>> -> T

      which allows the user to fill in whatever residual fields are not refined in \(T\).

      Lifting canonical coercions to theory refinements [01HQ]

      The theory coercion preorder is only tip of the iceberg in terms of how coercions must get dealt with. These coercions need to be extended coherently across the negative fragment of the type theory itself.

      For example, if we have a synthesis form X:Monoid / {car => Nat}, we must be able to elaborate X:Semigroup / {car => Nat} seamlessly. There are a few ways that we might imagine this working. The simplest is to apply the constructor for Semigroup / {car => Nat} and then in each case apply the corresponding destructor of Monoid. I am not in love with this option because it leads very eager \(\eta \)-expansion during coercion, which can cause term size to blow up.

      I think there could be another implementation strategy which is more systematic. Let us consider a refinement scenario where we have refined a theory T by a partial instantiation R.

      Now, suppose we have two refined theories T0/R0 and T1/R1. There are many possible functions T0/R0 -> T1/R1 but I wish to argue that only some of these functions are canonical. In particular, a canonical function T0/R0 -> T1/R1 is one that arises in the following way from a canonical coercion T0 -> T1:

      To make it more intuitive, we can instantiate the scenario above with something concrete:

      (Thanks to Owen Lynch for pointing out some mistakes in the prior version of the diagrams above!)

      The definition of canonical map between refined theories gives, immediately, an algorithm for lifting coercions to refinements. The algorithm involves checking that the squares commutes up to definitional equality. In the implementation, we would not literally define the induced canonical map, but instead we would give it as a syntactic constructor and associate to the correct computation rules. This is transparent from the point of view of the type theory, but it avoids unnecessary \(\eta \)-expansions that would cause term sizes to blow up.

      Lifting canonical coercions to other type constructors [01HR]

      We will lift coercions to \(\Pi / \Sigma \) types in the standard way. What we will not ever try to do is lift coercions through any type constructors that lack \(\eta \)-laws, such as parameterised inductive types. This is not only because handling coercions for parameterised inductive types is syntactically difficult (but see the heroic work of some of my colleagues). Lost in the question of whether we can figure out how to deal with the syntactic difficulties of pushing coercions through positive types is the more troubling question of whether this can be made semantically compatible with the interpretation of inductive types in higher categorical models of type theory, where the “obvious” interpretations of inductive types involve some kind of fibrant replacement.

      Avoiding dependent coercions via “selfification” [01HS]

      Many treatments of coercions do not handle well the problem of when the type of the coercion seems to depend on the value being coerced. Luo and Soloviev attempted to address this problem by introducing a notion of “dependent coercion”; Lean also has a notion of dependent coercion. Luo and Soloviev’s version seems to have some issues, where the most expressive rules that one would want cannot be included without breaking transitivity elimination; Lean’s version explicitly does not support chaining of dependent coercions, and I wonder if this is the reason why.

      I am contending today that many useful cases of dependent coercions don’t actually need to be dependent. My idea is based off an old trick known only to the ML Modules Crew called “selfification”, which my PhD advisor Bob Harper kindly taught me several years ago. The idea of “selfification” is to transform a dependent coercion problem into a non-dependent one.

      Suppose that we have a bidirectional elaborator, and we are now at the mode-shift. We have received some typed term M:T where T is a theory expression and we are trying to check it at type B. Rather than searching for a canonical coercion from T -> B, we instead first construct the maximal refinement “T/M” of T to a definitional singleton type that contains only M; this means refining all the fields of T to project the corresponding ones from \(M\). Then we try to find the canonical coercion from T/M to B.

      (I think we can also generalise the algorithm to work even when the synthesised type is not a theory expression, but I won’t talk about that today. In case I forget, the idea is treat the mode shift as always being between theory types, which can be done by having a built-in theory for typed terms.)

      I want to show an example. Consider the case of trying to define the following dependent function:

      cool (X : Monoid): Semigroup / {car => X.car}
cool X => X

      The idea here is that (1) if X is a monoid, then it’s a semigroup by forgetting the extra stuff; and (2) forgetting this extra stuff leaves the carrier set fixed. Can we justify returning X as above via elaboration?

      Yes. The elaboration state at that point is asking us to convert X : Monoid to Semigroup / {car => X.car}. Obviously we cannot hope to find a coercion Monoid -> Semigroup / {car => X.car}, but what we do instead is attempt to find a coercion from

      Monoid / {car => X.car, join => X.join, unit => X.unit, join/assoc => X.join/assoc, join/unit/left => X.join/unit/left, join/unit/right => X.join/unit/right}

      to Semigroup / {car => X.car}. And that is something we can evidently do, using our notion of canonical coercion between refined theories!

      In summary, we have very strong dependent-type-friendly coercions, without needing the coercions themselves to be dependent functions.

      Labelled preorders and implicit coercions [01HB]

      Project Pterodactyl aims to support coherent algebraic hierarchies with multiple inheritance as well as user-defined edges. As I mentioned in my HoTTEST talk, there are a few points worth mentioning here in regard to the so-called “diamond problem”.

      What is the diamond problem? [01HD]

      The first thing to get out of the way is that the phrase “diamond problem” means different things to different people. There are actually two different diamond problems that arise when building systems that support implicit coercion; these two problems are actually mutually exclusive, in the sense that you can have only one version of the diamond problem at once.

      1. There is the coherence problem, which concerns ensuring that diamonds (and loops) in the coercion graph commute. A system in which all diamonds and loops commute is called coherent. In a coherent system, backtracking is never required and so the resolution of coercions can be extremely efficient. This is the “diamond problem” for Theory B computer scientists.
      2. In an incoherent system, resolution of coercions must traverse all possible paths from the source to the target, and the presence of diamonds and loops in the graph can cause an exponential blowup for the naïve backtracking algorithm. This is the “diamond problem” for Theory A computer scientists.

      Indeed, if your system is coherent then no backtracking is required; but you must find a way to maintain the coherence invariant. On the other hand, if you have an intentionally incoherent system, then you do have to deal with the exponential blowup, but you don’t have to check coherence because you don‘t care about coherence. This is the sense in which the two problems are mutually exclusive.

      Approaches to the diamond problem(s) in existing systems [01HE]

      Here I outline some (but not all) existing approaches to dealing with implicit coercions, multiple inheritance, and the various diamond problems.

      Coherent type classes in Haskell [01HF]

      Haskell employs a syntactic condition to ensure that type classes instances do not overlap, leading to a global coherence property. Practice in the Haskell community has shown that it is possible (but painful) to develop coherent hierarchies. Many advanced libraries will activate a language extension to allow overlapping instances, which renders the hierarchy incoherent.

      Fast but incoherent type classes in Lean [01HG]

      Type class hierarchies arising in mathematics tend to be unavoidably incoherent; therefore, systems like Lean implement a backtracking type class resolver and are therefore confronted with the second diamond problem above. The Lean team have discovered an algorithm that they call Tabled Typeclass Resolution that mitigates the exponential blow-up using ideas from logic programming.

      The state of affairs for Lean is, then, that type class resolution is pretty fast but the actual resolution of coercions is in theory non-deterministic; in reality, it does the same thing every time (so far as I know), but there is no guarantee about which coercions it is choosing.

      Coherent locale hierarchies in Isabelle [01HH]

      Locales provide a coherent way to organise mathematical hierarchies. The problems that lead type class hierarchies to become incoherent do not seem to apply to locale hierarchies, I think, because the resolution of the locale’s operations is name-based rather than component-based. (I am not completely certain that this is the full story, but it seems like it is part of the story.)

      One way to think about locales and the reason they can remain coherent is by analogy with Haskell’s newtype trick, which Haskell programmers use liberally to maintain coherence, but taken to its logical conclusion. Instead of generating a fresh copy of a type in order to indicate its intended role in the type class hierarchy, Isabelle doesn’t hang identity on the type at all and instead just starts with the name that carries intentional force.

      The coherence of the locale hierarchy in Isabelle is checked when activating a locale as a local theory. Here, an algorithm called “roundup” reaches through the entire locale inheritance graph and brings all the needful operations into scope, and if there is a clash (two names pointing to different things), this results in an error. Such a clash always corresponds to a failure of coherence, and conversely, failures of coherence will always lead to such clashes.

      Coherent coercions in Rocq [01HI]

      Rocq has a coercion mechanism, which checks coherence and warns users when they are installing incoherent coercions. Coercions are most used in the world of Mathematical Components in combination with the canonical structures feature, which simulates type-class like features using something like unification hints (to my knowledge).

      The algorithm used in Rocq was created by Kazuhiko Sakaguchi and described in the PhD thesis Refinement and extension of mathematical structures in proof assistants based on dependent type theory. The idea here is to maintain the reflexive-transitive closure (path category) of the coercion graph at all times; when inserting a new coercion, you check a generating class of diamonds for coherence and then add all the induced paths. Coherence then ensures that the path category is a preorder, with a functorial embedding into the syntactic category of the language under consideration.

      Evaluating: Isabelle‘s roundup algorithm vs. Rocq’s coercion graph [01HJ]

      I am ruling out incoherent hierarchies from the outset, because these lead to unpredicatable resolution. The two viable approaches seem therefore to be the one of Isabelle and the one of Rocq; I believe that the latter will work best for our needs, even if our goal is to enable an Isabelle-style user experience.

      The thing with Isabelle’s “roundup” algorithm is that it seems to rely heavily on the idea that the instances of a locale in scopes are fully top-level, so that you can walk through them and eagerly install all their operations into the appropriate scope. In this sense, Isabelle’s implementation of locales does not involve implicit coercion at all. In a dependent type theoretic setting, we must account for things like families of structures and ensuring that we can project components from these as well. For example, if we have a constant \(M \colon I \to \mathsf {Monoid}\), we will need to be able to call things like \((M~i).\mathsf {join}\) which would involve passing through the coercion to semigroups, etc. I am not sure how to capture something like that via a roundup-like algorithm.

      For this reason, I believe that the best foundation for Pterodactyl’s handling of algebraic hierarchies will be Sakaguchi’s labelled preorders as deployed in Rocq.

      A clean-room implementation of Sakaguchi’s labelled preorders [01HK]

      In order to learn how the algorithm works, I built a clean-room generic implementation in Swift of the labelled preorder structure following Sakaguchi’s algorithm. (Oh, did I mention I’m using Swift?)

      Our case will be a bit simpler than that of Rocq. In Rocq, coercions can be between arbitrary things, and therefore the vertices must include definitional equivalence classes of terms. That seems very tricky! We will be using a more restricted kind of coercion in Pterodactyl, where the vertices are only theory names. (We might later on also support coercions to sorts like those of types and functions, like Rocq does, which would not be difficult.)

      As a result, the only thing that we need to use expensive definitional equality checks for is the coercion paths themselves. It will indeed be pretty costly to install coercions, but resolving them will be very cheap: it is a single lookup in a hashtable by a totally discrete key. My code is available here.

      I am not certain that we will use literally this code (abstracting and modularising too early can be hazardous), but it’s a good start.

      A focused vision for Project Pterodactyl [01H3]

      After a few very enlightening conversations following my HoTTEST seminar talk “Is it time for a new proof assistant?”, I have realised that one of the more important aspects of my plans for Pterodactyl is its focused and restricted vision. I cannot promise that we will succeed, but I do think that by not trying to be all things to all people, we may be able to avoid some likely ways of biting the dust.

      We are not building a general-purpose programming language [01H4]

      Any implementation of dependent type theory is a programming language of sorts, following the Curry–Howard correspondence, but I have come to believe that to build an actually good programming language (like OCaml, Lean, Rust, or Idris) is a very different task from building an actually good proof assistant (like Rocq, Lean, or Isabelle).

      If you have enough resources, you can do both at the same time (like Lean). If you don’t have enough resources, I think you end up with something that is going to be inadequate as either a general-purpose programming language or as a proof assistant.

      I do think that this is a point we could revisit in the future, but only after we have achieved our primary goals. Not having general-purpose programming as a primary goal doesn’t mean we can’t write programs in the language; I think that, instead, punting on things like “Being competitive with OCaml and Rust” means that there will be more space for ambitious dependent-type-native people to explore the possibilities of dependently typed programming without having to answer questions for which we don’t yet have good enough answers.

      We have no plans to self-host, ever [01H5]

      When you build a language you really like, it is natural to want to rewrite its compiler in itself. This is a reasonable impulse, but I believe that it can also create inertia and painful coupling as you have to negotiate changes to the language with changes to the compiler in both directions rather than in only one direction.

      Here’s the thing: if we were to write a highly-performance-constrained system (like a proof assistant) in itself, the proof assistant’s compiler and execution model would need to immediately be competitive with state-of-the-art programming languages with vastly more resources and expertise behind them. I do think that we can build something that is competitive with Agda, but I do not think we could build something that is competitive with both Agda and Rust or OCaml at the same time.

      I believe that it is a good goal to have a system that can do both. But I think that in order to get there in a resource-constrained environment, it is very important that the goals be achievable separately. If we have to achieve both in order to achieve one, we will realistically achieve none.

      We do not have plans for general-purpose metaprogramming [01H6]

      One of the most interesting things about Idris 1, Agda, and Lean is their approach to metaprogramming. In either system, you can hook directly into their elaboration monad and write metaprograms directly in the language, and then designate certain of these metaprograms as tactics or macros.

      I think that this is an excellent model, but one of the reasons I am planning to shy away from it is that I believe it introduces a great deal of coupling between user-land code and the implementation details of the system (including its representation of syntax, its approach to elaboration and the suspension of elaboration problems, its approach to unification, etc.).

      This is similar to the self-hosting problem; with enough resources, you can pat your head and rub your belly at the same time, but I believe that avoiding the coupling that metaprogramming introduces for the longest time possible will increase our probability of achieving our primary goals.

      We do have plans for procedural reasoning [01H7]

      Some community members have expressed skepticism about what might be lost in reducing everything to a problem-oriented programming model like that of “The View From the Left”. For example, a large part of typical tactic scripts in Rocq amounts to procedurally generalising goals and calling eliminators, and this is indeed well-handled by the McBride—McKinna model; on the other hand, there are many other useful pieces of tactical reasoning like apply f or eapply f that aren’t discussed in that paper. If we built a system in which you could not easily backchain through a lemma, it would indeed be a pretty unrewarding system to use.

      The particular case of backchaining through lemmas can, however, be addressed within a very small extension of the McBride–McKinna model. For this, we will need what might be referred to as the “view from the right”. There is an analogy to be had here:

      • McBride and McKinna defined a general notion of “elimination operator”, and devised a pattern matching notation for it.
      • We seem to need to define a general notion of “introduction operator”, and then devise a co-pattern matching notation for it.

      In Epigram, we can think of the ability to return a value (written \(\Rightarrow \mathit {val}\)) as the beginning of a “view from the right”, which is just lacking any kind of right-handed decomposition. Our goal is to add this decomposition.

      Consider the case of showing that a particular sum \(\sum _{x:\mathbf {1}}x=()\) is a proposition, using a lemma about the closure of propositions under internal sums. Here is our initial proof state as it might appear in our editor:

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example}~\color {gray}[?\colon \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=()] \end {aligned} \]

      Next, we use the backchaining introduction operator, which generalises the usual “return” / \(\Rightarrow \) co-gadget of Epigram to allow for subgoals.

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}~\color {gray}[?\colon \mathsf {isProp}~\mathbf {1}] \\ &\mathsf {example}.\mathsf {famIsProp}~\color {gray}[?\colon (x:\mathbf {1}) \to \mathsf {isProp}~(x=\mathbf {1})] \end {aligned} \]

      Note that with records, we can easily arrange for the subgoals of to have more human-readable names than \(\pi _1,\pi _2\), as we’ve done above. The first goal is easy to solve using another lemma; that lemma has no subgoals, so that branch is finished off like so:

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~\color {gray}[?\colon (x:\mathbf {1}) \to \mathsf {isProp}~(x=\mathbf {1})] \end {aligned} \]

      In the second branch, we can abstract the variable.

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~x~\color {gray}[?\colon \mathsf {isProp}~(x=\mathbf {1})] \end {aligned} \]

      Next, we backchain through yet another lemma, namely that propositions are sets.

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~x~\Rightarrow \mathsf {propsAreSets}\\ &\mathsf {example}.\mathsf {famIsProp}~x~\color {gray}[?\colon \mathsf {isProp}~\mathbf {1}] \end {aligned} \]

      Finally, we finish up the problem with a lemma that has no subgoals.

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {propsAreSets}\\ &\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {unitIsProp} \end {aligned} \]

      Personally, I find the above to strike a good balance between readability and writeability while maintaining the very important procedural aspect of how mathematicians write proofs; it is an extremely small generalisation of the McBride–McKinna model.

      We can workshop the notation and improve it, but I think the underlying idea here is viable. For those who think “But that is exactly what we already had with tactics”, that is actually my entire point: I don’t want to get rid of procedural tactical reasoning, but I do want to find a way to incorporate it into a problem-oriented notation that mostly documents itself in connection with editor facilities to see the proof state at a given step.

      I won’t say that this solves all problems, but I hope it gives some impression of the methodology by which we will tackle procedural reasoning.

      Stepping through proofs is important [01H8]

      It is important to be able to see what the goal was at a given point in a proof that has already been completed. If we return to our example of right-handed procedural reasoning:

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {propsAreSets}\\ &\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {unitIsProp} \end {aligned} \]

      We could instrument the language server to emit either tooltips or expandable inlays on each \(\Rightarrow \) or \(\Leftarrow \) that will display the goal that is being refined. For example, I plan to make it so that if you select the second \(\Rightarrow \) in the above, the editor would display something like \[ \mathsf {isProp}~\mathbf {1} \] and if you select the third \(\Rightarrow \), the editor would display something like \[ x:\mathbf {1}\vdash \mathsf {isProp}~(x=())\text {.} \]

      Ideally, selecting the occurrences of the backchained lemmas on the right-hand side would lead to a display that reveals exactly how they have been specialised for the goal. For example, if you select the occurrence of \(\mathsf {propsAreSets}\) the editor might display something like the following:

      \[ x:\mathbf {1}, \square :\mathsf {isProp}~\mathbf {1}\vdash \mathsf {propsAreSets}~\mathbf {1}~\square ~x~() : \mathsf {isProp}~(x=()) \]

      Jon Sterling › Blog [007W]

      This is my blog, in which I write about a variety of topics including computer science, mathematics, and the design of tools for scientists. See also my “creek” for shorter-form posts; or see just my book reviews; I also publish weeknotes. You can subscribe to the Atom feed if you prefer.

      Generalised quasi-coherence, sober spaces, and spatial algebras [0LVV]

      Lingyuan Ye and I have put on the arXiv a new version of our paper, Domains and Classifying Topoi, which is currently under review. We have made an important improvement, correcting an terminological error that I deeply regret.

      The error I am referring to is not a mathematical or technical one, but rather an issue of clarity and terminological coherence. This work is about transplanting Ingo Blechschmidt’s notion of synthetic quasi-coherence from algebraic geometry to domain theory. There is a very general way to state the synthetic quasi-coherence principle in the context of any algebraic theory \(\mathbb {T}\) that has a notion of module, which is Definition 18.18 of Bleschmidt’s PhD thesis.

      Definition. Synthetic quasi-coherence [0LVX]

      Let \(R\) be a model of \(\mathbb {T}\). An \(R\)-module \(E\) is called synthetically quasi-coherent when for any finitely presented \(R\)-algebra \(A\), the canonical \(R\)-module homomorphism \[E\otimes _R A\multimap E^{\hom _{\mathbf {Alg}(R)}(A,R)}\] is invertible.

      We now consider a special case of Definition [0LVX].

      Definition. Spectrum and observational algebra [0LVY]

      Let \(R\) be a distinguished \(\mathbb {T}\)-model that we shall think of as a “line object” generating some kind of geometry. We define the observational algebra of a set \(X\) to be the power \(\mathcal {O}(X) :\equiv R^X\); conversely, we define the spectrum of an \(R\)-algebra \(A\) to be the space of homomorphisms \(\operatorname {Spec} A :\equiv \hom _{\mathbf {Alg}(R)}(A,R)\). These operations are functorial and adjoint:

      \[ \mathcal {O}\dashv \operatorname {Spec}\colon \mathbf {Alg}(R)^{\mathsf {op}}\to \mathbf {Set} \]

      Observation. Quasi-coherence of the line object [0LVZ]

      Then the line object \(R\), viewed as a module over itself, is (by definition!) synthetically quasi-coherent if and only if the counit homomorphism \(\epsilon \colon A\multimap \mathcal {O}\operatorname {Spec} A\) is invertible for every finitely presented \(R\)-algebra \(A\), noting that \(R\otimes _R A = A\).

      The definition of quasi-coherence that we inherit from Ingo Blechschmidt is fixed specifically to finitely presented algebras. The idea of some recent works, including A Foundation for Synthetic Stone Duality and our own paper, is to consider versions of synthetic quasi-coherence with respect to larger classes of algebras (particularly, the countably presented ones).

      Our own ideological contribution was to make the trivial observation that synthetic quasi-coherence of the line object is really about characterising the fixed points of the adjunction \(\mathcal {O}\dashv \operatorname {Spec}\). This reflects our perspective that the fundamental property of concern is whether something is a fixed point of this adjunction, not whether it is (e.g.) finitely presented, countably presented, etc. In specific models, there is a direct correspondence between the two notions, but it is another matter entirely to design a civilised axiomatics.

      Where we went wrong, terminologically [0LW0]

      When we wrote this paper, we were thinking only of the quasi-coherence of the line object, and this emphasis caused an unfortunate bit of semantic drift. In particular, we introduced the following terminology:

      1. We called the fixed points of \(\mathcal {O}\dashv \operatorname {Spec}\) in \(\mathbf {Set}\) “affine spaces”.
      2. We called the fixed points of \(\mathcal {O}\dashv \operatorname {Spec}\) in \(\mathbf {Alg}(R)\) “quasi-coherent algebras”.

      Although there is an argument to be made that the terminology of “affine spaces” above is reasonable, our use of “quasi-coherent algebra” in the paper was extremely misleading. Indeed, these are the algebras with respect to which the line object is quasi-coherent, not the actual quasi-coherent algebras!

      Synthetic topology to the rescue [0LW1]

      Luckily, our carelessness with the terminology was not difficult to fix. In fact, topology already has a reasonable terminology for the fixed points of \(\mathcal {O}\dashv \operatorname {Spec}\) adjunction:

      1. A fixed point of \(\mathcal {O}\dashv \operatorname {Spec}\) in \(\mathbf {Set}\) is a sober space.
      2. A fixed point of \(\mathcal {O}\dashv \operatorname {Spec}\) in \(\mathbf {Alg}(R)\) is a spatial algebra.

      Under this terminology, the synthetic quasi-coherence axioms that have appeared in the literature should be rephrased as follows:

      1. The synthetic quasi-coherence principle of Blechschmidt’s PhD thesis and A foundation for synthetic algebraic geometry should be stated as follows: Every finitely presented \(R\)-algebra is spatial.
      2. The synthetic quasi-coherence principle of A Foundation for Synthetic Stone Duality and Domains and Classifying Topoi should be stated as follows: Every countably presented \(R\)-algebra is spatial.

      Let’s be careful with the terminology… [0LW3]

      I am hoping that others will adopt the terminology and axiomatics that we have proposed. Much of the current work in this area of racing to pick low-hanging fruit, and in this rapid movement I fear that a great mess is being made of the terminology. For example, A Foundation for Synthetic Stone Duality is a great work from which we have taken a lot of inspiration, but it defines an “overtly discrete type” to be one that is a sequential colimit of finite sets, and although this may be equivalent to the correct definition in the intended model, it is not in my opinion a reasonable definition in axiomatics: a space \(X\) being overt has nothing intrinsic to do with presentation by finite things, and has everything to do with the existence of a left adjoint to \(X^*\colon \mathcal {O}(\mathbf {1})\to \mathcal {O}(X)\); being discrete likewise has nothing to do with finitude, and everything to do with the diagonal \(X\to X\times X\) being an open immersion.

      I regret having added to the messiness in this area, but I am really hopeful that we can clean things up before it is too late and the bad terminologies and definitions are writ in stone.

      Primitive identity types and proof-relevant unification [01LB]

      I’ve been thinking about the Elimination with a Motive transformation as modernised in terms of type theoretic equivalences. One thing that is striking me right away is that this is going to lead to a pretty scary code blow-up. For instance, if we only consider the basic analysis and the solution rule, a simple construction like the pasting of identifications is going to result in a really large term involving four calls to based path induction, each themselves with increasingly complicated motives. Doing this systematically in the form of unifiers-as-equivalences would result in some even more complicated terms.

      Agda gets around this by not actually constructing the equivalences; Cubical Agda and Mikan, however, need the left-inverse part of the equivalence, and even this quickly blows up when types have more than a couple indices, as the Mikan team have recently noted. Project Pterodactyl would likewise need the left-inverse part as well.

      I was thinking that perhaps one way to deal with this problem would be to use a bit of a hybrid approach. The extreme position is to elaborate everything in sight to eliminators, but a middle ground might be to extend the core language with a schema for the various unification rules and their left inverses with the appropriate computational behaviour. Every time a proof-relevant unification rule used in the elaboration process, a new abstract top-level declaration is inserted that has (by fiat) the correct reduction rules. Because the operator cannot write these terms, we can make them very compact and probably even avoid annotating them with motives.

      Doesn’t this beat the point of eliminating dependent pattern matching? I don’t think so. In Elimination with a Motive, eliminators are playing two distinct roles:

      1. User-land pattern matching and recursion are reduced to core eliminators.
      2. Specialisation of motives against targets is achieved internally using a built-in identity type and its eliminator.

      What I am proposing is that the specialisation step might be achieved using any computationally well-behaved primitives that the built-in identity type comes equipped with. Even if something can be reduced to a very complicated instance of based path induction, we don’t necessarily need to do so. Moreover, doing so may introduce usability problems (where two things that ought not be definitionally equal from the operator’s point of view become equal by coincidence).

      Maybe another way to put it is: it is a coincidence that the user-facing identity type is the same as the identity type used to eliminate dependent pattern matching. If the operator defines their own user-land identity type, then pattern matching definitions defined in terms of it will be reduced to the user-land based path induction principle, but in order to achieve specialisation against the elimination target, the internal identity type (and its rules, whatsoever they are!) will also be used.

      Project Pterodactyl’s layered architecture [01KF]

      I have made a great deal of progress with Pterodactyl in the past week. One thing I have been working on is modularising the system, which I resisted doing for a while because it was unclear which parts needed to depend on which. But now a reasonable architecture is emerging. Pterodactyl is split into several Swift libraries:

      1. PterodactylCore contains the core syntax, semantic domain, evaluator, and conversion checker. This library is completely indepenent from the rest of the system.
      2. PterodactylKernel contains the rules of Martin-Löf type theory, implemented as closure conditions on functions that produce core terms from an environment and a goal. I will discuss this more below. This depends only on PterodactylCore and is completely independent of concrete syntax. The kernel is trusted, and its outputs are (in LCF style) unforgeable.
      3. PterodactylSyntax contains the concrete syntax of the Pterodactyl, implemented with Roslyn-style homogeneous “green trees”. This library includes the layout lexer and the parser. This library is independent of the other parts of the system.
      4. PterodactylElaborator glues the kernel to the concrete syntax by means of a function inductively converting concrete syntax to calls to the kernel.
      5. PterodactylBuild contains what is usually called the “driver” of a proof assistant: the routine that processes entire modules and workspaces. Our driver is incrementalised at file-prefix granularity, using the swift-llbuild2 infrastructure. See also The CAS model of incremental build systems for previous discussion of this.
      6. PterodactylLanguageServer is the only executable at the moment, and it depends on all of the above—mainly via PterodactylBuild. The language server keeps track of the communication with the language client via RPC, keeping track of buffer state, calling the build system at appropriate times, and sending both diagnostics and subgoal displays to the language client.

      Kernel vs. Elaborator

      My separation of the kernel from the elaborator is unconventional for dependently typed systems: usually an elaborator a bit nest of mutually recursive functions that are trusted to produce valid core language terms. This coupling of surface syntax to the rules of the core type theory is totally unnecessary, as any inductive definition can obviously be translated into a collection of closure conditions. This makes the kernel testable independently of the concrete syntax, and (indeed) it can be run with many different concrete syntaxes if desired.

      The basic forms of judgement of (Pterodactyl’s version of) Martin-Löf type theory are represented in Swift as protocols with methods valued in an abstract type Trust<V>.

      public protocol ElabType {
  func elabType(
    _ env: Environment,
    size: Size<Value>?
  ) async throws(ElabError)
  -> Trust<Term.Type_>
}

// Checking mode
public protocol ElabTerm {
  func elabTerm(
    _ env: Environment,
    type: Value.Type_
  ) async throws(ElabError)
  -> Trust<Term>
}

// Synthesis mode
public protocol ElabTypedTerm {
  func elabTypedTerm(
    _ env: Environment
  ) async throws(ElabError)
  -> Trust<(Value.Type_, Term)>
}

      An example piece of trusted kernel code is the formation rule of dependent function types, as quoted below:

      public struct FunctionFormation: ElabType {
  let binder: TypedBinder
  let fam: ElabType

  public init(binder: TypedBinder, fam: ElabType) {
    self.binder = binder
    self.fam = fam
  }

  public init(dom: ElabType, cod: ElabType) {
    self.init(binder: TypedBinder(name: nil, type: dom), fam: cod)  // consider adding explicit weakening rule to use in 'fam' here
  }

  public func elabType(_ env: Environment, size: Size<Value>?) async throws(ElabError) -> Trust<Term.Type_> {
    let env_dom = env.extendingNamespace(.machine("dom"))
    let idom = try await binder.type.elabType(env_dom, size: size).value

    var env_fam = env
    env_fam.extendNamespace(.machine("fam"))
    let boundName = binder.name.map(Name.user(_:))
    await env_fam.bind(name: boundName, type: idom)
    let ifam = try await fam.elabType(env_fam, size: size).value
    return Trust(.funType(dom: idom, boundName: boundName, fam: ifam))
  }
}

      Finally, the elaborator converts concrete syntax into calls to the above. In the concrete syntax a dependent function type can appear in iterated form, so this must be folded up into multiple applications of the formation rule as below:

      extension SyntaxTreeCursor {
  var depFunTypes: ElabType? {
    guard case .depFunType = kind else { return nil }
    var binders: ArraySlice<TypedBinder> = []
    for (ix, subtree) in subtrees.enumerated() {
      if let binder = subtree.typedBinder {
        binders.append(binder)
      } else {
        guard ix == binders.endIndex else { return nil }
        binders.reversed().reduce(subtree) { partialResult, binder in
          FunctionFormation(binder: binder, fam: partialResult)
        }
      }
    }

    return nil
  }
}

      The query-based build system

      Our build system is query-based and, as I mentioned, incrementalised. Here is an example of a query that computes the top-level environment that results from elaborating a given source tree (an abstraction in CAS of a group of files):

      struct ToplevelEnvOfSourceTree: AsyncFXKey {
  enum ValueType: Codable, FXValue {
    case success(ToplevelEnv)
    case circularImport
  }

  let sourceTreeId: LLBDataID

  public static let versionDependencies: [any FXVersioning.Type] = [Keys.SourceTree.GetDependencyGraph.self, ElaborateUnit.self]

  func computeValue(_ fi: llbuild2fx.FXFunctionInterface<Self>, _ ctx: TSCUtility.Context) async throws -> ValueType {
    let graph = try await fi.request(Keys.SourceTree.GetDependencyGraph(sourceTreeId: sourceTreeId), ctx)
    guard let vertices: [UnitName] = graph.topologicalSort else { return .circularImport }

    var env = ToplevelEnv(decls: [:])
    for unit in vertices {
      let unitResult = try await fi.request(ElaborateUnit(sourceTreeId: sourceTreeId, unitName: unit), ctx)
      env.decls.merge(unitResult.newDecls) { _, new in new }
    }

    return .success(env)
  }
}

      When elaborating an actual source unit, we use the dependency graph to narrow the global source tree to just the parts that the unit is allowed to depend upon. Then we get compute the top-level environment for the narrowed source tree using the above, and proceed with elaboration. Here's a prefix of the unit elaboration query:

      public struct ElaborateUnit: AsyncFXKey {
  public struct ValueType: Codable, FXValue {
    public var newDecls: OrderedDictionary<QName, TypedDataID<GlobalDef>>
    public var feedbacks: [Feedback]
  }

  /// The global source tree
  public let sourceTreeId: LLBDataID
  public let unitName: UnitName

  public init(sourceTreeId: LLBDataID, unitName: UnitName) {
    self.sourceTreeId = sourceTreeId
    self.unitName = unitName
  }

  public static let versionDependencies: [any FXVersioning.Type] = [
    Keys.SourceTree.NarrowToUnit.self, ToplevelEnvOfSourceTree.self, Keys.SourceTree.GetUnitBlobId.self, Keys.Blob.ParseDocument.self, ElaborateDecl.self
  ]

  public func computeValue(_ fi: llbuild2fx.FXFunctionInterface<Self>, _ ctx: TSCUtility.Context) async throws -> ValueType {
    let narrowedSourceTreeId = try await fi.request(Keys.SourceTree.NarrowToUnit(sourceTreeId: sourceTreeId, unitName: unitName), ctx)
    let blobId = try await fi.request(Keys.SourceTree.GetUnitBlobId(sourceTreeId: sourceTreeId, unitName: unitName), ctx).blobId
    let tree = try await fi.request(Keys.Blob.ParseDocument(blobId: blobId), ctx).tree
    let cursor = SyntaxTreeCursor(tree: tree, utf16Offset: 0)

    switch try await fi.request(ToplevelEnvOfSourceTree(sourceTreeId: narrowedSourceTreeId), ctx) {
      // ...

      As you can see, queries are versioned. This is important because the function cache may be stored on disk! Versioning allows these caches to be invalidated when an incompatible version of Pterodactyl is being run.

      All the subrequests are, naturally, cached in the database which allows top-level environments to be rapidly reconstructed as-needed without re-elaborating anything. As I mentioned before, the granularity of incrementalisation is file prefixes: it might be nice to have declaration-level granularity, but I think that is not possible in any system with type classes, an implicit coercion graph, or any other feature that introduces implicit dependencies. Our incrementalisation is, however, insensitive to changes in position that do not lead to semantic differences.

      It remains to be seen if the build system will be performant: llbuild2 has never been used in this way, and there may be bottlenecks that we need to resolve, or mistaken aspects of the design that we must revisit. It will be difficult to tell until we can run Pterodactyl on a codebase of reasonable size, which is not currently possible because so little of the language is in place.

      Am I the only one still wondering what is the deal with linear types? [01KB]

      One thing that is still pretty hazy to me is the claimed relationship between “linear types” (qua Cyclone/Rust/OxCaml/Swift/Hylo/etc.) and actual linear logic. I have gotten the feeling that people have spent years claiming that they have created a linear type system, etc., or talking about how their system is affine rather than linear when it is not clear to me what the precise relationship is to either affine or linear logic, etc. There are intuitions at play, but sometimes these intuitions are too far away from the mathematics to justifiably inform a point of view on either syntax or semantics or both. For example, there’s a lot of hand-waving that starts with intuitions about “the number of aliases in the past / future at runtime” and ends with “and this is why we have this modality”, but the former is so vague that I struggle to accept it as the basis for a mathematical definition or claim.

      I watched Guillaume Munch-Maccagnoni’s ML ’24 talk Is there a use for linear types because the abstract promised to shed some light on this and related questions, but I have to say that the talk, shall we say, left me a bit cold: the abstract promised to shed some light, and all I can say after watching it twice is that the talk…also promised to shed some light. By the time Guillaume got to the criticisms of prior work on linear types, it seems he did not have enough time to make them precise enough to be evaluated on a mathematical basis; perhaps this was not the venue to do so, but I would have loved if he could have got a bit more technical here, as there is an opportunity to make some points understood that are actually not understood by almost anybody (including myself).

      For example, he alludes to a “non-standard (and computationally uninteresting) interpretation of [the bang modality]” in what I assume is the paper Linearity and Uniqueness: An Entente Cordiale, but he doesn‘t ever say what it was! I assume he had planned to address this in the Q&A but unfortunately nobody asked the pertinent question. My guess is that the dereliction rule in that paper looks a little dodgy because it seems to require a cartesian context (contrast with Alms), but I really have no idea if that was the actual problem. It would have been nice if he could have said what the precise problem was. Similarly with the “overly-constrained definition of linearity not suitable for resource management”, which is something I definitely want to understand.

      As Guillaume points out in his talk, the “opposition” or “duality” (which I agree not to be substantiated on a mathematical basis) between uniqueness and linearity really does make the system a lot more complicated, and it is part of the “rat king” of modalities that OCaml is presently turning into. If there is a practically and theoretically sound viewpoint that allows us to rethink this distinction, it is very urgent that we understand it now rather than later. That is why I sincerely hope that Guillaume will be willing to expand on his very interesting arguments in a position paper aimed at a mathematically literate audience. Guillaume is one of the very few people in the world who understands both sides of this divide very well, and I think the community would benefit greatly from him having the opportunity to intervene at a more technical level.

      In the meanwhile, I have been reading with great interest the short paper Towards a linear functional translation for borrowing, written by Guillaume’s student Sidney Congard. Technical contributions in this area are very welcome, and I’m eager for more.

      NewsRadar is now NewsDrawer, and it’s lickable [01K5]

      Somehow I have managed to get some time in the past couple weeks to work on my newsreader app, which I had been calling NewsRadar. Last week I had an epiphany, and realised it ought to be named NewsDrawer — not only an homage to one of the best user interface controls left on the cutting room floor, but also as a metaphor for how I want the app to function: articles are calmly deposited into appropriate “drawers” governed by sophisticated database queries that the user can write themselves.

      My renewed energy to work on NewsDrawer started a week or two ago when I began prototyping a feed organiser window to solve a frustration that I have with most newsreading apps. The issue is that when the only way to manage subscriptions is messing around in the sidebar, things quickly get out of control as soon as you have more than 10 feeds and several categories. So I want to have a professional-grade user interface for managing these things quickly. In last week’s weeknotes I put a screenshot of my first attempt, but it was really bothering me how hideous the toolbar is when toolbar button icons are simply SF Symbols glyphs.

      As a first step, I began drawing some classic-style toolbar icons using the amazing Sketch app, which is really one of the last great professional Mac apps.

      Hand-drawing vector toolbar icons drawn in Sketch, inspired by the classic OmniWeb.

      I am not an icon designer, or a visual designer of any kind, but this was extremely easy. I adapted my toolbar to use these icons, but then I realised that the nice shaded icons looked out of place in macOS Tahoe’s horrible “sea of white” design, so I replaced the window chrome with a slight gradient inspired by Mac OS X 10.4 (Tiger). But if you give a mouse a cookie, he will ask for a glass of milk—naturally, the horrid window buttons that we have endured since Mac OS X 10.10 (Yosemite) began to chafe, and I of course needed to re-draw these. Anyway, it seemed that the time had arrived to bring back my old AquaUI project (but done better), so I set to work, drawing various controls in Quartz. As you can see in the screenshot below, I have done a far better job than last time drawing the window traffic light controls.

      NewsDrawer’s feed organiser window, with Aqua controls and window chrome drawn in Quartz. The clumsily shadowed NSSearchToolbarItem stands out like a sore thumb, and I may need to re-draw it from scratch.

      Although the styling is inspired by Tiger’s version of Aqua, everything is drawn programmatically in Quartz using NSBezierPath, NSGradient, and NSShadow. You may have noticed the little lozenge-shaped button in the upper right-hand corner; this is of course the toolbar toggle button, which is one of the most beloved affordances of Mac OS X that was lost in 10.7 (Lion). This is actually really easy to restore, as the vestigial functionality is still present.

      I have restored the traditional toolbar toggle lozenge to NSWindow, which was lost in Mac OS X 10.7 (Lion).

      Naturally, the inactive window state introduces some subtle transparency and pinstriping, which I have implemented as a custom NSColor that tiles a programmatically drawn NSImage.

      Obviously the inactive state has subtly pinstriped window chrome.

      What comes next is a thorough redesign of the main feed view, which is currently using a sidebar. Unfortunately, the new behaviour of sidebars starting from macOS Tahoe is extremely hostile to the user and does not go with the Aqua styling that I am using, so I need to rethink how this should work. I am considering reconstructing from scratch the old non-full-height sidebars from Mac OS X, but this will be a lot of work. (Why not a drawer? As the HIG pointed out in the old days, not everything should be a drawer; I think this is an example of something that really ought to be a sidebar.)

      Disentangling unification and implicit coercion [01JQ]

      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?

      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:

      1. Rocq’s coercion mechanism is very predictable but its unification is not.
      2. 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?

      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

      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:

      1. 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.
      2. 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!

      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?

      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.

      It Is Wrong To Take Life: language & mockery in the Shing era [01JN]

      In City of Illusions, the Shing have shattered the old League of All Worlds and dominated the Earth—whose people they allow to live quiet pastoral lives subject to only one rarely enforced Law: It Is Wrong To Take Life.

      City of Illusions by Ursula K. Le Guin. Cover art by Chris Foss (source: Literary Hub).

      The power of the Shing, the legend says, is that they are able to mindlie—a skill that goes beyond the normal human telepathic capabilities in the Hainish universe. Everything about the Shing is some kind of falsehood or mockery. They have elevated animals with the power of speech: flocks of birds chatter with human words, and wild pigs and chickens squawk the Shing Law to human hunters (“It is wrong to take life!”).

      Le Guin’s focus on mockery and falseness as the form of evil reminds me of Tolkien. In The Silmarillion, Melkor’s every prideful effort to emulate God is transformed into a mockery and a counterfeit of the object of his imitation. That something is “untrue” is what makes it evil. It is very clear that the humans of Shing Earth see things in much the same way—the pleading appeal of the pig and the chicken to the Shing’s Law against killing is a nuisance and a symbol of a poisoned world whose right and natural order has been perverted.

      The narrative perspective of City of Illusions is that only a race in which killing runs deep could conceive of an absolute Law against all killing; and the Shing do things worse than killing anyway, like erasing people’s memory or letting people kill each other. Thus reassured of the hypocrisy and essential falseness of the Shing, we can get on with the “liberation” of all the Earth’s species from Laws that go against the true natural order, which is (naturally) that animals who cannot speak Man’s languages must serve Man in the the only form intelligible to his insatiable appetite: protein, blood, and fat.

      Perhaps it is true that the Shing do protest too much and that their Law testifies to their own vicious nature, but of all known races in our own known universe, there is none so dedicated to killing as Humankind, and our own statutes provide for the lawful killing of humans and non-humans alike at scales that defy belief and all sense of morality—even Human morality. City of Illusions suggests that even if the birds and pigs were given intelligible voice, Man would view their pleas as mockery.

      The magnificent churches of Cambridgeshire [01JK]

      This vacation, my mom came to visit us for two weeks. This is the first time she’d been to England in four decades, and the first time I’d been able to spend the holidays with her in many years. It was a great visit! One of the things she is very interested in is old churches, and there is no better place to go than Cambridgeshire in search of old churches.

      St Andrew’s Church, Girton [01JL]

      Our first outing was to the beautiful St Andrew’s Church in Girton, not a ten minute walk from our house. St Andrew’s is quite old, with some of the construction dating back to the 13th century, though most what stands today was rebuilt in the 15th and 16th centuries. Like essentially all churches of this age, it was originally Catholic until the dissolution of the monasteries by Henry VIII.

      A small blue door on the side of St Andrew’s Church, Girton.

      Ely Cathedral [01JM]

      We spent a day in Ely to experience the magnificent Ely Cathedral. I can honestly say that I have never seen something as grand as this in my entire life, and it is a shame that it took a relative visiting to get us to visit it.

      The outside and inside view of Ely Cathedral’s octagon tower.
      The choir of Ely Cathedral.

      Most amazing to me was to stand in the presence of Byrhtnōð’s remains, interred in a niche within the cathedral alongside several other Saxon benefactors, since I had encountered The Battle of Maldon in my study of Old English many years ago.

      Burial niches inside Ely Cathedral, notably including the remains of Byrhtnōð, who perished in a hopeless last stand (The Battle of Maldon) of the English against the Viking invaders in 991.

      Another thing I found fascinating with the medieval engineering of the tower, whose interior is a a timber construction made fast by pegwork.

      Medieval timberwork in the octagon of Ely Cathedral.

      I would very much like to return and spend more time there. My only disappointment was, perhaps in light of the mixed use of the cathedral, its nave is filled with rows and rows of cheap stackable plywood chairs with metal legs—a culturally inappropriate and barely functional adornment for so grand a space.

      2025 Year in Review [01JD]

      A year of reading fiction [01JE]

      Reflecting on 2025, the biggest change I have made to my life is that I started reading fiction again after many years of reading only mathematics. Glancing through my reading corner and The Jon Sterling Review of Books, I’ve read the following books in the past year:

      1. West of Eden, Winter in Eden and Return to Eden by Harry Harrison.
      2. The Fountains of Paradise by Arthur C. Clarke
      3. Children of Time, Children of Ruin, and Children of Memory by Adrian Tchaikovsky
      4. The City and the Stars by Arthur C. Clarke
      5. Alien Clay by Adrian Tchaikovsky
      6. The Looking Glass War and Call for the Dead by John le Carré
      7. Saturation Point by Adrian Tchaikovsky
      8. The Dispossessed by Ursula K. Le Guin
      9. Foundation and Empire by Isaac Asimov
      10. Children of Dune, God Emperor of Dune, and Heretics of Dune by Frank Herbert
      11. The Godfather by Mario Puzo
      12. Rocannon’s World by Ursula K. Le Guin
      13. Rendezvous with Rama by Arthur C. Clarke
      14. The Three-Body Problem, The Dark Forest, and Death’s End by Liu Cixin
      15. Dinosaur Wars: Earthfall by Thomas Hopp

      These books fall into a few categories for me. There is the quick low-calorie read (e.g. Alien Clay and Saturation Point), the good long read (Adrian Tchaikovsky’s Children series and Liu Cixin’s Three Body Problem), the outrageous concept that I can’t look away from (Harry Harrison’s Eden trilogy, Frank Herbert’s God Emperor), and the beautiful art-novel that I can’t stop thinking about months after reading it (The City and the Stars, The Dispossessed, and Rendezvous with Rama).

      As we draw near the new year, I am settling into The Lathe of Heaven by Ursula K. Le Guin.

      Joy in coding: Swift is fun [01JF]

      I‘ve been doing more software engineering this year than in past years, where my coding was essentially limited to work on Forester. This year I’ve worked on a few projects, including NewsRadar (see my introductory blog post) and Project Pterodactyl. Both of these are written in Swift (though the latter may change), and I have to say that Swift is a pretty good language that is moving in a pretty good direction.

      We’ll see how I feel about it as time goes on, but frankly it is sparking more joy for me than OCaml coding these days, where I seem to always get sucked into dealing with bad standard library choices, bad tooling (the Hell of modern opam), and promising but incomplete transitions (e.g. the Dune transition and the effects/Eio transition). I just want something where I can write reasonable code right now without friction, I can actually use a debugger in an actual IDE, etc. Swift seems to be fine.

      I don’t mean any harm to the OCaml developers; I love the OCaml project and am excited for its future. I also understand that some of the things I’m finding frustrating may even be solvable today and might be characterised as a “skill issue” on my part. The problem is, I don’t want to have to solve these things. I just want things to work properly without me having to constantly troubleshoot stuff that is either broken or confusing or, worse, “documented” in such a way that you can find out everything about every option but never see how to actually do anything (as in the Dune documentation). LLMs don’t help with this problem, because they are always subtly out of date and then start to make up “reasons” for why things aren’t working as predicted.

      Another year of Forester [01JG]

      This year has seen the release of Forester 5.0, thanks to the generous support of ARIA who engaged Kento Okura and myself on a contract to make a number of improvements to Forester. In the coming year, we are very grateful to Tarides and the OCaml Software Foundation for stepping in with sponsorships that will assist us in the next phase of development, during which I hope to bang out many bugs and make Forester both more reliable and futureproof.

      Changes in College [01JH]

      This year, I joined the Tutorial team in my College. So far that’s been a very good experience and hasn’t added a ton of work to my plate (crossing fingers for next year). I am glad I did it when I did, because our amazing Senior Tutor Jackie Tasioulas is reaching the end of a ten year term and will be leaving us to become the next Principal of Newnham College. It is a bit of luck that I managed to get in whilst I could still learn from Jackie’s immense institutional knowledge and wisdom. However, I’m very happy for Newnham College who will be getting one of the finest people I know.

      The CAS model of incremental build systems [01IP]

      I have continued on my quest to understand and compare different architectures for demand-based/query-based compilation and elaboration. This week I have been exploring the llbuild2fx library from Apple, which its authors describe as a fresh take on low-level build system API. I’m incredibly grateful to Nima Johari for taking the time to answer my many questions about it, and to Cameron Zwarich for some very useful discussions about the incrementalisation of elaboration.

      It seems that there are two major approaches to demand-based build systems. The first, which is better known, is incremental computation based on dirtying of inputs which ripple outward in the form of cache invalidations. To my knowledge, this style is represented in Adapton, Shake, Rock, Incremental, and Salsa. Incremental computation in this sense is built up from a network of pure functions operating on stateful inputs at the edges.

      A second approach, which is being explored by Apple’s build team, is completely stateless; rather than input nodes being subject to update and inducing cache invalidation, inputs are instead ingested into content-addressed storage (CAS). The entire input to a build process (the source tree and the configuration) is then referred to (via a content-address) in the query nodes. The CAS-based approach, therefore, is not really involving cache invalidation: instead the data of a query contains a stable reference to CAS that can be narrowed to smaller fragments of the CAS in subsequent queries. When input state changes, it is ingested into the CAS and new queries are made that refer to the new data; naturally, child queries will narrow their reference to CAS and this will result in cache hits when the scope has narrowed to something that has already been computed.

      There are trade-offs between the two approaches. The first (which I will call stateful incremental computation) is easier to use, because dependency on stateful edge nodes is dynamic and determined in the process of query evaluation automatically. In contrast, the stateless CAS approach requires you to think very carefully about how to narrow the CAS keys referenced in queries. On the other hand, the stateless approach is more flexible in terms of the execution models it supports, which includes distributed builds. (I have a feeling distributed builds are going to be very important for large mathematical libraries in the future, or maybe even in the present if you look at the resources needed to build Mathlib.)

      Apple uses (or aims to use) llbuild2fx to coordinate internal builds of their software and its complex dependencies, and I believe they also plan for this (or something like it) to eventually be used in Xcode and the Swift compiler. I am, however, apparently the first person to be attempting to use llbuild2fx on the interior of a compiler, which is of course a potential risk. But a fun risk that I expect to learn a lot from either way.

      Sending strict propositions to the Ripley cupboard [01IK]

      Please note: I am no longer confident in the conclusions of this post, and I believe that I have made some mistakes. When I have ironed out what is true and what is not true, I will write a follow-up and link to it from here.

      Conor Mc Bride likes to send hopeless ideas and design mistakes to their Ripley Cupboard, a reference to a scene in the highly underrated film Alien: Resurrection in which all the hopeless attempts to reconstruct Ellen Ripley from DNA are stored in a gruesome menagerie. I am afraid that in spite of their successful semantic rehabilitation, strict / definitionally proof-irrelevant propositions must nonetheless find their permanent residence in my own Ripley cupboard for syntactical reasons.

      One thing that I had noticed a couple nights ago was that there might be a problem finding a suitable generalisation of Miller’s pattern fragment for dependent type theory with strict propositions. I was not really precise about what my concern was, but thankfully Matthieu Sozeau managed to pin it down.

      In essence, the problem has to do with what syntacticians call “strengthening”. The thing that makes higher-order pattern unification work well is the ability to tell whether or not some term actually depends on a given variable up to definitional equality; this is important because if you can eliminate a syntactic dependency, two things might happen that could allow the unification process to proceed further (1) a blocked unification problem may suddenly fall into the pattern fragment, and (2) a failing “occurs check” may start to succeed.

      With definitional singleton types, this is all fine: we can reliably eliminate dependency on singletons in a number of different ways, but these ways all rely on the fact that singleton types are inhabited. For definitional subsingletons, i.e. strict propositions, it is another story. Imagine that you have a strict proposition \(P\) and a subterm \(M(x,y,z):P\) of a larger proof-relevant unification problem; in order to find out whether or not the whole problem depends on \(x,y,z\) you need to know whether or not a “shorter” proof of \(P\) is derivable, which is obviously an undecidable problem.

      The upshot is, as Matthieu put it, we are not going to be able to find most general unifiers in any fragment of the language that involves strict propositions. Completeness of unification within a well-defined fragment is, in my opinion, the mathematical shadow of a more important but intangible property of unification being reliable and predictable. Therefore, I think that this observation may imply that reliable and predictable unification is not compatible with having strict propositions in any form.

      The implication for Project Pterodactyl is that we will not be pursuing strict propositions in any form, including my recent proposal.

      (It would be very welcome if someone noticed a way to get around this apparent obstruction, but I am not optimistic. It seems pretty airtight to me at the moment.)

      Shall we strictify some homotopy propositions? [01I6]

      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]

      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]

      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]

      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]

      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]

      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. 

      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]

      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

      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.

      Fuss-free universe hierarchies [01HX]

      The thing about universe hierarchies is that they are both painful to implement properly, and punting on them leads to even more pain later on because introducing a hierarchy is an extremely disruptive change for both the system and its libraries. After going through this treadmill a few times, I’ve learned my lesson: universes are something we need to get right from day one. Let me clarify that it is a non-goal to have inferred universe levels; I instead want to make working with universe levels as simple as possible, and to minimise the number of places where they need to appear.

      The first thing people ask is whether we will use universes “à la Russell” or “à la Tarski”. This is a question laden with false ideology, because the only kind of universes that exist in an objective (i.e. generalised algebraic) sense are the latter. But there is a valid question lying under the surface, which is whether or not users will be expected to explicitly write the decodings and universe level coercions. To that, I answer that we have the elaboration technology today to reliably avoid these bureaucratic details cluttering the source language.

      So you want a coherent universe hierarchy… [01HY]

      Someone who wishes to deploy modern elaboration technology to achieve an implicit source language, however, must think very carefully about the algebraic formulation of the core language to ensure that it has enough equations to maintain predictable behaviour under the implicit Russell-style notation. For example, if the level coercions are not coherent enough, it is easy to create unacceptable error messages that appear to the user like “Could not unify A -> B with A -> B.” Unfortunately, strong enough core languages are very laborious to specify and implement; for example, you will need the following (or some variation):

      1. You need top-level type constructors for all type theoretic connectives.
      2. For each universe level i, a type U[i] : Type and a dependent type el[i] : U[i] -> Type and codes closing U[i] under all type theoretic connectives, including codes for U[j] with j<i. The el[i] operation needs to commute strictly with the type constructor codes.
      3. For universe levels i <= j, you need a lifting operation lift[i<=j]: U[i] -> U[j] that commutes with all type constructor codes and is, moreover, definitionally functorial in the level preorder.
      4. You need el to commute with lift. (Thanks to Meven Lennon-Bertrand for catching this!)
      5. You need both lift[i<=j] and el[i] to be definitionally injective.

      There could be ways to refactor the above; for example, you could get rid of the top level of types altogether and just have universes. This is sometimes referred to as “universes à la Coquand”. Although admirable for its parsimony, I no longer like this approach because I agree with Per Martin-Löf that types and their elements are different concepts. And, for engineering purposes, although it seems at first easiest to have only universes, I think there are subtle ways in which that choice can make other aspects of the implementation more complicated. I think the importance of a separate top-level notion of type is argued for very well in the recent paper of Bezem, Coquand, Dybjer and Escardó.

      Anyway, this is a lot to implement in the kernel of a proof assistant.

      A new idea: Working your way down from the top [01I0]

      About a year ago, I started to get the inkling of an idea that we should not program with respect to a universe at all if we don’t need it. Instead, we should do large things by default (just like in everyday mathematics) and then when we have a need to talk about small things, we should just specialise them as-needed. For example, let’s consider the generalised algebraic theory of a category as phrased in univalent foundations:

      1. We have a \(1\)-type of objects C.
      2. For every two x,y:C we have a \(0\)-type of arrows C(x,y).
      3. And a bunch of operations and axioms involving the above.

      There is nothing about this definition that requires any particular constraints on the size of C and of C(x,y). In fact, the proper definition would not require that C(x,y) have the same size as C(u,v)! From the point of view of (generalised) algebra, these are just sorts. In fact, you never need to constrain the size of these things until you wish to start talking about things like the (bi)category of categories, etc.

      In contrast, if you require all types mentioned in a theory to have a given size, you immediately create a lot of complexity. First of all, you will be automatically assuming that the category is locally small for some universe—by requiring that C(x,y) be V-small for all x,y; there can be times when this is an unnatural assumption. But maybe the bigger problem is that when you want to start developing the theory of functors and natural transformations and so on, you will end up having at a half-dozen universe levels annotating every definition. Implicit universe polymorphism is not a solution to this problem: implicitly resolving the levels does not remove the complexity, and any experienced mechaniser will know that you inevitably need to debug a universe constraint graph.

      Some dream code [01I1]

      What I would like is the best of both worlds: to be allowed to develop the theory with fully unconstrained sizes, and then specialise the theory to more specific sizes later. Consider the following dream code for the theory of categories:

      theory Category where
  ob: Type
  hom: ob -> ob -> Type
  // operations and axioms...

      There is no implicit polymorphism happening in this definition. It is literally a very large theory of large categories. We can develop the theory of functors and natural transformations at this level too:

      theory Functor where
  C: Category
  D: Category
  ob: C.ob -> D.ob
  hom: (x y: C.ob) -> C.hom x y -> D.hom (ob x) (ob y)
  // axioms...

theory NaturalTransformation where
  C: Category
  D: Category
  F: Functor / {C => C, D => D}
  G: Functor / {C => C, D => D}

  go: (x: C.ob) -> D.hom (F.ob x) (G.ob x)
  // naturality axiom...

      If we want to talk about small or locally small strict categories, this is going to be very easy, and we can reuse everything from the theory of functors and natural transformations by instantiation.

      theory LocallySmallCategory where
  V: Universe
  ob: Type
  hom: ob -> ob -> V

  inherit Category / {ob => ob, hom => hom}

theory SmallCategory where
  U: Universe
  ob: U
  inherit LocallySmallCategory / {V => U, ob => ob}

      The above registers implicit coercions SmallCategory >-> LocallySmallCategory >-> Category. So if we want to talk about functors between X: SmallCategory and Y: LocallySmallCategory, we can do so by specialisation with no fuss:

      Functor / {C => X, D => Y}

      We will also be able to define the large category of small categories, again with no fuss.

      theory SmallStrictCategory where
  inherit SmallCategory

  code: U
  code/is-set: is-set code

  encode: code -> ob
  encode/surjective: is-surjective encode

theory CategoryOfSmallStrictCategories where
  U: Universe

  scat: Category
  scat.ob => SmallStrictCategory / {U => U}
  scat.hom X Y => Functor / {C => X, D => Y}
  // ...

      The theoretical foundation [01I2]

      I am now going to describe a way to set up a coherent universe hierarchy so as to ensure a parsimonious interpretation. I would like to emphasise that the dream code above can be elaborated to a traditional coherent universe hierarchy with enough equations, and that my reformulation here is only aiming to make this easier.

      In essence the main idea is to think about the image of the universe decoding maps el[i]: U[i] -> Type. In the generalised algebraic theory, we have required that these encoding maps be injective; an easily overlooked consequence of the injectivity is that the image of the decoding map is a derivable sort in the generalised/essentially algebraic doctrine.

      From this observation, we might instead consider a reformulation where instead of axiomatising the type codes and decoding maps and lifting coercions at each level and all the equations they must satisfy, we might instead axiomatise the images of the decoding maps in Type. This corresponds syntactically to defining a smallness judgement on types, which has a particularly extrinsic feeling to it. In fact, we would define this judgment using a judgemental partial ordering of universe levels; one example rule is the following:

      \[ \frac {\Gamma \vdash i+1 \leq j}{\Gamma \vdash U_i\ \mathit {small}_{j}} \]

      (The real generalised algebraic theory would have a sort of smallness-proofs, but this sort is axiomatised as a proposition. The fact that coherence/proof-irrelevance is baked into the theory fully justifies a notation in which the proofs are omitted.)

      Now, we recover the codes and the level coercions in one fell swoop by means of the following simple rules:

      \[ \frac { \Gamma \vdash A\ \mathit {small}_i }{ \Gamma \vdash \lceil A\rceil _i : U_i } \quad \frac {\Gamma \vdash A:U_i}{ \Gamma \vdash \lfloor A\rfloor _i\ \mathit {type} } \quad \frac {\Gamma \vdash A:U_i}{\Gamma \vdash \lfloor A \rfloor _i\ \mathit {small}_i} \] \[ \frac { \Gamma \vdash A\ \mathit {type} \quad \Gamma \vdash A\ \mathit {small}_i }{ \Gamma \vdash \big \lfloor \lceil A \rceil _i \big \rfloor _i \equiv A\ \mathit {type} } \quad \frac { \Gamma \vdash \lfloor A\rfloor _i \equiv \lfloor B\rfloor _i\ \mathit {type} }{ \Gamma \vdash A \equiv B : U_i } \]

      Now, supposing that the smallness and level inequality judgements have been filled out sufficiently, we can derive codes for connectives at the lower levels from the corresponding top-level type connectives. For example, consider the dependent function space:

      \[ \frac { \displaystyle \frac { \Gamma \vdash A: U_i }{\Gamma \vdash \lfloor A \rfloor _i\ \mathit {type}} \quad \frac { \Gamma ,x:\lfloor A\rfloor _i \vdash B[x]: U_i }{\Gamma , x: \lfloor A\rfloor _i\vdash \lfloor B[x] \rfloor _i\ \mathit {type}} \quad \frac { (\cdots ) }{ \Gamma \vdash (x:\lfloor A\rfloor _i)\to \lfloor B[x]\rfloor _i \ \mathit {small}_i } }{ \Gamma \vdash \big \lceil (x:\lfloor A\rfloor _i)\to \lfloor B[x]\rfloor _i \big \rceil _i : U_i } \]

      Of course, the notation is a little noisy, but these operations are precisely the sorts of things that are easy for a bidirectional elaborator to insert (and then hide from the user). It works equally well for Agda-style hierarchies with joins:

      \[ \frac { \displaystyle \frac { \Gamma \vdash A: U_i }{\Gamma \vdash \lfloor A \rfloor _i\ \mathit {type}} \quad \frac { \Gamma ,x:\lfloor A\rfloor _i \vdash B[x]: U_j }{\Gamma , x: \lfloor A\rfloor _i\vdash \lfloor B[x] \rfloor _j\ \mathit {type}} \quad \frac { (\cdots ) }{ \Gamma \vdash (x:\lfloor A\rfloor _i)\to \lfloor B[x]\rfloor _j\ \mathit {small}_{i \sqcup j} } }{ \Gamma \vdash \big \lceil (x:\lfloor A\rfloor _i)\to \lfloor B[x]\rfloor _j \big \rceil _{i \sqcup j} : U_{i \sqcup j} } \]

      The beauty of this simple approach is that we cut by two-thirds the number of universe-related operations we must implement in the core language. In that sense, we have an equivalent reformulation of coherent universe hierarchies that is more friendly on the engineering side.

      What about universe polymorphism? [01HZ]

      There are a few directions that one might go for introducing universe polymorphism. I will outline a couple options, both of which can be built on top of the above.

      Explicit polymorphism with a sort or type of levels [01I5]

      In Agda, the levels themselves form a type; this simplifies some things, and makes other things more complicated; on the other hand, Bezem, Coquand, Dybjer, and Escardó have proposed a stratified system in which levels can be abstracted but are not organised into an actual type. The main comment I would like to make here is that the formulation of universe heirarchies that I have described above will work regardless of whether levels form a type. The main syntactical challenge is to implement the smallness and inequality judgements, but is easily done in the style of Allais, McBride, and Boutillier as recently reformulated by Corbyn et al.. Put in terms of the latter, the type of universe levels is the free semilattice with successor on the presheaf of neutral terms of level type; and it is easy to decide equality in free semilattices with successor.

      A semantic challenge for Agda-style levels is that the semilattice laws are very strict, and so an interpretation into a higher-topos model might be a problem; for example, we cannot rely on the natural numbers being strict in every model of HoTT, which means that the semilattice laws might not hold definitionally. But we can stratify things in such a way that the type of levels is not small for any universe; then the universe levels could be interpreted as the “exo-naturals” in the extensional outer-layer of two-level type theory, which is conservative over HoTT.

      McBride’s Crude but Effective Stratification [01I4]

      In 2012, Conor Mc Bride proposed what they called Crude but Effective Stratification. Their idea is to define everything at the lowest possible level where it can live, but then subject the entire type theory to a functoriality in displacement operations, which allows developments to be shunted upward in the hierarchy as-needed. One way to think about the simplest version of Crude but Effective Stratification is that every top-level definition is polymorphic in a secret universe level variable, which can be restricted along edges in the universe level preorder. For more advanced functionality, you instead think of the top-level definitions as being polymorphic in a displacement.

      Conor’s idea is very flexible. As Favonia, Angiuli, and Mullanix pointed out, you could also have a universe hierarchy indexed in integers, and then shunt the developments both upward and downward. This one is justified in syntactical way—a semantic model of the system would not have have negative universe levels, but would instead pass through the observation that a given piece of syntax can only use finitely many universe levels.

      Either way, the benefit of McBride’s universe displacements is that when you have an arrangement of universes that need to be in some linear relationship to each other, you can just pick the tightest possible instantiation (e.g. U, U+, U++), and then later use a displacement to create extra room between the universes.

      Anyway, I think this is a good idea for handling universe polymorphism, but that question is a orthogonal to the design of the hierarchy itself. If we want, we can implement Crude but Effective Stratification on top of our foundation. I don’t plan to do this on day one, because I first want to see what the usability limitations are before introducing general displacements.

      In Project Pterodactyl, I will start with a preference for the explicit polymorphism to keep things simple. I am open to revisiting this in the future. By the way, I have already implemented everything I have described in this post in my secret Pterodactyl kernel (minus the elaboration itself).

      Lifting coercions to theory refinements [01HN]

      Last time, I spoke about plans for handling multiple inheritance and implicit coercions in Pterodactyl’s theory preorder. Today it is time to talk about bundling and refinement, and the rules for constructing and coercing implementations of refined theories.

      Refining bundled theories [01HO]

      When you have a theory, like that of semigroups, you define it in a fully unbiased/bundled way:

      theory Semigroup where
  car: Set
  join: car -> car -> car
  join/assoc: (x y z : car) -> join (join x y) z = join x (join y z)

      Then we might define monoids in terms of semigroups:

      theory Monoid where
  inherit Semigroup

  unit: car
  join/unit/left: (x : car) -> join unit x = x
  join/unit/right: (x : car) -> join x unit = x

      Suppose we want to describe the assumptions to the Eckmann–Hilton argument, where you have a pair of monoids sharing the same carrier set and satisfying a distributive law. For that, we need a way to refine a theory by a partial instantiation of its fields. Here is how it might look:

      theory EckmannHilton where
  X: Set
  M, N: Monoid / {car => X}
  dist: (u v w x: X) -> M.join (N.join u v) (N.join w x) = N.mul (M.mul u w) (M.mul v x)

      Things like this are dealt with in the world of Rocq’s Mathematical Components by using a “mixin” pattern: for every structure you predict in advance what unbundlings you are going to need, and then define a bundled version by taking a sum over these. This works very well, though it is a bit cumbersome and inflexible. I would like to build this feature directly into the language, and do it in such a way that you don’t need to predict unbundlings in advance.

      Introduction rules for refined theories [01HP]

      “Semantically”, a theory expression denotes a telescope in Martin-Löf type theory, and the type corresponding to a given theory expression should be the corresponding dependent record type / \(\Sigma \)-type; a refined theory corresponds to a smaller telescope. But theories are also names onto which various operations can be attached, so we can’t just elaborate them directly to the record type, as we will lose information that we need to keep ahold of.

      My thinking is that any theory expression T should induce a telescope <<T>> that consists of the remaining fields. So Monoid / {car => Nat} would correspond to the following telescope <<Monoid / {car => Nat}>>:

      join: Nat -> Nat -> Nat)
join/assoc: (x y z : Nat) -> join (join x y) z = join x (join y z)
unit: Nat
join/unit/left: (x: Nat) -> join unit x = x
join/unit/right: (x: Nat) -> join x unit = x

      Then every theory expression \(T\) comes equipped with a constructor form 

      make: <<T>> -> T

      which allows the user to fill in whatever residual fields are not refined in \(T\).

      Lifting canonical coercions to theory refinements [01HQ]

      The theory coercion preorder is only tip of the iceberg in terms of how coercions must get dealt with. These coercions need to be extended coherently across the negative fragment of the type theory itself.

      For example, if we have a synthesis form X:Monoid / {car => Nat}, we must be able to elaborate X:Semigroup / {car => Nat} seamlessly. There are a few ways that we might imagine this working. The simplest is to apply the constructor for Semigroup / {car => Nat} and then in each case apply the corresponding destructor of Monoid. I am not in love with this option because it leads very eager \(\eta \)-expansion during coercion, which can cause term size to blow up.

      I think there could be another implementation strategy which is more systematic. Let us consider a refinement scenario where we have refined a theory T by a partial instantiation R.

      Now, suppose we have two refined theories T0/R0 and T1/R1. There are many possible functions T0/R0 -> T1/R1 but I wish to argue that only some of these functions are canonical. In particular, a canonical function T0/R0 -> T1/R1 is one that arises in the following way from a canonical coercion T0 -> T1:

      To make it more intuitive, we can instantiate the scenario above with something concrete:

      (Thanks to Owen Lynch for pointing out some mistakes in the prior version of the diagrams above!)

      The definition of canonical map between refined theories gives, immediately, an algorithm for lifting coercions to refinements. The algorithm involves checking that the squares commutes up to definitional equality. In the implementation, we would not literally define the induced canonical map, but instead we would give it as a syntactic constructor and associate to the correct computation rules. This is transparent from the point of view of the type theory, but it avoids unnecessary \(\eta \)-expansions that would cause term sizes to blow up.

      Lifting canonical coercions to other type constructors [01HR]

      We will lift coercions to \(\Pi / \Sigma \) types in the standard way. What we will not ever try to do is lift coercions through any type constructors that lack \(\eta \)-laws, such as parameterised inductive types. This is not only because handling coercions for parameterised inductive types is syntactically difficult (but see the heroic work of some of my colleagues). Lost in the question of whether we can figure out how to deal with the syntactic difficulties of pushing coercions through positive types is the more troubling question of whether this can be made semantically compatible with the interpretation of inductive types in higher categorical models of type theory, where the “obvious” interpretations of inductive types involve some kind of fibrant replacement.

      Avoiding dependent coercions via “selfification” [01HS]

      Many treatments of coercions do not handle well the problem of when the type of the coercion seems to depend on the value being coerced. Luo and Soloviev attempted to address this problem by introducing a notion of “dependent coercion”; Lean also has a notion of dependent coercion. Luo and Soloviev’s version seems to have some issues, where the most expressive rules that one would want cannot be included without breaking transitivity elimination; Lean’s version explicitly does not support chaining of dependent coercions, and I wonder if this is the reason why.

      I am contending today that many useful cases of dependent coercions don’t actually need to be dependent. My idea is based off an old trick known only to the ML Modules Crew called “selfification”, which my PhD advisor Bob Harper kindly taught me several years ago. The idea of “selfification” is to transform a dependent coercion problem into a non-dependent one.

      Suppose that we have a bidirectional elaborator, and we are now at the mode-shift. We have received some typed term M:T where T is a theory expression and we are trying to check it at type B. Rather than searching for a canonical coercion from T -> B, we instead first construct the maximal refinement “T/M” of T to a definitional singleton type that contains only M; this means refining all the fields of T to project the corresponding ones from \(M\). Then we try to find the canonical coercion from T/M to B.

      (I think we can also generalise the algorithm to work even when the synthesised type is not a theory expression, but I won’t talk about that today. In case I forget, the idea is treat the mode shift as always being between theory types, which can be done by having a built-in theory for typed terms.)

      I want to show an example. Consider the case of trying to define the following dependent function:

      cool (X : Monoid): Semigroup / {car => X.car}
cool X => X

      The idea here is that (1) if X is a monoid, then it’s a semigroup by forgetting the extra stuff; and (2) forgetting this extra stuff leaves the carrier set fixed. Can we justify returning X as above via elaboration?

      Yes. The elaboration state at that point is asking us to convert X : Monoid to Semigroup / {car => X.car}. Obviously we cannot hope to find a coercion Monoid -> Semigroup / {car => X.car}, but what we do instead is attempt to find a coercion from

      Monoid / {car => X.car, join => X.join, unit => X.unit, join/assoc => X.join/assoc, join/unit/left => X.join/unit/left, join/unit/right => X.join/unit/right}

      to Semigroup / {car => X.car}. And that is something we can evidently do, using our notion of canonical coercion between refined theories!

      In summary, we have very strong dependent-type-friendly coercions, without needing the coercions themselves to be dependent functions.

      Labelled preorders and implicit coercions [01HB]

      Project Pterodactyl aims to support coherent algebraic hierarchies with multiple inheritance as well as user-defined edges. As I mentioned in my HoTTEST talk, there are a few points worth mentioning here in regard to the so-called “diamond problem”.

      What is the diamond problem? [01HD]

      The first thing to get out of the way is that the phrase “diamond problem” means different things to different people. There are actually two different diamond problems that arise when building systems that support implicit coercion; these two problems are actually mutually exclusive, in the sense that you can have only one version of the diamond problem at once.

      1. There is the coherence problem, which concerns ensuring that diamonds (and loops) in the coercion graph commute. A system in which all diamonds and loops commute is called coherent. In a coherent system, backtracking is never required and so the resolution of coercions can be extremely efficient. This is the “diamond problem” for Theory B computer scientists.
      2. In an incoherent system, resolution of coercions must traverse all possible paths from the source to the target, and the presence of diamonds and loops in the graph can cause an exponential blowup for the naïve backtracking algorithm. This is the “diamond problem” for Theory A computer scientists.

      Indeed, if your system is coherent then no backtracking is required; but you must find a way to maintain the coherence invariant. On the other hand, if you have an intentionally incoherent system, then you do have to deal with the exponential blowup, but you don’t have to check coherence because you don‘t care about coherence. This is the sense in which the two problems are mutually exclusive.

      Approaches to the diamond problem(s) in existing systems [01HE]

      Here I outline some (but not all) existing approaches to dealing with implicit coercions, multiple inheritance, and the various diamond problems.

      Coherent type classes in Haskell [01HF]

      Haskell employs a syntactic condition to ensure that type classes instances do not overlap, leading to a global coherence property. Practice in the Haskell community has shown that it is possible (but painful) to develop coherent hierarchies. Many advanced libraries will activate a language extension to allow overlapping instances, which renders the hierarchy incoherent.

      Fast but incoherent type classes in Lean [01HG]

      Type class hierarchies arising in mathematics tend to be unavoidably incoherent; therefore, systems like Lean implement a backtracking type class resolver and are therefore confronted with the second diamond problem above. The Lean team have discovered an algorithm that they call Tabled Typeclass Resolution that mitigates the exponential blow-up using ideas from logic programming.

      The state of affairs for Lean is, then, that type class resolution is pretty fast but the actual resolution of coercions is in theory non-deterministic; in reality, it does the same thing every time (so far as I know), but there is no guarantee about which coercions it is choosing.

      Coherent locale hierarchies in Isabelle [01HH]

      Locales provide a coherent way to organise mathematical hierarchies. The problems that lead type class hierarchies to become incoherent do not seem to apply to locale hierarchies, I think, because the resolution of the locale’s operations is name-based rather than component-based. (I am not completely certain that this is the full story, but it seems like it is part of the story.)

      One way to think about locales and the reason they can remain coherent is by analogy with Haskell’s newtype trick, which Haskell programmers use liberally to maintain coherence, but taken to its logical conclusion. Instead of generating a fresh copy of a type in order to indicate its intended role in the type class hierarchy, Isabelle doesn’t hang identity on the type at all and instead just starts with the name that carries intentional force.

      The coherence of the locale hierarchy in Isabelle is checked when activating a locale as a local theory. Here, an algorithm called “roundup” reaches through the entire locale inheritance graph and brings all the needful operations into scope, and if there is a clash (two names pointing to different things), this results in an error. Such a clash always corresponds to a failure of coherence, and conversely, failures of coherence will always lead to such clashes.

      Coherent coercions in Rocq [01HI]

      Rocq has a coercion mechanism, which checks coherence and warns users when they are installing incoherent coercions. Coercions are most used in the world of Mathematical Components in combination with the canonical structures feature, which simulates type-class like features using something like unification hints (to my knowledge).

      The algorithm used in Rocq was created by Kazuhiko Sakaguchi and described in the PhD thesis Refinement and extension of mathematical structures in proof assistants based on dependent type theory. The idea here is to maintain the reflexive-transitive closure (path category) of the coercion graph at all times; when inserting a new coercion, you check a generating class of diamonds for coherence and then add all the induced paths. Coherence then ensures that the path category is a preorder, with a functorial embedding into the syntactic category of the language under consideration.

      Evaluating: Isabelle‘s roundup algorithm vs. Rocq’s coercion graph [01HJ]

      I am ruling out incoherent hierarchies from the outset, because these lead to unpredicatable resolution. The two viable approaches seem therefore to be the one of Isabelle and the one of Rocq; I believe that the latter will work best for our needs, even if our goal is to enable an Isabelle-style user experience.

      The thing with Isabelle’s “roundup” algorithm is that it seems to rely heavily on the idea that the instances of a locale in scopes are fully top-level, so that you can walk through them and eagerly install all their operations into the appropriate scope. In this sense, Isabelle’s implementation of locales does not involve implicit coercion at all. In a dependent type theoretic setting, we must account for things like families of structures and ensuring that we can project components from these as well. For example, if we have a constant \(M \colon I \to \mathsf {Monoid}\), we will need to be able to call things like \((M~i).\mathsf {join}\) which would involve passing through the coercion to semigroups, etc. I am not sure how to capture something like that via a roundup-like algorithm.

      For this reason, I believe that the best foundation for Pterodactyl’s handling of algebraic hierarchies will be Sakaguchi’s labelled preorders as deployed in Rocq.

      A clean-room implementation of Sakaguchi’s labelled preorders [01HK]

      In order to learn how the algorithm works, I built a clean-room generic implementation in Swift of the labelled preorder structure following Sakaguchi’s algorithm. (Oh, did I mention I’m using Swift?)

      Our case will be a bit simpler than that of Rocq. In Rocq, coercions can be between arbitrary things, and therefore the vertices must include definitional equivalence classes of terms. That seems very tricky! We will be using a more restricted kind of coercion in Pterodactyl, where the vertices are only theory names. (We might later on also support coercions to sorts like those of types and functions, like Rocq does, which would not be difficult.)

      As a result, the only thing that we need to use expensive definitional equality checks for is the coercion paths themselves. It will indeed be pretty costly to install coercions, but resolving them will be very cheap: it is a single lookup in a hashtable by a totally discrete key. My code is available here.

      I am not certain that we will use literally this code (abstracting and modularising too early can be hazardous), but it’s a good start.

      A focused vision for Project Pterodactyl [01H3]

      After a few very enlightening conversations following my HoTTEST seminar talk “Is it time for a new proof assistant?”, I have realised that one of the more important aspects of my plans for Pterodactyl is its focused and restricted vision. I cannot promise that we will succeed, but I do think that by not trying to be all things to all people, we may be able to avoid some likely ways of biting the dust.

      We are not building a general-purpose programming language [01H4]

      Any implementation of dependent type theory is a programming language of sorts, following the Curry–Howard correspondence, but I have come to believe that to build an actually good programming language (like OCaml, Lean, Rust, or Idris) is a very different task from building an actually good proof assistant (like Rocq, Lean, or Isabelle).

      If you have enough resources, you can do both at the same time (like Lean). If you don’t have enough resources, I think you end up with something that is going to be inadequate as either a general-purpose programming language or as a proof assistant.

      I do think that this is a point we could revisit in the future, but only after we have achieved our primary goals. Not having general-purpose programming as a primary goal doesn’t mean we can’t write programs in the language; I think that, instead, punting on things like “Being competitive with OCaml and Rust” means that there will be more space for ambitious dependent-type-native people to explore the possibilities of dependently typed programming without having to answer questions for which we don’t yet have good enough answers.

      We have no plans to self-host, ever [01H5]

      When you build a language you really like, it is natural to want to rewrite its compiler in itself. This is a reasonable impulse, but I believe that it can also create inertia and painful coupling as you have to negotiate changes to the language with changes to the compiler in both directions rather than in only one direction.

      Here’s the thing: if we were to write a highly-performance-constrained system (like a proof assistant) in itself, the proof assistant’s compiler and execution model would need to immediately be competitive with state-of-the-art programming languages with vastly more resources and expertise behind them. I do think that we can build something that is competitive with Agda, but I do not think we could build something that is competitive with both Agda and Rust or OCaml at the same time.

      I believe that it is a good goal to have a system that can do both. But I think that in order to get there in a resource-constrained environment, it is very important that the goals be achievable separately. If we have to achieve both in order to achieve one, we will realistically achieve none.

      We do not have plans for general-purpose metaprogramming [01H6]

      One of the most interesting things about Idris 1, Agda, and Lean is their approach to metaprogramming. In either system, you can hook directly into their elaboration monad and write metaprograms directly in the language, and then designate certain of these metaprograms as tactics or macros.

      I think that this is an excellent model, but one of the reasons I am planning to shy away from it is that I believe it introduces a great deal of coupling between user-land code and the implementation details of the system (including its representation of syntax, its approach to elaboration and the suspension of elaboration problems, its approach to unification, etc.).

      This is similar to the self-hosting problem; with enough resources, you can pat your head and rub your belly at the same time, but I believe that avoiding the coupling that metaprogramming introduces for the longest time possible will increase our probability of achieving our primary goals.

      We do have plans for procedural reasoning [01H7]

      Some community members have expressed skepticism about what might be lost in reducing everything to a problem-oriented programming model like that of “The View From the Left”. For example, a large part of typical tactic scripts in Rocq amounts to procedurally generalising goals and calling eliminators, and this is indeed well-handled by the McBride—McKinna model; on the other hand, there are many other useful pieces of tactical reasoning like apply f or eapply f that aren’t discussed in that paper. If we built a system in which you could not easily backchain through a lemma, it would indeed be a pretty unrewarding system to use.

      The particular case of backchaining through lemmas can, however, be addressed within a very small extension of the McBride–McKinna model. For this, we will need what might be referred to as the “view from the right”. There is an analogy to be had here:

      • McBride and McKinna defined a general notion of “elimination operator”, and devised a pattern matching notation for it.
      • We seem to need to define a general notion of “introduction operator”, and then devise a co-pattern matching notation for it.

      In Epigram, we can think of the ability to return a value (written \(\Rightarrow \mathit {val}\)) as the beginning of a “view from the right”, which is just lacking any kind of right-handed decomposition. Our goal is to add this decomposition.

      Consider the case of showing that a particular sum \(\sum _{x:\mathbf {1}}x=()\) is a proposition, using a lemma about the closure of propositions under internal sums. Here is our initial proof state as it might appear in our editor:

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example}~\color {gray}[?\colon \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=()] \end {aligned} \]

      Next, we use the backchaining introduction operator, which generalises the usual “return” / \(\Rightarrow \) co-gadget of Epigram to allow for subgoals.

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}~\color {gray}[?\colon \mathsf {isProp}~\mathbf {1}] \\ &\mathsf {example}.\mathsf {famIsProp}~\color {gray}[?\colon (x:\mathbf {1}) \to \mathsf {isProp}~(x=\mathbf {1})] \end {aligned} \]

      Note that with records, we can easily arrange for the subgoals of to have more human-readable names than \(\pi _1,\pi _2\), as we’ve done above. The first goal is easy to solve using another lemma; that lemma has no subgoals, so that branch is finished off like so:

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~\color {gray}[?\colon (x:\mathbf {1}) \to \mathsf {isProp}~(x=\mathbf {1})] \end {aligned} \]

      In the second branch, we can abstract the variable.

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~x~\color {gray}[?\colon \mathsf {isProp}~(x=\mathbf {1})] \end {aligned} \]

      Next, we backchain through yet another lemma, namely that propositions are sets.

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~x~\Rightarrow \mathsf {propsAreSets}\\ &\mathsf {example}.\mathsf {famIsProp}~x~\color {gray}[?\colon \mathsf {isProp}~\mathbf {1}] \end {aligned} \]

      Finally, we finish up the problem with a lemma that has no subgoals.

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {propsAreSets}\\ &\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {unitIsProp} \end {aligned} \]

      Personally, I find the above to strike a good balance between readability and writeability while maintaining the very important procedural aspect of how mathematicians write proofs; it is an extremely small generalisation of the McBride–McKinna model.

      We can workshop the notation and improve it, but I think the underlying idea here is viable. For those who think “But that is exactly what we already had with tactics”, that is actually my entire point: I don’t want to get rid of procedural tactical reasoning, but I do want to find a way to incorporate it into a problem-oriented notation that mostly documents itself in connection with editor facilities to see the proof state at a given step.

      I won’t say that this solves all problems, but I hope it gives some impression of the methodology by which we will tackle procedural reasoning.

      Stepping through proofs is important [01H8]

      It is important to be able to see what the goal was at a given point in a proof that has already been completed. If we return to our example of right-handed procedural reasoning:

      \[ \begin {aligned} &\mathsf {example} : \mathsf {isProp}~\textstyle \sum _{x:\mathbf {1}}x=() \\ &\mathsf {example} \Rightarrow \mathsf {sumIsProp} \\ &\mathsf {example}.\mathsf {baseIsProp}\Rightarrow \mathsf {unitIsProp} \\ &\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {propsAreSets}\\ &\mathsf {example}.\mathsf {famIsProp}~x\Rightarrow \mathsf {unitIsProp} \end {aligned} \]

      We could instrument the language server to emit either tooltips or expandable inlays on each \(\Rightarrow \) or \(\Leftarrow \) that will display the goal that is being refined. For example, I plan to make it so that if you select the second \(\Rightarrow \) in the above, the editor would display something like \[ \mathsf {isProp}~\mathbf {1} \] and if you select the third \(\Rightarrow \), the editor would display something like \[ x:\mathbf {1}\vdash \mathsf {isProp}~(x=())\text {.} \]

      Ideally, selecting the occurrences of the backchained lemmas on the right-hand side would lead to a display that reveals exactly how they have been specialised for the goal. For example, if you select the occurrence of \(\mathsf {propsAreSets}\) the editor might display something like the following:

      \[ x:\mathbf {1}, \square :\mathsf {isProp}~\mathbf {1}\vdash \mathsf {propsAreSets}~\mathbf {1}~\square ~x~() : \mathsf {isProp}~(x=()) \]

      Thoughts on XSLT in the “web platform” [01DI]

      Mason Freed, a Chromium/Blink developer employed by Google, opened a ticket a couple weeks ago on the WHATWG/html repository: Shall we remove XSLT from the web platform? Typical of the simultaneously high-handed and ignorant approach of the browser vendor cartels that have come to dominate the Web, Freed is proposing that client-side XSLT support be removed from the “web platform” (which is cartel code for “whatever We decide”). Like most attacks on the Open Web, this one is backed by concerns about “security”—as if the only way forward was to keep using libxslt without paying its developers.

      Mason’s laughably ignorant proposal of a polyfill is completely unworkable, as such a polyfill would increase payloads by an order of magnitude—and it wouldn’t even work for most use-cases where the goal is to serve an XML document that is automatically rendered, rather than to serve an HTML document that embeds the result of transforming an XML document at load-time. It’s a non-starter. Why do people who know nothing have authority over people who know something? I guess it’s the way of the world.

      Now, I understand that XSLT in the browser is not as commonly used as it was in the past. Moreover, real industrial users of XSLT are not using XSLT 1.0 but rather later more fully-featured versions like 3.0 via tools like Saxon, etc. But one very common use of client-side XSLT is to render RSS/atom feeds (for blogs and podcasts—yes, people still do those!) in a user-friendly way when viewed in the browser; of course Forester uses client-side XSLT as well. Since the writing has been on the wall for a while, I have been planning to change Forester to not depend on client-side XSLT, but I would prefer not to be forced into this by the browser cartels.

      Many of the people whose comments have not been censored in the GitHub thread seem to be entirely unaware of the fact that RSS even exists. My guess is these viciously ignorant people think that podcasts are things that you subscribe to on Spotify, or watch on YouTube.

      Anyway, I was thinking. I wonder if the health and security of the Open Web would be greatly benefited if Mason Freed and his colleagues in the other major browser vendors did not have the ability to change the Web without consent of its actual constituents—the people who publish websites. Using a tiny fraction of these vendors’ resources, we could fund the amazing team building xrust (a modern implementation of XPath 3.1, XQuery 3.1, and XSLT 3.0 in Rust), or any one of several other teams working to implement modern XML tooling in open source. I’d love to restore the “web platform” to its rightful owners—the PEOPLE. I don‘t know if Ladybird is the solution, but I’m glad to see some competition in this space from outside the cartel.

      To Mason: I’m sure you’re a fine guy in real life. There is a sense in which you are only a vessel for these proposals, which would be made by someone else if you weren’t involved. But I think there are plenty of people for whom there would be no salary big enough to get them to let the cartel’s words flow through their lips so uncritically. I think those are the kind of people we need in stewardship over the Web.

      See also this post by David Bushell.

      NewsRadar: a work-in-progress newsreader for the Macintosh [01C9]

      During my Summer holiday, I began working on a new newsreader for the Macintosh which I have tentatively named NewsRadar. I am a mostly happy user of the great NetNewsWire by Brent Simmons, but I have an idea for a few unique features that would greatly improve my own newsreading workflow. I also believe strongly in the capability of syndication (in the form of RSS, Atom, JSON Feed, etc.) as a much simpler and cheaper alternative to federation as a means to reclaim the World Wide Web. Obviously, this is a fully native app that complies with Macintosh user interface conventions.

      Organising feeds with labels instead of folders [01CE]

      Most newsreaders organise their feeds into folders: that means that one feed appears in at most one folder. I have found that it is sometimes unnatural for me to decide upon one categorisation of my feeds. For example, I subscribe to many people’s weeknotes feeds; ideally all these would be in one folder. On the other hand, I also subscribe to various blogs from people and groups locally in Cambridge and at times I would like to view just the Cambridge Feeds. The problem is that some of these are weeknotes: so I must decide whether to put (e.g.) a student’s weeknotes in the Weeknotes folder or in the Cambridge folder.

      To solve this problem, I am switching to a style of organising feed subscriptions based on labels or tags (like Gmail does for individual emails). A label is like a folder except that a given feed can have multiple labels without duplicating the subscription.

      Deduplicating articles that appear in many feeds [01CJ]

      An overlooked reality of syndication is that a given article may appear in several feeds. For example, some of my book reviews get posted both to my main blog and to The Jon Sterling Review of Books, and it is conceivable that someone might subscribe to them both. My model allows the same article to have multiple “sources”; of course, it is possible that the content may differ, and I will eventually come up with a way to flag this to the user. One thing to keep in mind, however, is that it is not necessary to account for all possible contingencies in an environment like newsreading where there is no adversary.

      Smart collections for news triage [01CF]

      Sometimes you want to constrain your view to something more (or less) specific than a single label. For example, you might want to look at the union of two labels, or constrain by publication date, etc. For this, I am introducing Smart Collections, which are essentially named queries; these are similar to Smart Folders in the Macintosh Finder, but my notion of predicate is more sophisticated (unions and intersections can be nested arbitrarily).

      In the future: posting to your own feed! [01CH]

      Louie Mantia had a great idea for an RSS reader-writer app; this would be an app that lets you post to an RSS feed just as easily as you subscribe to others. I actually believe this would entirely replace the functionality of social media that I benefit from, and conveniently it would be poorly adapted to replace the parts of social media that I don’t benefit from. Here’s what Louie says:

      As Twitter crumbles and people scatter into federated social media, I remembered we already had a method to self-publish posts, large or small: RSS. I think a big reason it hasn’t caught on for most people is that there’s not a good method to open an app, compose a post, and send it. I think it could exist, and maybe it would look like this.

      I think this is the right direction. I think it will take a bit of thought and design work to do this right, but I believe it’s worthwhile. It is worth noting that the blog authoring app MarsEdit was originally part of NetNewsWire. It is high time to consider a modern take on the unification of reading and writing, building on what came before as well as newer ideas drawn from modern social media like Dave Winer’s Textcasting concept.

      Let’s get back to syndication! [01CG]

      Federated social media like Mastodon presents a number of downsides and even dangers to users and operators:

      1. When you run a social media site, you are subject to the Law—not only of your own country, but even other that of foreign countries. Maybe you are small enough that nobody notices, but at some point, there is going to be a regulator knocking on your door telling you that CSAM or other illegal material has been posted on your website and you should not be surprised to find out that you are responsible for that. At times you will also be obligated to censor your users who post from the point of view of proscribed organisations, and it is worth considering whether this may in the future entail a legal obligation to censor those who are speaking out to prevent a new Holocaust, etc.
      2. Moderation at the “instance” level comes into contradiction with the federation model, because (1) different users have different legitimate preferences, (2) the prevalence of culture war engagement among instance owners leads inexorably towards mass defederation, and the “normies” are constantly getting robbed of their social graphs as a result whilst having no idea what controversy they inadvertently stepped into. To be very clear, I support people having spaces with moderation policies that protect them from harm; but I believe that making these decisions at the granularity of instances rather than individual people does not stabilise over time.
      3. Each person running their own federated Mastodon instance seems to be too expensive (putting aside the need for system administration, etc.). When you start to federate with high-volume instances, you can get totally blown up.

      As Louie points out, we don’t need content moderation at all with ordinary syndication via RSS, Atom, etc. The big reason content moderation is needed on present-day social media platforms is, aside from legal requirements for platform operators, the insistence on unrestricted replies and the “discoverability brainworm” (Louie’s coinage) that has made the Web into a place that serves influencers, hucksters, and narcissists to the detriment of artists and intellectuals. The way to escape from this is to stop trying to be platform operators; the Web is the platform.

      I understand that many people want to use the Web to make money or become famous; but I am equally within my rights to wish to use the Web to communicate ideas, create and consume educational materials, and socialise with my friends and family. It is a good thing rather than a bad thing to create tools that explicitly do not support the kind of fame-seeking behaviour that has turned the Web into a hellscape of scams, advertising, shilling, gambling, and exploitation. I do not judge the way any person chooses makes a living, but I know what I do and do not want in my life.

      In light of recent efforts by content platforms to blacklist and “de-host” creators of media deemed unsavoury by the large financial institutions, I believe that syndication via RSS/Atom/etc. is a comparatively safe direction for individual sovereignty in our use of the Web, and it luckily costs almost nothing to host a feed (and you can get a free Wordpress.com or $1/month Micro.blog account and just not worry about it if that’s your speed). What is needed, however, is software to make it easier for ordinary people to “jack in” to the World Wide Web in a way that sticks.

      Stay tuned for more! [01CI]

      The software is in a very early prototype stage right now, and I am considering the design in light of Apple’s recent changes; it is really a challenge to develop a usable app whilst hewing to Apple’s haphazard design language, but I believe there is also an opportunity here to go above and beyond and return to the great era of polish in applications for the Macintosh.

      I am also considering funding models. One option is to sell the app in the traditional way; I am resistant to subscriptions because I would never personally subscribe to an app like this. I understand that the economics of the one-time purchase don’t work well anymore, but I am not looking to make a living from this; the subscription model rarely provides enough value for users, who end up feeling exploited—indeed, software today in the subscription era costs far more than software did in the 2000s even taking into account yearly upgrade prices. The blown up costs of good software today is one of the reasons why there is, I believe, so little diversity in the software market compared to the old days when you could spend $40 on an app and use it forever until you choose to upgrade.

      I would also be open to a donation model, but I have to consider the matter carefully.

      Feel free to write to me if you are interested in trying out an early version when that is ready (it won‘t be soon).

      The Greatest Predator Ever Known! [01C8]

      Frank Herbert’s God Emperor of Dune is the most delightfully unhinged novel I have ever read. I cannot deny that I have loved all three of the preceding Dune novels, perhaps even more so than God Emperor. But just as Leto II intentionally reduced the mystique of Paul-Muad’Dib to parody in order to deliver Humankind from a horrifying future, I suppose Herbert’s ruthless approach to our memory of wind-swept Arrakis may have been a requirement to make room for the larger-than-life whimsy of God Emperor.

      The first four Dune novels by Frank Herbert: Dune, Dune Messiah, Children of Dune, God Emperor of Dune

      I have always thought that we should write what we know deeply. The problem with Dune and its copious epigrapha—often straight from the blessed lips of Muad’Dib—is the combination of absolute seriousness and near-total lack of signal in his wordy pronouncements. Was Muad’Dib a bullshitter, or was Herbert the bullshitter? I think Herbert aimed to portray Paul-Muad’Dib as a great (but fatally flawed) thinker of another world and time, but the danger of writing speculatively about things you do not know deeply (philosophy, history, the State, and the Spirit) is that successive generations may find the result less credible than did the Mid-Century Man, whose more limited access to the breadth of human culture tended to generate “profound” insights that are quickly hackneyed.

      God Emperor turns all this on its head—Leto II’s wordiness and tendancy to unclear (meaningless?) pronouncement is legendary (and a thorn in the side of his retainers and his enemies alike), but that is one of the privileges accorded to a God. Leto II is the greatest bullshitter to ever live, and he knows it! The Golden Path, that tenuous thread in the tapestry of time by which Mankind may narrowly avoid total extermination by prescient machine minds, demands nothing less than Leto’s unintelligible tyranny. Who are we to question a God, and who can be Shai-Hulud besides the only living sandworm?

      Thoughts on Apple’s new design language [01BX]

      As many predicted, Apple unveiled at its Worldwide Developer Conference a new design language for all its platforms centred around a material that they call Liquid Glass. I have some personal reflections about my time as an iOS platform app developer during the iOS 7 transition, and some thoughts about what the new design language may mean for the remaining independent developers whose businesses have not been destroyed by the App Store’s race to the bottom.

      A screenshot of the Music app with the new Liquid Glass design. Source: Apple.

      (I will not speak much here about the merits (or lack thereof) of the new design language. There is a lot to say and critique there, but there’s also some reason for hope.)

      Flat design was about de-skilling app development [01BZ]

      If you believe that the purpose of a system is what it does, the purpose of the iOS 7 redesign was to de-skill app development. Admittedly this sounds like a conspiracy theory that ignores Apple designers’ stated motivations, but my experience is that whenever there is a business case for something, that thing will simply happen and those involved in the transition tend to explain it to themselves in ways that flatter their sensibilities—a macrocosm of the epiphenominalist hypothesis for the world of business.

      The economic context of the transition, returning to the early 2010s, is that Apple’s native platforms were losing ground to (objectively terrible for users) cross-platform alternatives in large part because of the exorbitantly high cost of designing platform-native apps to the standard set in the visually and materially rich design language of iOS 6 and below. Think about that terrible “web view inside an app” thing that your phone provider makes you use in which scrolling is broken and back-buttons are dangerous to press, and which constantly logs you out in the middle of a task, or stalls on a 10-factor authentication labyrinth, or charges your credit card twice due to a lag in responding to a confirmation button press, and you will know exactly what I mean.

      App development in the iOS 6 era

      I was a native mobile app developer in both eras, and I’ll tell you that a serious iOS 6 app would involve hundreds of designer-hours producing meticulous custom graphics for most controls—designed to be thematically harmonious with the system appearance, but customised to delight and surprise: think wooden navigation bars with inset text that looks like it was carved with a router. After this artwork was produced (naturally at 1x and 2x resolution, as we were still in the throes of the Retina transition!), the engineers take ahold of it and begin overriding the -drawRect: methods of many views, which was often non-trivial due to the need to change the behaviour of views managed deep within system classes.

      A screenshot of Runenstein, a rune catalogue that I designed and built many years ago.
      A screenshot of Yardsale, the pre-iOS 7 iPhone app that I worked on with Ed McManus, Ryan Mickle, and Michael Sanders in the early 2010s. Source: Wired

      App development post iOS 7

      By way of contrast, designing an app post iOS 7 is considerably less expensive: there are essentially no custom graphics at all, and the only thing the designers are doing is choosing colours and fonts to “highlight the brand”. If there are custom controls, they can be drawn without an expensive designer’s intervention, as in nearly all cases, these are just ugly buttons with slightly non-standard shapes that someone with no skills at all easily can draw in Quartz—or SwiftUI. Certainly there is no engineer sweating over pixels and perfecting the custom animations that support the delightful illusion of material.

      A screenshot of FOBO, a live auction app that I built together with the Yardsale team during the iOS 7 transition. Suddenly one’s brand could be reduced to a colour. Source: Laughing Squid

      What did “centering the content” achieve?

      I have no doubt that behind Jony Ive’s prattling about “centering the content”, which Alan Dye has taken to new extremes more recently, was an actual business case that Apple considered to be of existential importance: if the cost of native application development is not lowered dramatically, native application development will (for all intents and purposes) cease. It is not lost on me that Apple’s de-skilling strategy had the exact opposite of the likely intended effect: there has never been as many non-native apps on Apple platforms as there are today, and I believe there are two reasons for this.

      1. With the advent of Apple Silicon, performance is no longer a strong differentiator for native apps. Many Electron apps (including Visual Studio Code) perform better than native alternatives.
      2. In the era of flat design, in which intricate and materially rich design has been “cancelled”, visual beauty and detail are no longer strong market differentiators for native apps, nor is respect for platform-specific functionality (like proxy icons on the Macintosh!) that is increasingly de-emphasised in Apple’s native toolkits.

      Liquid Glass is a gift to the indies [01BY]

      I was listening to Accidental Tech Podcast’s discussion of the new design language and one thing that struck me was Marco Arment’s prescient comment that essentially no corporate apps besides Apple’s will adopt it. There are three reasons for this:

      1. Large corporations have gotten used to treating Apple’s decade-long lack of design as a blank slate on which to paint their “brand”. Suppressing the “brand” to unify with the system appearance is a complete non-starter in the corporate world. If you suggest something like that, you will be laughed out of the room.
      2. Most smaller corporate apps were designed and built by consultants rather than in-house, and no small company will be able to justify dropping an additional $200K+ on an app refresh.
      3. Most corporate apps are using some unwieldy cross-platform toolkit like React or Flutter anyway (enough said).

      I think the Liquid Glass design presents an opportunity for independent app developers to differentiate themselves from the competition in ways that have not been possible since before iOS 7. The return of texture and depth and active light and subtle animation means that those who treat app development as craft will be able to create vastly different experiences from those created by consultants or even corporate in-house teams whose business motives do not include platform integration or, indeed, delight. (Not all is rosy: the changes to icon dimensions and composition represent a new de-skilling manoeuvre by Apple—but for users, it is hard to say that this is worse than the present dystopia of soulless glyphs.)

      These prospects for craft seem not to depend on whether the Liquid Glass design is actually good and accessible for users—it is just complex enough that (good or not) it will lead to the kind of differentiation that we had on both iOS and the Mac OS X platforms in the old days—when an app that was either non-native or poorly crafted (usually both) stood out like a sore thumb in ways that regular users could notice just by touching a control and seeing what happens when you move things around, or finding they can select text that should not selectable, or scrolling to reveal incorrect insets and content boundaries, etc. Attempts to replicate the Liquid Glass material using web technologies will likely lead to stuttering scrolling and drained batteries, which (again) regular users will be able to notice.

      So, whilst I’m shaken by the potential for a further degraded user interface on the Macintosh, I’m more optimistic than I thought I would be about the prospects for independent Apple platform application development in the next ten years. I’m also not certain what this means for AquaUI—I need to experiment with Liquid Glass to better understand its strengths and weaknesses before returning to that project.

      We have AI at home… [01AS]

      On Tuesday, I travelled by train to Sheffield to take part in the Yorkshire and Midlands Category Theory Seminar #37 meeting, where I would be speaking about my paper that compares partial map classifiers with Sierpiński cones in synthetic (domain/category) theory, which I summarised previously.

      A pleasant surprise [01AT]

      I was preparing for my chalk talk when I realised that I could not remember the details of the proof of the main result and they couldn’t really be reconstructed from the abbreviated proof in the paper.

      Luckily, I had actually formalised this result in Agda! I did not mention my formalisation in the paper because I do not think of formalisations as scientific contributions except in certain cases (that is a conversation for another day). But I did indeed formalise it because the proof was subtle enough that I needed computerised assistance back when I proved it the first time. The result I obtained was frustratingly weak, and seemed to require some annoying side conditions in order to go through; the formalisation helped me be certain that these side conditions were in fact sufficient.

      Anyway, I was messing around with the code and what I realised was that I had missed a trick back then: one of the side conditions was actually unnecessary, and it seems kind of likely that the other one is unnecessary too. I am certain I would not have noticed this if I hadn't had the proof assistant, which made it easy for me to try something out and see if it worked. I should have time to update the paper to claim the strong result prior to the LICS camera-ready deadline next month.

      Arise, symbolic AI! [01AU]

      There is a lot of discussion lately of the impact that some current machine learning techniques, marketed as “Artificial Intelligence”, can have on formalisation of mathematics in proof assistants. Some of the most esteemed members of the mathematical community have gone all in on this trend (is it a requirement of scientific fame and esteem that you begin to cause trouble in areas of research that you know nothing about?), but I think that evaluating LLMs on Olympiad questions is really missing the point of what computers can do to assist mathematicians. Olympiads are a good fit for LLMs, because kids who participate in Olympiads are behaving much more like LLMs than human mathematicians—the mathematics Olympiad is the ultimate feat of pattern-recognition without understanding, and they are certainly a good fit for the Might Makes Right approach being taken within AI today.

      Agda (and Lean and Rocq and Isabelle) are “Artificial Intelligences” in the most progressive sense—they augment the limited context that a human can store in their mind at once, and are nimble tools for working mathematicians to check and verify their ideas, and (most importantly) they do not proceed by creating a fetish of illusion and misdirection that deceives the public. Their capabilities are limited, but well-circumscribed. I think often about how important it is to know in a definite sense what a tool can and cannot do, and I increasingly think that this is actually part of what makes something a tool. Some of my colleagues have compared LLMs to calculators, in order to make the case that we should get ready for them to be used as everyday tools; but LLMs are not simply tools in the sense that a calculator is a tool.

      Putting Mac OS X Tiger back to work [01AH]

      Over the Christmas holiday, I bought an iMac off eBay for £50. Why was it so cheap? Because it is a 2006 model firing on a single gigabyte of RAM with an Intel Core 2 Duo processor, running Mac OS X Tiger. When I was a kid, I dreamed of having a computer like this—for me, the white plastic era will always be peak Apple design, and Tiger’s version of Aqua was the most polished and refined form of the design language that they ever managed to produce. My first Macintosh was a white polycarbonate unibody MacBook running Leopard—and at the time I greatly regretted having just missed the Tiger era for the gaudy and overly darkened feel of Leopard with its sinister-coloured window controls. I did not know at the time how much worse things would get…

      My excuse for purchasing this machine was that I “needed” to run Mac OS X Tiger as “research” for my experimental project AquaUI, which imagines how the Aqua design language could have evolved if it had been allowed to. But really, I wanted to relive my rare trips to Apple retailers as a kid, where I would spend minutes doing nothing but just moving the scrollbar while watching its stationary “wave” texture, or highlighting buttons to see them burst with blue radiance.

      (I spoke about many of the topics covered in this post in my appearance on the Kodsnack podcast hosted by Fredrik Björeman: Episode 626, “The great flattening of everything”.)

      Day One: what can you do 19 year old iMac? [01AI]

      When the delivery came, I took the machine gingerly out of its battered and taped over original packaging and turned it on to a feeling of great excitement, which quickly gave way to loss and melancholy: so much of what computers are “for” involves the World Wide Web, and the forced transition to HTTPS/TLS has stolen access to the Web from users of many working computers of access to the Web (unless they gut the machine by downgrading to a modern but severely less polished operating system, like Linux). The old Intel Macs are a prime example of this loss—although some volunteer projects exist to enable safe access to the Web for PowerPC machines, older Intel Macintoshes have received comparatively less attention. Capitalist forced obsolescence comes to all, however, and there will no doubt come a time when the “necessary” “security” routines will simply not be executable with the kinds of hardware resources that could be mustered in 2006, no matter the system architecture. After playing around and finding much of the functionality crippled due to being barred from the Internet, I had to ask myself, What should I even do with this thing?

      The iMac lay dormant in my College room for the next few months while I figured out an answer to that question.

      My iMac sleeping peacefully in my office at Clare College Memorial Court, connected to a vintage A1048 keyboard and Apple Pro Mouse (as it should be!). Nearby is my iPod Classic, which I use for about an hour each day and charge once every 6-8 weeks.

      With a little love, everything has a use [01AJ]

      Last week I finally realised that there is a lot I can still do with this machine. I turned it on when I had a bit of free time, and found that it remains very snappy—software opens instantly without hanging, and in fact the built-in programs are significantly less bug-ridden than they were in subsequent versions of Mac OS X and its (unworthy) successor macOS. To put this into perspective, the “outdated” iMac’s performance was far better than that of my last Intel iMac from 2020 with sixteen times the RAM and several times the processor cores.

      It is well-known that hardware capabilities get better and better each year, but this did not translate into improved performance for users until after the Apple Silicon transition—when the hardware improvement was so great that it was able to outpace the deathmarch of inefficient software, for a time. Don’t worry, the “transition to AI” is going to destroy all those gains soon and we’ll be back where we started.

      Mac OS X Tiger is still King—with the peak versions of Finder, Preview, and iTunes.

      But I digress. Even if you can’t use the Web, there are many things that a 19 year old iMac running Mac OS X Tiger is better at than a more recently manufactured machine. For example, Tiger was the last version of Mac OS X in which Preview.app (the PDF and image viewer) had a working search interface; from the subsequent version (Leopard) all the way until the present day, searching is somehow both too fuzzy and not fuzzy enough, and there seems to be no combination of quotation marks that will lead to reasonable results appearing in the search pane. (Same with Mail.app, which has somehow got even worse in the past year; you can’t connect to email on such an old machine anyway, so the point is moot.)

      Similarly, iTunes 7 was the functional peak for Apple’s music management and playback software (although iTunes 6 was visually superior), and people who have only used Apple’s current “Music” app will not be able to understand what they are missing. Likewise, the version of Finder shipped with Tiger was the most polished and least buggy version they ever produced; it is really amazing to switch back and forth between macOS 15.3 and Mac OS X 10.4, and find that most of the bugs or usability problems I have encountered on a daily basis for the past decade or so are actually regressions.

      The perfect music and PDF reading workstation [01AK]

      So I transferred my music and PDF libraries to the iMac—this was easy to do by creating a local WiFi network from the iMac, a functionality that has been removed in macOS(!). Indeed, modern macOS has replaced some (but not all) aspects of this functionality with what is called “Internet Sharing”, but this feature does not work reliably and in many cases the needful functionalities are unpredictably grayed out and disabled without any message explaining why. Death by a thousand papercuts... But I digress: I set up a local WiFi network with a file server easily using the old System Preferences application (don’t get me started on the bizarre redesign of System Settings introduced in macOS Ventura), and easily transferred everything I wanted to the iMac and then I was off to the races.

      I listen to music and study papers on this machine, and it gives me so much joy to use this masterpiece of practical industrial design every day—I even write referee reports on it using an ancient version of OmniOutliner, a venerable piece of software that I have to say has not improved much in the past two decades. After installing a copy of Scrivener 2.5 (don’t worry, I own a license for Scrivener 3.0 and you should too!), I find myself creative writing in my free time like it’s 2006.

      What about my iPod Classic? [01AL]

      Some of you may be aware that I use an iPod Classic every day. The thing is a godsend—the best mobile device I own. I bought it with a fresh battery and SSD, and the damn battery lasts for months before I have to recharge it. That is the kind of technology that was taken from us and replaced by resource-intensive devices governed by the logic of planned obsolescence. But I have it back—my world is not the same as your world, but it is a world I am glad to have returned to.

      Naturally, the first thing I wanted to do was use the iMac as a hub for synchronising the iPod with iTunes. This will work, but what I did not anticipate is that one of my main uses of the iPod is to listen to podcasts, and podcasts cannot be downloaded on the iMac because of the vicious imposition of TLS on all parts of the web that didn’t need it (Let’s Encrypt really ought to have been called Let’s Kill The Open Web). So I continue synchronising my iPod with my modern day MacBook Air—and it is a testament to Apple’s historical approach to backward compatibility that this is still possible (and even integrated with the otherwise terrible Podcasts app!).

      Is retrocomputing sustainable? [01AM]

      I constantly feel a pang in the back of my throat when I think about retrocomputing over the long term. We are scrounging around for intact pieces of old technology, but there will come a time when these are too scarce, or when we have really lost the ability to repair them. It is like living in a post-apocalyptic film where a cataclysm has made all manufacturing impossible—but today the cataclysm is not a war or even a virus, but just the simple vicious logic of Capital and a technology industry that has hitched itself to the most ignorant and anti-human trends emanating from the most technologically ignorant people on Wall Street.

      Retrocomputing is decidedly not sustainable, in the same sense that living on a stash of canned foods that can no longer be manufactured cannot be sustainable. But also unsustainable is the present day technological treadmill of consumer goods containing precious metals and dangerous chemicals being produced in the billions and sent directly almost directly to the landfill.

      I think a better question to ask is whether retrocomputing is progressive. I think that retrocomputing can be progressive insofar as it is part of a practice of looking forward—how can we build sovereign technology that respects constrained resources as well as users of different abilities, and cannot be taken away or made useless by Capital and the irrational whims of the stock market. Such a project must have a significant design component, and this cannot be done amateurishly; looking to the iconic design languages of the past for inspiration and education is, then, deeply progressive in this environment.

      The tragedy of Mac OS X is not that Apple took it away and replaced it with something inferior: the tragedy is that free software communities have never managed to produce something even remotely approaching its level of fit and finish. Volunteer projects do not deserve my ire, which I reserve for our economic system in which nearly all competent design work is confined to corporate environments, and then wiped away when the wind shifts.

      Bring back the joy in computing! [01AN]

      Forget your troubles and find something that makes you smile, and reminds you of what is possible when a team brimming with talent comes together to build something beautiful.

      Write to me with any joyful and quirky projects, hardware or software, that you would like to share.

      Ventriloquy of the Mid-Century Man [019W]

      Moments before leaving for a meeting in Barbados with my colleagues Anil Madhavapeddy and Mark Elvers, I hastily loaded Arthur C. Clarke’s The Fountains of Paradise onto my Kindle for airplane reading. I really want to love “hard science fiction” — I spent months with Asimov’s Foundation in 2022 — but I must admit that I am struggling with the limitations of this genre.

      The cover of The Fountains of Paradise.

      In her 2013 interview with The Paris Review, Ursula Le Guin questioned the hard/soft divide in science fiction, pointing out that the distinction seems to be based on authors and readers of sci-fi arbitrarily deciding which of the sciences are “Science” and which aren’t.

      The “hard”–science fiction writers dismiss everything except, well, physics, astronomy, and maybe chemistry. Biology, sociology, anthropology—that’s not science to them, that’s soft stuff. They’re not that interested in what human beings do, really. But I am. I draw on the social sciences a great deal. I get a lot of ideas from them, particularly from anthropology. When I create another planet, another world, with a society on it, I try to hint at the complexity of the society I’m creating, instead of just referring to an empire or something like that.

      There is a good point here, and Le Guin’s attention to social sciences and anthropology and history was indeed a strength, but Asimov was also preoccupied with the same throughout Foundation. So what is the difference, aside from the fact that Foundation was written by a man? Well, it cannot be unrelated to Asimov being a man, but perhaps we will get to the point sooner by referring to a specific type of man — the Mid-Century Man.

      The Mid-Century Man has no time for the usual literary rules governing the development of characters and their arc of growth. He is interested in science and humanity, yes, but through the lens of his own avatar whom he transplants directly from our world of his time into the futuristic world of his story. This hapless transplant finds himself, with no volition, speaking the author’s words through his own lips… He hears his own voice prattle on about “the last refuge of the incompetent” and can do absolutely nothing about it.

      The inclination of the Mid-Century Man to spill no ink that might distract from his speculations (flavoured with thematic orientalism, as in the case of Fountains) is not limited to hard science fiction — Herbert falls prey to the same tendancy in Dune, which I adore, but he is saved by his mastery of the tragedy-form: indeed, we are already weeping with Paul over Chani’s fate a quarter of the way through Dune Messiah.

      In contrast, there is little that is compelling about the characters of The Fountains of Paradise, nor those of 2001: A Space Odyssey, and the same holds for Asimov’s Foundation. The mostly one-dimensional characters of these works are foils for the authors’ speculative ideas about technology or “future history”, and a shorter work could have been written that omits the ventriloquy act entirely and just directly makes the point the author so strongly wished to make.

      Will Fountains be the last “hard science fiction” book I read? Surely not… There is still much to enjoy and marvel over — and there is a true sense in which Clarke’s elevator to Heaven is compelling enough to outweigh even the worst of his flimsy characterisation.

      Winter in Eden and Return to Eden: an imperfect conclusion [019O]

      Two months ago I reviewed Harry Harrison’s delightful West of Eden, a piece of speculative fiction that considers a world in which the Cretaceous–Paleogene extinction event never occurred, and one species of dinosaur went on to evolve over the subsequent 66 million years into a highly sophisticated society stratified by uneven linguistic abilities. The most intelligent stratum of this species calls itself Yilanè, which is at once an ethnonym and a classification of linguistic ability.

      In Harrison’s Eden, reptiles of all kinds dominate Africa (Entoban in Yilanè) whereas mankind (Tanu and Sasku in their languages) and other mammals live in North America (Gendasi in Yilanè), confined at first mainly to its colder northern reaches. The icy winds of climate change blow across Entoban and northern Gendasi alike, which leads mankind to migrate south just as the Yilanè begin to colonise southern Gendasi. The encounter of Tanu and Yilanè is predictably violent—when the Tanu encounter the torpid Yilanè males basking on the birthing beaches of Alpèasak (the new Yilanè colony in our own Florida), they slay them immediately and spark a war of the species that shapes the entire trilogy.

      Covers of the Eden Trilogy.

      That is the premise of West of Eden, the first book of the Eden Trilogy, which tells the story of a young Tanu man named Kerrick who is kidnapped and raised by Yilanè in Alpèasak. The next two books, Winter in Eden and Return to Eden, concern the continuing struggle of Tanu and their Sasku allies to survive in the South while being pursued by a genocidal Yilanè expedition, and of the minority faction of Yilanè called the Daughters of Life who aim to establish a peaceful city in South America.

      Although Winter in Eden and Return to Eden share the charm of the first book, they do not quite live up to its promise. Without revealing anything that might spoil the Trilogy (which I do still recommend), there are several imperfections that give a reader the distinct impression of rushed writing—especially in Return.

      • Throughout Return to Eden the toponyms Gendasi and Entoban are frequently mixed up, leading to a great deal of confusion. For example, Vaintè says “But Entoban is large, most of it unknown to us, warm and filled with good meat” but this could only refer to Gendasi in the context of the novel. I am apparently not the only person to notice this oversight, as can be seen by perusing the Amazon reviews.
      • Relatedly, there is no explicit toponym for South America, which plays an important role in the story. Indeed, South America appears to be referred to as part of Gendasi, which makes sense considering the land bridge that joins it to North America, but in that case it is surprising that Gendasi is glossed as North America rather than The Americas.
      • Several interesting story-lines appear to be dropped on the floor. What of the scientist Ambalasei’s fate, and will the radical city Ambalasokei survive?

      Perhaps what was needed most was more time. Despite these imperfections, I don’t regret my time in Eden—and I dream of returning there one day.

      West of Eden: you can judge a book by its cover [015W]

      I have found that one could do far worse than perusing the r/CoolSciFiCovers subreddit and picking things to read at random. This week I chose West of Eden based on its outstanding cover art, and it turned out to be a very enjoyable read.

      The cover of West of Eden, by Harry Harrison and illustrated by Bill Sanderson.

      The premise is that the impact causing the mass extinction of non-avian dinosaurs never occurred, and neolithic Man unknowingly shares the Earth with a very advanced and highly stratified female-dominated race of intelligent lizards whose males have two penises (don’t ask me why! apparently this is common in nature). When climate change threatens both the human and lizard civilisations, they are forced to migrate and, in doing so, discover each other’s presence and clash violently.

      Some aspects of the story are a little old-fashioned—I barely need to discuss the instinctive disgust and “racial hatred” felt by the humans and the lizards for each other, but the narrative ultimately challenges this feeling by revealing each culture to be civilised in its own terms, if not in terms that would lead to a cooperative multi-species stewardship of the Earth.

      The initial inability of the intelligent lizards to fathom that the “filthy ustuzou”—the lizard phrase for humans and other mammalian creatures—may be sentient and even conscious entities of moral force is challenged by their experience, and by a religious extremist trend within their society that recognises the intrinsic value of all forms of conscious life. In a time where current science continues to reveal, bit by bit, the overconfident ignorance and moral wickedness of those who have insisted that the “lower forms of life” on our own Earth are without sentience, value, moral force (the octopus, the elephant, etc.), it is hard to read this without thinking about our own “filthy ustuzou” and the future consequences of our vicious behaviour toward them.

      We must fund intellectual infrastructure for the long term [013G]

      How can we effectively and sustainably fund the intellectual infrastructure for generational human advancement? Intellectual infrastructure—which I would define to encompass the tools used to develop, teach, and learn science—is mistreated by essentially all extant funding models that I am aware of.

      To be clear, when I speak of “tools” I mean not only software (like Lean, Coq/Rocq, Agda, Isabelle, Forester, SageMath, or Mathematica)—but also more broadly intellectual tools like the nLab and The Stacks project whose main aim is not necessarily to contribute new ideas but to consolidate what is known in order to lay the groundwork for the future.

      Funding intellectual infrastructure using research grants [013H]

      In a traditional research grant proposal, one describes a scientific vision instrumented by several key deliverables that can be achieved in anywhere from the space of a year to several years.

      There are three main problems with research grants as far as the funding of intellectual infrastructure.

      Problem. Inadequate timescale of research grants [013J]

      Research grants are usually time-limited (for example, five years tends to be on the longer side for grants), whereas the sustainable intellectual infrastructure that can actually be safely adopted in critical areas must be funded stably on the scale of decades rather than years.

      Problem. Unquantified impact of intellectual infrastructure [013K]

      Funding is, as a rule, devoted to projects that promise (1) significant and (2) essentially predictable intellectual contributions. Intellectual infrastructure typically does not yield a direct intellectual contribution, but when neglected for too long can impede these intellectual contributions in invisible ways. Funders of research grants are, however, reluctant to fund what they cannot quantify.

      Problem. “implicit” production of intellectual infrastructure [013L]

      Because intellectual infrastructure is nearly always developed by a combination of volunteer labour and student labour, funders are reluctant to devote resources to what they anticipate will be done anyway without their intervention—or, given that many PhD studentships are sponsored by such bodies, there may be a perception that the existing model is already adequately funding the production of intellectual infrastructure.

      Funding intellectual infrastructure on the FRO model [013I]

      An interesting and encouraging development is the emergence of the Focused Research Organisation model, which recognises and aims to solve Problem [013K] and Problem [013L]. For example, the most excellent Lean Focused Research Organization describes their mission as follows:

      We are excited to share the news of the Lean Focused Research Organization (FRO)! A new nonprofit dedicated to advancing the Formal Mathematics revolution, we aim to tackle the challenges of scalability, usability, and proof automation in the Lean proof assistant. Our 5-year mission is to empower Lean towards self-sustainability. Please check our current roadmap for details. (Lean FRO, Mission)

      I think that this is a great development indeed, and it will be good for Lean and therefore good for our community. But I think that the FRO model cannot address Problem [013J]—the inadequate timescale. Even the reference to “self-sustainability” in the Lean FRO mission statement suggests an assumption that there is anything “self-sustaining” whatsoever about the infrastructure that makes scientific and intellectual progress possible.

      It is one thing (a very good thing indeed) to solve usability problems and address pain points that prevent institutional and industrial adoption of intellectual tools in the near term. I have every reason to believe that the Lean FRO will be be very successful in this area (and they have made great strides already). An FRO naturally does not aim to solve all problems, and we should certainly not judge them on that unrealistic basis; but we should use the experience to better understand where the gaps are in our current models for the funding and production of intellectual infrastructure.

      Problems with the bimodal theory/practice cycle [013M]

      The bimodal “practice—then theory—then practice” model presupposed by the dichotomy between traditional research grants and focused research organisations and other short-term “moon-shots” neglects the dialectical interplay between theory and practice, in ways that can have real consequences for human intellectual advancement. Indeed, it seems to me that the model of dividing funding between traditional research grants and FROs is based on the idea that progress occurs in a two step cycle:

      1. First the “real science” reaches the point where it is strong enough that it could be applied in a practical way, but this application would be impossible to achieve within the research grant funding model.
      2. So an FRO is spun up to pick up where the science left off, and develop the application to the point that it can be practically adopted in institutions and industry.
      3. (Repeat!)

      I do not think that the cycle above can lead to sustainable intellectual infrastructure, which requires (1) a more responsive interplay between theory and practice, and (2) long-term continuity of lessons and advances that cannot be achieved on the current model of “once or twice per decade post-mortems” in the form of successive research grant and FRO proposals.

      Unsustainable tool enhancement is a barrier to progress [013N]

      I am going to say something strange, and I hope that I will not be misunderstood.

      By concentrating an immense amount of funding into “developing the application” without regard for the evolving theoretical basis and sustaining the development over a timescale of decades, we can unintentionally and disastrously raise the bar for high-impact advances by increasing product inertia in unsustainable ways. For example, I would estimate that it costs upwards of £1–2M to create an excellent IDE—so when a five year program results in an excellent IDE for a specific language along the understandably narrow mission of an FRO, the funders may have unintentionally raised the financial baseline for any future transformative impact by at least £1M.

      We do not need to make any guesses or conjectures as to whether increased inertia is a likely outcome of these new funding models—as this has already occurred, incontrovertibly, as a consequence of the existing industrial-adoption-based model of production of programming languages, where a large corporation can put millions of funding into a language of relatively low quality (and thus raise significantly the usability of the tooling) to the point that making a competently designed language meet the minimum standard for adoption would cost far more than is possible to fund on the academic model.

      Obviously the solution to this problem is not to slow the march of tool enhancement—quite the opposite. But we must find a way to achieve these enhancements without making future improvements of a more radical nature prohibitively expensive. I think that the key to unlocking the long-term sustainability of intellectual tool enhancement to develop a unified and responsive theory/practice funding model that can exercise leadership on the scale of decades.

      A call to action for a sustainable theory/practice spiral [013O]

      I am calling for the endowment and funding of independent research institutions on a permanent or decades-long basis, whose mission is not bound to a specific tool (e.g. Lean or Coq or Forester) but rather to a set of scientific principles and society-level goals to be achieved on a generational timescale.

      It may seem as though open-ended endowments of this kind are a pipedream, but I would draw your attention to the example of the Hoskinson Center for Formal Mathematics at Carnegie Mellon University established in 2021 by a gift from billionaire Charles Hoskinson; although the Center is mainly focused on Lean, I see no reason why institutions of this nature could not be endowed on a permanent basis with a broader technical approach.

      For future endowments, it will be important to place an emphasis on the funding of permanent staff over the funding of research students and postdocs—whose near-term career needs are often in deep and irreconcilable conflict with the mission of an institution that aims to make generational social impact. If you have resources that could be brought to bear on such an ambitious project, or are connected with someone who does, please get in touch with me (js2878@cl.cam.ac.uk). It is time for us to build and sustain the scaffolding for the next three centuries of Science.

      Acknowledgments [013P]

      My sincere thanks to Johan Commelin for his comments and encouragement.

      Tips for using plain text email on macOS [00QB]

      I am a proponent of using plain text (or Markdown-formatted) emails rather than HTML-formatted emails. Although there are some legitimate uses for rich formatting in email, I find the well is poisoned: HTML-formatted email manipulates, surveils, and controls.

      A renaissance for plain text email?

      Although plain text email has gone the way of the dinosaur in most parts of society, it remains used among many technical communities (such as the Linux kernel developers, etc.). Recently, SourceHut has emerged as a free and open source code forge whose workflow is entirely based on plain text email as described on the useplaintext.email website. Naturally, this has led to both curiosity and friction as users attempt to adapt to working technology of the 1990s that Capital has made increasingly difficult to interact with using present-day software. As a maintainer of several projects on SourceHut, I have seen many of my valued collaborators completely fall on the ground when it comes to following the etiquette recommendations for plaintext emails (especially text wrapping) and this is certainly not for lack of trying on their part. The available technological options are just that difficult to use.

      The main viable tools for working with plain text email are terminal-based: for example, aerc and mutt and its derivatives. These are, however, a non-starter for most users (even technical users): for example, they are difficult to configure, and integrating with address books from standard email providers is nearly impossible or requires a Nobel prize; a bigger problem is that for most of these tools, one must store passwords in plain text (or use some very complicated authentication scheme that a typical user will be unable to set up).

      The only viable modern GUI client recommended by useplaintext.email for macOS is MailMate. Unfortunately, MailMate’s visible settings do not have any option for wrapping text, which would contradict its viability for plaintext email users. Furthermore, the versions of MailMate available for download from its website (both the released version and the prerelease) seem to be incompatible with macOS Sonoma. By doing a bit of spelunking, I have found that both these problems can be solved (at least for now).

      Using MailMate for plain text email [00QD]

      Step. Download the prerelease of MailMate

      First, download the latest prerelease binary for MailMate from this directory: http://updates.mailmate-app.com/archives/?C=M;O=D. I found that the this program can take a very long time to open for the first time, but after this it is speedy.

      Step. Enable format=flowed

      Second, enable format=flowed using the following completely undocumented command:

      defaults write com.freron.MailMate MmFormatFlowedEnabled -bool true

      Note that this option is so undocumented that it does not even appear in the list of hidden preferences. There is some discussion of this on the mailing list.

      Although the format=flowed standard standard is very rarely implemented by clients, email sent using this flag will be formatted correctly by SourceHut Lists.

      Day tensors of fibered categories [009F]

      I have been thinking about monoidal closed structures induced by slicing over a monoid, which has been considered by Combette and Munch-Maccagnoni as a potential denotational semantics of destructors à la C++. It occurred to me that this construction is, in fact, almost a degenerate case of Day convolution on an internal monoidal category — and this made me realize that there might be a nice way to understand Day convolution in the language of fibered categories. In fact, many of these results (in particular the relativization to internal monoidal categories) are probably a special case of Theorem 11.22 of Shulman’s paper on enriched indexed categories.

      Definition. The “Day tensor” of fibered categories [009A]

      Let \(E\) and \(F\) be two fibered categories over a semimonoidal category \({\mathopen {}\left (B,\otimes ,\alpha \right )\mathclose {}}\). We may define the “Day tensor” product \(E\otimes _B F\) of \(E\) and \(F\) to be the following fibered category over \(B\):

      \[ E\otimes _BF :\equiv \otimes _!{\mathopen {}\left (\pi _1^*E\times _{B\times B} \pi _2^*F\right )\mathclose {}} \]

      Note that \(f_!\) refers to the left adjoint of base change \(f^*\) for fibered categories, which is not postcomposition.

      Exegesis. Stepping through the Day tensor of fibered categories [009C]

      To understand the construction of the Day tensor, we will go through it step-by-step. Let \(E\) and \(F\) be two fibered categories over a semimonoidal category \({\mathopen {}\left (B,\otimes ,\alpha \right )\mathclose {}}\).

      1. Given that \(E\) and \(F\) are displayed over \(B\), we may restrict them to lie the two disjoint regions of \(B\times B\) by base change along the two projections:
        The above can be seen as cartesian lift in the 2-bifibration of fibered categories over \(\mathbf {Cat}\).
      2. Next, we took the fiber product of fibered categories, giving a vertical span over \(B\): \[ \pi _1^*E \leftarrow \pi _1^*E\times _{B\times B} \pi _2^*F \rightarrow \pi _2^*F \] Of course, this corresponds to pullback in \(\mathbf {Cat}\) or cartesian product in \({\mathbf {Cat}}_{/B}\).
      3. Finally, we take a cocartesian lift along the tensor functor \({B\times B}\xrightarrow {{\otimes }}{B}\) to obtain the Day tensor:
        Note: the cocartesian lift above does not correspond to composition in \(\mathbf {Cat}\) except in the discrete case.

      Under appropriate assumptions, we may also compute a “Day hom” by adjointness.

      Definition. The “Day hom” of fibered categories [009G]

      Let \(E\) and \(F\) be two fibered categories over a semimonoidal category \({\mathopen {}\left (B,\otimes ,\alpha \right )\mathclose {}}\). We may define the “Day hom” \(E\multimap _B F\) of \(E\) and \(F\) to be the following fibered category over \(B\):

      \[ E\multimap _BF :\equiv {\mathopen {}\left (\pi _1\right )\mathclose {}}_*{\mathopen {}\left ( \pi _2^*E\Rightarrow _{B\times B} \otimes ^*F \right )\mathclose {}} \]

      Proof. 

      First of all, we note that the pullback functor \({{\mathbf {Cat}}_{/B}}\xrightarrow {{\pi _1^*}}{{\mathbf {Cat}}_{/B\times B}}\) has a right adjoint \(\pi _1^*\dashv {\mathopen {}\left (\pi _1\right )\mathclose {}}_*\), as \({B\times B}\xrightarrow {{\pi _1}}{B}\) is (as any cartesian fibration) a Conduché functor, i.e. an exponentiable arrow in \(\mathbf {Cat}\). We have already assumed that \(E\) is a Cartesian fibration, and thus so is its restriction \(\pi _1^*E\); it therefore follows that \(\pi _1^*E\) is exponentiable. With that out of the way, we may compute the hom by adjoint calisthenics:

      \[ \begin {aligned} &\mathbf {hom}_{{\mathbf {Cat}}_{/B}}{\mathopen {}\left (X\otimes _B E,F\right )\mathclose {}} \\ &\quad \equiv \mathbf {hom}_{{\mathbf {Cat}}_{/B}}{\mathopen {}\left ( \otimes _!{\mathopen {}\left ( \pi _1^*X\times _{B\times B}\pi _2^*E \right )\mathclose {}} ,F\right )\mathclose {}} \\ &\quad \simeq \mathbf {hom}_{ {\mathbf {Cat}}_{/B\times B} }{\mathopen {}\left (\pi _1^*X\times _{B\times B}\pi _2^*E,\otimes ^*F\right )\mathclose {}} \\ &\quad \simeq \mathbf {hom}_{{\mathbf {Cat}}_{/B\times B}}{\mathopen {}\left ( \pi _1^*X ,\pi _2^*E\Rightarrow \otimes ^*F\right )\mathclose {}} \\ &\quad \simeq \mathbf {hom}_{{\mathbf {Cat}}_{/B}}{\mathopen {}\left (X, {\mathopen {}\left (\pi _1\right )\mathclose {}}_*{\mathopen {}\left ( \pi _2^*E\Rightarrow \otimes ^*F \right )\mathclose {}} \right )\mathclose {}} \end {aligned} \]

      Definition. The “Day unit” of fibered categories [009B]

      Let \({\mathopen {}\left (B,\otimes ,I,\alpha ,\lambda ,\rho \right )\mathclose {}}\) be a monoidal category. We may define a “Day unit” for fibered categories over \(B\) to be given by the discrete fibration \({B}_{/I}\to B\), which corresponds under the Grothendieck construction to the presheaf represented by \(I\).

      Conjecture. The Day tensor preserves cartesian fibrations [009D]

      If \(E\) and \(F\) are cartesian fibrations over a semimonoidal category \({\mathopen {}\left (B,\otimes ,\alpha \right )\mathclose {}}\), then the Day tensor \(E\otimes _BF\) is also a cartesian fibration.

      I believe, but did not check carefully, that when \(E\) and \(F\) are discrete fibrations over a semimonoidal category \({\mathopen {}\left (B,\otimes ,\alpha \right )\mathclose {}}\) then the Day tensor is precisely the discrete fibration corresponding to the (contravariant) Day convolution of the presheaves corresponding to \(E\) and \(F\). Likewise when \({\mathopen {}\left (B,\otimes ,I,\alpha ,\lambda ,\rho \right )\mathclose {}}\) is monoidal, it appears that the Day unit corresponds precisely to the traditional one.

      There remain some interesting directions to explore. First of all, the claims above would obviously lead to a new construction of the Day convolution monoidal structure on the 1-category of discrete fibrations on \(B\) that coincides with the traditional one up to the Grothendieck construction. But in general, we should expect to exhibit both \({\mathbf {Cat}}_{/B}\) and \(\mathbf {Fib}_{B}\) as monoidal bicategories, a result that I have not seen before.

      Conjecture. A monoidal bicategory of fibered categories [009E]

      • September 20, 2023

      Let \({\mathopen {}\left (B,\otimes ,I,\alpha ,\lambda ,\rho \right )\mathclose {}}\) be a fibered category. Then the Day tensor and unit extend to a monoidal structure on the bicategory of fibered categories over \(B\).

      Conjecture [009E] is highly non-trivial, as monoidal bicategories are extremely difficult to construct explicitly. I am hoping that Mike Shulman’s ideas involving monoidal double categories could potentially help.

      On the relationship between QTT and STC [0094]

      I have been thinking again about the relationship between quantitative type theory and synthetic Tait computability and other approaches to type refinements. One of the defining characteristics of QTT that I thought distinguished it from STC was the treatment of types: in QTT, types only depend on the “computational” / unrefined aspect of their context, whereas types in STC are allowed to depend on everything. In the past, I mistakenly believed that this was due to the realizability-style interpretation of QTT, in contrast with STC’s gluing interpretation. It is now clear to me that (1) QTT is actually glued (in the sense of q-realizability, no pun intended), and (2) the nonstandard interpretation of types in QTT corresponds to adding an additional axiom to STC, namely the tininess of the generic proposition.

      It has been suggested to me by Neel Krishnaswami that this property of QTT may not be desirable in all cases (sometimes you want the types to depend on quantitative information), and that for this reason, graded type theories might be a better way forward in some applications. My results today show that STC is, in essence, what you get when you relax the QTT’s assumption that types do not depend on quantitative information. This suggests that we should explore the idea of multiplicities within the context of STC — as any monoidal product on the subuniverse spanned by closed-modal types induces quite directly a form of variable multiplicity in STC, I expect this direction to be fruitful.

      My thoughts on the precise relationship between the QTT models and Artin gluing will be elucidated at a different time. Today, I will restrict myself to sketching an interpretation of a QTT-style language in STC assuming the generic proposition is internally tiny.

      Let \(\mathscr {Q}\) be an elementary topos equipped with a subterminal object \(\P \hookrightarrow \mathbf {1}\) inducing an open subtopos \(\mathscr {E}\simeq {\mathscr {Q}}_{/\P }\hookrightarrow \mathscr {Q}\) and its complementary closed subtopos \(\mathscr {F}\hookrightarrow \mathscr {Q}\). This structure is the basis of the interpretation of STC; if you think of STC in terms of refinements, then stuff from \(\mathscr {E}\) is “computational” and stuff from \(\mathscr {F}\) is “logical”.

      We now consider the interpretation of a language of (potentially quantitative) refinements into \(\mathscr {Q}\). A context \(\Gamma \) is interpreted by an object of \(\mathscr {Q}\); a type \(\Gamma \vdash A\) is interpreted by a family \(A\to \bigcirc {\Gamma }\); a term \(\Gamma \vdash a : A\) is interpreted as a map \(\Gamma \to A\) such that \(\Gamma \to A \to \bigcirc \Gamma \) is the unit of the monad.

      So far we have not needed anything beyond the base structure of STC in order to give an interpretation of types in QTT’s style. But to extend this interpretation to a universe, we must additionally assume that \(\P \) is internally tiny, in the sense that the exponential functor \({\mathopen {}\left (-\right )\mathclose {}}^\P \) is a left adjoint. Under these circumstances, the idempotent monad \(\bigcirc \equiv j_*j^* : \mathscr {Q}\to \mathscr {Q}\) corresponding to the open immersion \(j : \mathscr {E}\hookrightarrow \mathscr {Q}\) has a right adjoint \(\square : \mathscr {Q}\to \mathscr {Q}\), an idempotent comonad.

      Proof. 

      As \(\bigcirc \equiv j_*j^*\) is the exponential functor \({\mathopen {}\left (-\right )\mathclose {}}^\P \), its right adjoint \(\square \) is therefore the “root functor” \({\mathopen {}\left (-\right )\mathclose {}}_\P \) that exhibits \(\P \) as an internally tiny object.

      Although \(\square \) lifts to each slice of \(\mathscr {Q}\), these liftings do not commute with base change; this will, however, not be an obstacle for us.

      We will now see how to use the adjunction \(\bigcirc \dashv \square \) to interpret a universe, either for the purpose of interpreting universes of refinement types, or for the purpose of strictifying the model that we have sketched. Let \(\mathcal {V}\) be a (standard) universe in \(\mathscr {Q}\), e.g. a Hofmann–Streicher universe; we shall then interpret the corresponding universe of refinements as \(\mathcal {U}:\equiv \square \mathcal {V}\). To see that \(\mathcal {U}\) classifies \(\mathcal {V}\)-small families of refinements, we compute as follows:

      1. A code \(\Gamma \vdash \hat {A} : \mathcal {U}\) amounts to nothing more than a morphism \(\hat {A}:\Gamma \to \square {\mathcal {V}}\).
      2. By adjoint transpose, this is the same as a morphism \(\hat {A}^\sharp : \bigcirc {\Gamma }\to \mathcal {V}\).

      Thus we see that if \(\mathcal {V}\) is generic for \(\mathcal {V}\)-small families of (arbitrary) types in \(\mathscr {Q}\), then \(\mathcal {U} \equiv \square \mathcal {V}\) is generic for \(\mathcal {V}\)-small families of type refinements, i.e. types whose context is \(\bigcirc \)-modal.

      Finally, we comment that the tininess of \(\P \) is satisfied in many standard examples, the simplest of which is the Sierpiński topos \(\mathbf {Set}^{\to }\).

      Classifying topoi and generalised abstract syntax [008J]

      For any small category \(\mathscr {C}\), Fiore treats \(\mathscr {C}\)-sorted abstract syntax in the functor category \({\mathopen {}\left [\mathscr {C},\operatorname {Pr}{\mathopen {}\left (\operatorname {\mathbb {L}}{\mathscr {C}}\right )\mathclose {}}\right ]\mathclose {}}\) where \(\operatorname {\mathbb {L}}\) is some 2-monad on \(\mathbf {Cat}\); any such functor \(P\) denotes a set that is indexed in sorts and contexts (where the 2-monad \(\operatorname {\mathbb {L}}\) takes a category of sorts to the corresponding category of contexts). When \(\mathscr {C}\) is a set and \(\operatorname {\mathbb {L}}\) is either finite limit or finite product completion, we recover the standard notions of many-sorted abstract syntax; in general, we get a variety of forms of dependently sorted or generalised abstract syntax.

      We will assume here that \(\operatorname {\mathbb {L}}\) is the free finite limit completion 2-monad; our goal is to study Fiore’s general substitution monoidal structure from the point of view of classifying topoi, building on Johnstone’s analogous observations (Elephant, D3.2) on the non-symmetric monoidal structure of the object classifier. The topos theoretic viewpoint that we will explore is nothing more than a rephrasing of Fiore’s account in terms of the Kleisli composition in a 2-monad; nonetheless the perspective of classifying topoi is enlightening, as it provides an explanation for precisely what internal geometrical structure one expects in a given topos for abstract syntax, potentially leading to improved internal languages.

      For any small category \(\mathscr {C}\), the category of presheaves \(\operatorname {Pr}{\mathopen {}\left (\operatorname {\mathbb {L}}\mathscr {C}\right )\mathclose {}}\) corresponds to the classifying topos of diagrams of shape \(\mathscr {C}\). Following Anel and Joyal, we shall write \(\mathbb {A}^{\mathscr {C}}\) for this “affine” classifying topos; under the conventions of op. cit., we may then identify the category of sheaves \(\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}\) with the presheaf category \(\operatorname {Pr}{\mathopen {}\left (\operatorname {\mathbb {L}}{\mathscr {C}}\right )\mathclose {}}\).

      The universal property of \(\mathbb {A}^{\mathscr {C}}\) as the classifying topos of \(\mathscr {C}\)-diagrams means that for any topos \(\mathcal {X}\), a diagram \({\mathscr {C}}\xrightarrow {{P}}{\operatorname {Sh}{\mathcal {X}}}\) corresponds essentially uniquely (by left Kan extension) to a morphism of topoi \({\mathcal {X}}\xrightarrow {{\bar {P}}}{\mathbb {A}^{\mathscr {C}}}\). We have a generic \(\mathscr {C}\)-shaped diagram \({\mathscr {C}}\xrightarrow {{\mathrm {G}_{\mathscr {C}}}}{\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}}\) corresponding under this identification to the identity map on \(\mathbb {A}^{\mathscr {C}}\). More explicitly, the diagram \(\mathrm {G}_{\mathscr {C}}\) is the following composite:

      \[ \mathrm {G}_{\mathscr {C}} :\equiv \mathscr {C}\xrightarrow {\eta _\mathscr {C}} \operatorname {\mathbb {L}}\mathscr {C}\xrightarrow {よ_{\mathscr {C}}} \operatorname {Pr}{\mathopen {}\left (\operatorname {\mathbb {L}}\mathscr {C}\right )\mathclose {}} = \operatorname {Sh}{\mathbb {A}^{\mathscr {C}}} \]

      Given a morphism of topoi \({\mathcal {X}}\xrightarrow {{f}}{\mathbb {A}^{\mathscr {C}}}\), we may recover the diagram \(\mathscr {C}\to {\operatorname {Sh}{\mathcal {X}}}\) that it classifies as the composite \(\mathscr {C}\xrightarrow {\mathrm {G}_{\mathscr {C}}}\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}\xrightarrow {f^{*}}\operatorname {Sh}{\mathcal {X}}\).

      In case \(\mathcal {X}\equiv \mathbb {A}^{\mathscr {C}}\), then, we have a correspondence between \(\mathscr {C}\)-shaped diagrams of sheaves on \(\mathbb {A}^{\mathscr {C}}\) and endomorphisms of \(\mathbb {A}^{\mathscr {C}}\); we are interested in representing the compositions of such endomorphisms as a tensor product on the functor category \({\mathopen {}\left [\mathscr {C},\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}\right ]\mathclose {}}\).

      In particular, let \({\mathscr {C}}\xrightarrow {{P,Q}}{\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}}\) be two diagrams; taking characteristic maps, we have endomorphisms of affine topoi \({\mathbb {A}^{\mathscr {C}}}\xrightarrow {{\bar {P},\bar {Q}}}{\mathbb {A}^{\mathscr {C}}}\), which we may compose to obtain \({\mathbb {A}^{\mathscr {C}}}\xrightarrow {{\bar {Q}\circ \bar {P}}}{\mathbb {A}^{\mathscr {C}}}\); then, we will define the tensor \(P\bullet Q\) to be the diagram whose characteristic morphism of affine topoi is \(\bar {P}\circ \bar {Q}\). In other words:

      \[ \begin {aligned} P\bullet Q &:\equiv \mathscr {C}\xrightarrow {\mathrm {G}_{\mathscr {C}}} \operatorname {Sh}{\mathbb {A}^{\mathscr {C}}} \xrightarrow {{\mathopen {}\left (\bar {P}\circ \bar {Q}\right )\mathclose {}}^{*}} \operatorname {Sh}{\mathbb {A}^{\mathscr {C}}} \\ &= \mathscr {C}\xrightarrow {\mathrm {G}_{\mathscr {C}}} \operatorname {Sh}{\mathbb {A}^{\mathscr {C}}} \xrightarrow {\bar {P}^{*}} \operatorname {Sh}{\mathbb {A}^{\mathscr {C}}} \xrightarrow {\bar {Q}^{*}} \operatorname {Sh}{\mathbb {A}^{\mathscr {C}}} \end {aligned} \]

      To give an explicit computation of the tensor product, we first compute the inverse image of any \({\mathbb {A}^{\mathscr {C}}}\xrightarrow {{f}}{\mathbb {A}^{\mathscr {C}}}\) on representables \(よ_{\mathscr {C}}\Gamma \) for \(\Gamma \in \operatorname {\mathbb {L}}\mathscr {C}\). As any left exact functor \({\operatorname {\mathbb {L}}\mathscr {C}}\xrightarrow {{H}}{\mathscr {E}}\) is the right Kan extension of \({\mathscr {C}}\xrightarrow {{H\circ \eta _\mathscr {C}}}{\mathscr {E}}\) along \({C}\xrightarrow {{\eta _\mathscr {C}}}{\operatorname {\mathbb {L}}\mathscr {C}}\), we can conclude that \(H\Gamma \cong \operatorname {lim}_{\Gamma \to \eta _\mathscr {C}{d}}H{\mathopen {}\left (\eta _\mathscr {C}{d}\right )\mathclose {}}\). We will use this in our calculation below, setting \(H:\equiv f^{*}\circ よ_{\mathscr {C}}\).

      \[ \begin {aligned} f^{*}{よ_{\mathscr {C}}\Gamma } &\cong \operatorname {lim}_{\Gamma \to \eta _\mathscr {C}{d}} f^{*}{ よ_{\mathscr {C}}{\eta _\mathscr {C}{d}} } \\ &\cong \operatorname {lim}_{\Gamma \to \eta _\mathscr {C}{d}} f^{*}{\mathrm {G}_{\mathscr {C}}{d}} \end {aligned} \]

      We are now prepared to compute the tensor product of any \({\mathscr {C}}\xrightarrow {{P,Q}}{\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}}\).

      \[ \begin {aligned} {\mathopen {}\left (P\bullet Q\right )\mathclose {}}c &= \bar {Q}^{*} \bar {P}^{*} \mathrm {G}_{\mathscr {C}}{c} \\ &\cong \bar {Q}^{*} {\mathopen {}\left (Pc\right )\mathclose {}} \\ &\cong \bar {Q}^{*} \operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc} よ_{\mathscr {C}}\Delta \\ &\cong \operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc} \bar {Q}^{*}よ_{\mathscr {C}}\Delta \\ &\cong \operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc} \operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}} \bar {Q}^{*}\mathrm {G}_{\mathscr {C}}d \\ &\cong \operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc} \operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}} Qd \end {aligned} \]

      Finally, we can relate the computation above to that of Fiore in terms of coends.

      \[ \begin {aligned} {\mathopen {}\left (P\bullet Q\right )\mathclose {}}\,c &\cong \operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc} \operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}} Qd \\ &\cong \int ^{\Delta \in \operatorname {\mathbb {L}}\mathscr {C}} {\mathopen {}\left [よ_{\mathscr {C}}\Delta ,Pc\right ]\mathclose {}} \cdot \operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}} Qd \\ &\cong \int ^{\Delta \in \operatorname {\mathbb {L}}\mathscr {C}} P\,c\,\Delta \cdot \operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}} Qd \\ &\cong \int ^{\Delta \in \operatorname {\mathbb {L}}\mathscr {C}} P\,c\,\Delta \cdot \int _{c\in \mathscr {C}} {\mathopen {}\left [\Delta ,\eta _\mathscr {C}{d}\right ]\mathclose {}}\pitchfork Qd \end {aligned} \]

      Above, we have written \({\mathopen {}\left (\cdot \right )\mathclose {}}\) and \({\mathopen {}\left (\pitchfork \right )\mathclose {}}\) for the tensoring and cotensoring of \(\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}\) over \(\mathbf {Set}\) respectively. Thus, the fully pointwise computation is as follows:

      \[ {\mathopen {}\left (P\bullet Q\right )\mathclose {}}\,c\,\Gamma \cong \int ^{\Delta \in \operatorname {\mathbb {L}}\mathscr {C}} P\,c\,\Delta \times \int _{c\in \mathscr {C}} {\mathopen {}\left [\Delta ,\eta _\mathscr {C}{d}\right ]\mathclose {}}\Rightarrow Q\,d\,\Gamma \]

      Thanks to Marcelo Fiore and Daniel Gratzer for helpful discussions.

      Scientific refereeing using Bike Outliner [0084]

      I have long been an enthusiast for outliners, a genre of computer software that deserves more than almost any other to be called an “elegant weapon for a more civilized age”. Recently I have been enjoying experimenting with Jesse Grosjean’s highly innovative outliner for macOS called Bike, which builds on a lot of his previous (highly impressive) work in the area with a level of fit and finish that is rare even in the world of macOS software. Bike costs $29.99 and is well-worth it; watch the introductory video or try the demo to see for yourself.

      The purpose of outliners is to provide room to actively think; Grothendieck is said to have been unable to think at all without a pen in his hand, and I think of outliners as one way to elevate the tactile aspect of active thinking using the unique capabilities of software. Tools for thinking must combat stress and mental weight, and the most immediate way that outliners achieve this is through the ability to focus on a subtree — narrowing into a portion of the hierarchy and treating it as if it were the entire document, putting its context aside. This feature, which some of my readers may recognize from Emacs org-mode, is well-represented in Bike — without, of course, suffering the noticeable quirks that come from the Emacs environment, nor the ill-advised absolute/top-down model of hierarchy sadly adopted by org-mode.

      As a scientist in academia, one of the most frequent things I am doing when I am not writing my own papers or working with students is refereeing other scientists’ papers. For those who are unfamiliar, this means carefully studying a paper and then producing a detailed and well-structured report that includes a summary of the paper, my personal assessment of its scientific validity and value, and a long list of corrections, questions, comments, and suggestions. Referee reports of this kind are then used by journal editors and conference program committees to decide which papers deserve to be published.

      In this post, I will give an overview of my refereeing workflow with Bike and how I overcame the challenges transferring finished referee reports from Bike into the text-based formats used by conference refereeing platforms like HotCRP and EasyChair using a combination of XSLT 2.0 and Pandoc. This tutorial applies to Bike 1.14; I hope the format will not change too much, but I cannot make promises about what I do not control.

      Refereeing in an outliner [0089]

      Most scientific conferences solicit and organize reviews for papers using a web platform such as HotCRP and EasyChair; although these are not the same, the idea is similar. Once you have been assigned to referee a paper, you will receive a web form with several sections and large text areas in which to put the components of your review; not all conferences ask for the same components, but usually one is expected to include the following in addition to your (numerical) assessment of the paper’s merit and your expertise:

      1. A summmary of the paper
      2. Your assessment of the paper
      3. Detailed comments for the authors
      4. Questions to be addressed by author response
      5. Comments for the PC (program committee) and other reviewers

      Usually you will be asked to enter your comments under each section in a plain text format like Markdown. The first thing a new referee learns is not to type answers directly into the web interface, because this is an extremely reliable way to lose hours of your time when a browser or server glitch deletes all your work. Most of us instead write out our answers in a separate text editor, and paste them into the web interface when we are satisfied with them. In the past, I have done this with text files on my computer, but today I want to discuss how to draft referee reports as outlines in Bike; then I will show you how to convert them to the correct plain text format that can be pasted into your conference’s preferred web-based refereeing platform.

      To start off, have a look at the figure below, which shows my refereeing template outline in Bike.

      Figure. A Bike outline for conference refereeing [0086]

      This Bike outline contains the skeleton of a referee report for a major computer science conference. Bike’s row types are used extensively: for example, sections are formatted as headings, and prompts are formatted as notes

      As you can see, there is a healthy combination of hierarchy and formatting in a Bike outline.

      Rich text editing in Bike [008B]

      Bike is a rich text editor, but one that (much like GNU TeXmacs) avoids the classic pitfalls of nearly all rich text editors, such as the ubiquitous and dreaded “Is the space italic?!” user-experience failure; I will not outline Bike innovative approach to rich text editing here, but I suggest you check it out for yourself.

      Row types in Bike [008A]

      One of the most useful features of Bike’s approach to formatting is the concept of a row type, which is a semantic property of a row that has consequences for its visual presentation. Bike currently supports the following row types:

      • Plain rows
      • Heading rows, formatted in boldface
      • Note rows, formatted in gray italics
      • Quote rows, formatted with a vertical bar to their left
      • Ordered rows, formatted with an (automatically chosen) numeral to their left
      • Unordered rows, formatted with a bullet to their left
      • Task rows, formatted with a checkbox to their left

      My refereeing template uses several of these row types (headings, notes, tasks) as well as some of the rich text formatting (highlighting). When I fill out the refereeing outline, I will use other row types as well — including quotes, ordered, and unordered rows. I will create a subheading under Detailed comments for the author to contain my questions and comments, which I enter in as ordered rows; then I make a separate subheading at the same level for Typographical errors, which I populate with unordered rows. Unordered rows are best for typos, because they are always accompanied already by line numbers. If I need to quote an extended portion of the paper, I will use a quote row.

      When working on the report outline, I will constantly be focusing on individual sections to avoid not only distractions but also the intense mental weight of unfinished sections. Focusing means that the entire outline is narrowed to a subtree that can be edited away from its context; this is achieved in Bike by pressing the gray south-easterly arrows to the right of each heading, as seen in the figure.

      From an outline to a plain text referee report [008C]

      Although we have seen how pleasant it is to use an outliner like Bike to draft a referee report, but we obviously cannot submit a .bike file to a conference reviewing website or a journal editor. Most conference reviewing systems accept plain text or Markdown responses, and so our goal will be to convert a Bike outline into reasonably formatted Markdown.

      It happens that Bike’s underlying format is HTML, so one idea would be to use Pandoc to process this HTML into Markdown. This would work, except that Bike’s model is sufficiently structured that it must make deeply idiosyncratic use of HTML tags, as can be seen from the listing below.

      Listing. The source code to a typical Bike outline [008G] 

      <?xml version="1.0" encoding="UTF-8"?>
<html xmlns="http://www.w3.org/1999/xhtml">
  <head>
    <meta charset="utf-8"/>
  </head>
  <body>
    <ul id="2sbcmmms">
      <li id="3C" data-type="heading">
        <p>Tasks</p>
        <ul>
          <li id="cs" data-type="task">
            <p>read through paper on iPad and highlight</p>
          </li>
        </ul>
      </li>
      <li id="XZ" data-type="heading">
        <p>Syntax and semantics of foo bar baz</p>
        <ul>
          <li id="Kp">
            <p><mark>Overall merit:</mark><span> </span></p>
          </li>
          <li id="d9">
            <p><mark>Reviewer Expertise:</mark></p>
          </li>
          <li id="uM" data-type="heading">
            <p>Summary of the paper</p>
            <ul>
              <li id="oB" data-type="note">
                <p>Please give a brief summary of the paper</p>
              </li>
              <li id="TWZ">
                <p>This paper describes the syntax and semantics of foo, bar, and baz.</p>
              </li>
            </ul>
          </li>
          <li id="V8" data-type="heading">
            <p>Assessment of the paper</p>
            <ul>
              <li id="vD" data-type="note">
                <p>Please give a balanced assessment of the paper's strengths and weaknesses and a clear justification for your review score.</p>
              </li>
            </ul>
          </li>
          <li id="zo" data-type="heading">
            <p>Detailed comments for authors</p>
            <ul>
              <li id="o0" data-type="note">
                <p>Please give here any additional detailed comments or questions that you would like the authors to address in revising the paper.</p>
              </li>
              <li id="bgy" data-type="heading">
                <p>Minor comments</p>
                <ul>
                  <li id="tMq" data-type="unordered">
                    <p>line 23: "teh" =&gt; "the"</p>
                  </li>
                  <li id="EmX" data-type="unordered">
                    <p>line 99: "fou" =&gt; "foo"</p>
                  </li>
                </ul>
              </li>
            </ul>
          </li>
          <li id="aN" data-type="heading">
            <p>Questions to be addressed by author response</p>
            <ul>
              <li id="7s" data-type="note">
                <p>Please list here any specific questions you would like the authors to address in their author response. Since authors have limited time in which to prepare their response, please only ask questions here that are likely to affect your accept/reject decision.</p>
              </li>
            </ul>
          </li>
          <li id="4S" data-type="heading">
            <p>Comments for PC and other reviewers</p>
            <ul>
              <li id="bN" data-type="note">
                <p>Please list here any additional comments you have which you want the PC and other reviewers to see, but not the authors.</p>
              </li>
              <li id="i2b">
                <p>In case any one is wondering, I am an expert in foo, but not in bar nor baz.</p>
              </li>
            </ul>
          </li>
        </ul>
      </li>
    </ul>
  </body>
</html>

      The Markdown that would result from postprocessing a Bike outline directly with Pandoc would be deeply unsuitable for submission. We will, however, use a version of this idea: first we will preprocess the Bike format into more conventional (unstructured) HTML using XSLT 2.0, and then we will use Pandoc to convert this into Markdown.

      System requirements to convert Bike outlines to Markdown [008E]

      XSLT 2.0 is unfortunately only implemented by proprietary tools like Saxon, developed by Saxonica. Nonetheless, it is possible to freely install Saxon on macOS using Homebrew:

      brew install saxon

      You must also install Pandoc, which is also conveniently available as a binary on Homebrew:

      brew install pandoc

      With the system requirements out of the way, we can proceed to prepare an XSLT stylesheet that will convert Bike’s idiosyncratic use of HTML tags to more conventional HTML that can be processed into Markdown by Pandoc. The stylesheet bike-to-html.xsl is described and explained in the listing below.

      Listing. An XSLT 2.0 transformer to convert Bike outlines to HTML [0087]

      We can write convert Bike outlines to reasonable HTML using an XSLT 2.0 stylesheet, bike-to-html.xsl detailed below.

      <?xml version="1.0"?>

<xsl:stylesheet version="2.0"
  xmlns="http://www.w3.org/1999/xhtml"
  xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  xmlns:html="http://www.w3.org/1999/xhtml"
  exclude-result-prefixes="xhtml">

  <xsl:output method="xml" version="1.0" encoding="UTF-8" indent="yes" />
  <xsl:strip-space elements="*" />

      We will allow several tags to be copied verbatim into the output, as Bike uses these in the same way that idiomatic HTML does.

        <xsl:template match="html:html | html:body | html:code | html:strong | html:em | html:mark">
    <xsl:copy>
      <xsl:apply-templates select="node()|@*" />
    </xsl:copy>
  </xsl:template>

      Bike leaves behind a lot of empty span elements; we drop these.

        <xsl:template match="html:span">
    <xsl:apply-templates />
  </xsl:template>

      Bike uses ul for all lists; the list type is determined not at this level, but rather by each individual item’s @data-type attribute. To get this data into the HTML list model, we must group items that have the same @data-type and wrap them in an appropriate list-forming element.

      To do this, we use XSLT 2.0’s xsl:for-each-group instruction to group adjacent li elements by their @data-type attribute. (It is extremely difficult and error-prone to write equivalent code in the more widely available XSLT 1.0.) We must convert @data-type to a string: otherwise, the transformer will crash when it encounters an item without a @data-type attribute.

        <xsl:template match="html:ul">
    <xsl:for-each-group select="html:li" group-adjacent="string(@data-type)">
      <xsl:choose>
        <xsl:when test="@data-type='ordered' or @data-type='task'">
          <ol>
            <xsl:apply-templates select="current-group()" />
          </ol>
        </xsl:when>
        <xsl:when test="@data-type='unordered'">
          <ul>
            <xsl:apply-templates select="current-group()" />
          </ul>
        </xsl:when>
        <xsl:otherwise>
          <xsl:apply-templates select="current-group()" />
        </xsl:otherwise>
      </xsl:choose>
    </xsl:for-each-group>
  </xsl:template>

      Next, we match each individual li element; the content of a list item is stored in a p element directly under li, so we let the transformer fall thorugh the parent and then format the content underneath according to the @data-type of the item.

        <xsl:template match="html:li">
    <xsl:apply-templates />
  </xsl:template>

  <xsl:template
    match="html:li[@data-type='ordered' or @data-type='unordered' or @data-type='task']/html:p">
    <li>
      <xsl:apply-templates />
    </li>
  </xsl:template>

      Bike has correctly adopted the optimal explicit and relative model of hierarchy, in contrast to HTML; this means that the depth of a heading is not reflected in the element that introduces it, but is instead inferred from its actual position in the outline hierarchy. To convert Bike outlines to idiomatic HTML, we must flatten the hierarchy and introduce explicit heading levels; luckily, this is easy to accomplish in XSLT by counting the ancestors of heading type.

        <xsl:template match="html:li[@data-type='heading']/html:p">
    <xsl:element
      name="h{count(ancestor::html:li[@data-type='heading'])}">
      <xsl:apply-templates />
    </xsl:element>
  </xsl:template>

      The remainder of the row types are not difficult to render; you may prefer alternative formatting depending on your goals.

        <xsl:template match="html:li[@data-type='quote']/html:p">
    <blockquote>
      <xsl:apply-templates />
    </blockquote>
  </xsl:template>

  <xsl:template match="html:li[@data-type='note']/html:p">
    <p>
      <em>
        <xsl:apply-templates />
      </em>
    </p>
  </xsl:template>

  <xsl:template match="html:li[not(@data-type)]/html:p">
    <p>
      <xsl:apply-templates />
    </p>
  </xsl:template>
</xsl:stylesheet>

      Next, we can use Saxon to convert a Bike outline to idiomatic HTML using the stylesheet above.

      cat review.bike | saxon -xsl:bike-to-html.xsl - > review.html

      Go ahead and open the resulting HTML file in a text editor and a browser to see the results.

      Listing. A Bike outline transformed to idiomatic HTML [008F]

      The following is the result of transforming an example Bike outline to idiomatic HTML using an XSLT stylesheet.

      <?xml version="1.0" encoding="UTF-8"?>
<html xmlns="http://www.w3.org/1999/xhtml">
   <body>
      <h1>Tasks</h1>
      <ol>
         <li>read through paper on iPad and highlight</li>
      </ol>
      <h1>Syntax and semantics of foo bar baz</h1>
      <p>
         <mark>Overall merit:</mark>
      </p>
      <p>
         <mark>Reviewer Expertise:</mark>
      </p>
      <h2>Summary of the paper</h2>
      <p>
         <em>Please give a brief summary of the paper</em>
      </p>
      <p>This paper describes the syntax and semantics of foo, bar, and baz.</p>
      <h2>Assessment of the paper</h2>
      <p>
         <em>Please give a balanced assessment of the paper's strengths and weaknesses and a clear justification for your review score.</em>
      </p>
      <h2>Detailed comments for authors</h2>
      <p>
         <em>Please give here any additional detailed comments or questions that you would like the authors to address in revising the paper.</em>
      </p>
      <h3>Minor comments</h3>
      <ul>
         <li>line 23: "teh" =&gt; "the"</li>
         <li>line 99: "fou" =&gt; "foo"</li>
      </ul>
      <h2>Questions to be addressed by author response</h2>
      <p>
         <em>Please list here any specific questions you would like the authors to address in their author response. Since authors have limited time in which to prepare their response, please only ask questions here that are likely to affect your accept/reject decision.</em>
      </p>
      <h2>Comments for PC and other reviewers</h2>
      <p>
         <em>Please list here any additional comments you have which you want the PC and other reviewers to see, but not the authors.</em>
      </p>
      <p>In case any one is wondering, I am an expert in foo, but not in bar nor baz.</p>
   </body>
</html>

      Next, we will process this HTML file using Pandoc; unfortunately, Pandoc leaves behind a lot of garbage character escapes that are not suitable for submission anywhere, so we must filter those out using sed.

      cat review.html | pandoc -f html -t markdown-raw_html-native_divs-native_spans-fenced_divs-bracketed_spans-smart | sed 's/\\//g'

      Listing. A Bike outline transformed to Markdown [008H]

      The following is the result of converting the idiomatic HTML representation of a Bike outline to Markdown using Pandoc, with some light postprocessing by sed.

      # Tasks

1.  read through paper on iPad and highlight

# Syntax and semantics of foo bar baz

Overall merit:

Reviewer Expertise:

## Summary of the paper

*Please give a brief summary of the paper*

This paper describes the syntax and semantics of foo, bar, and baz.

## Assessment of the paper

*Please give a balanced assessment of the paper's strengths and
weaknesses and a clear justification for your review score.*

## Detailed comments for authors

*Please give here any additional detailed comments or questions that you
would like the authors to address in revising the paper.*

### Minor comments

-   line 23: "teh" => "the"
-   line 99: "fou" => "foo"

## Questions to be addressed by author response

*Please list here any specific questions you would like the authors to
address in their author response. Since authors have limited time in
which to prepare their response, please only ask questions here that are
likely to affect your accept/reject decision.*

## Comments for PC and other reviewers

*Please list here any additional comments you have which you want the PC
and other reviewers to see, but not the authors.*

In case any one is wondering, I am an expert in foo, but not in bar nor
baz.

      We can compose all these tasks into a one-liner as follows:

      cat review.bike | saxon -xsl:bike-to-html.xsl - | pandoc -f html -t markdown-raw_html-native_divs-native_spans-fenced_divs-bracketed_spans-smart | sed 's/\\//g'

      A convenient Bike-to-Markdown script [008I]

      I have gathered the scripts to convert Bike outlines into Markdown via idiomatic HTML in a Git repository where they can be easily downloaded. If you have any improvements to these scripts, please submit them as a patch to my public inbox! I am also interested in whether it is possible to write the XSLT 2.0 stylesheet as equivalent XSLT 1.0, to avoid requiring the proprietary Saxon tool. Feel free also to send comments on this post to my public inbox, or discuss with me on Mastodon.

      ☕. Crowdfunding and sponsorship [0088]

      Apart from my day-job at the University of Cambridge, I am independently researching tools for scientific thought and developing software like Forester that you can use to unlock your brain. If you have benefited from this work or the writings on my blog, please considering supporting me with a sponsorship on Ko-fi.

      A synthetic proof of HTT 7.2.1.14 [007T]

      Lurie states the following result as Proposition 7.2.1.14 of Higher Topos Theory:

      Let \(\mathcal {X}\) be an ∞-topos and let \({\mathcal {X}}\xrightarrow {{\tau _{\leq 0}}}{\tau _{\leq 0}\mathcal {X}}\) be the left adjoint to the inclusion. A morphism \({U}\xrightarrow {{\phi }}{X}\) in \(\mathcal {X}\) is an effective epimorphism if and only if in \(\tau _{\leq 0}{\mathopen {}\left (\phi \right )\mathclose {}}\) is an effective epimorphism in the ordinary topos \(\mathrm {h}{\mathopen {}\left (\tau _{\leq 0}\mathcal {X}\right )\mathclose {}}\).

      Several users of MathOverflow have noticed that the proof of this result given by Lurie is circular. The result is true and can be recovered in a variety of ways, as pointed out in the MathOverflow discussion. For expository purposes, I would like to show how to prove this result directly in univalent foundations using standard results about \(n\)-truncations from the HoTT Book.

      First we observe a trivial lemma about truncations.

      Lemma. Propositions do not notice set truncation of indices [007U]

      Any proposition is orthogonal to the map \(\mathchoice {\textstyle \sum _{{\mathopen {}\left (x:A\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (x:A\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (x:A\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (x:A\right )\mathclose {}}}}B\left \lvert x\right \rvert _{0}\to \mathchoice {\textstyle \sum _{{\mathopen {}\left (x:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (x:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (x:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (x:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}Bx\) sending \({\mathopen {}\left (x,y\right )\mathclose {}}\) to \({\mathopen {}\left (\left \lvert x\right \rvert _{0},y\right )\mathclose {}}\).

      Proof. 

      This follows from the dependent induction principle of set-truncation, as any proposition is a set.

      It follows from Lemma [007U] that \(\left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (x:A\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (x:A\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (x:A\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (x:A\right )\mathclose {}}}}B\left \lvert x\right \rvert _{0}\right \rVert _{-1}\) is equivalent to \(\left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (x:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (x:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (x:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (x:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}Bx\right \rVert _{-1}\). This is enough to deduce the main result.

      Theorem. Set-truncation preserves and reflects surjections [007V]

      A function \(f:A\to B\) is surjective (i.e. an effective epimorphism) if and only if its set-truncation \(\left \lVert f\right \rVert _{0}:\left \lVert A\right \rVert _{0}\to \left \lVert B\right \rVert _{0}\) is surjective.

      Proof. 

      We deduce that \(\mathsf {isSurjective}\,\left \lvert f\right \rvert _{0}\) is equivalent to \(\mathsf {isSurjective}\,f\) as follows:

      \(\mathsf {isSurjective}\,\left \lvert f\right \rvert _{0}\)
      \( \equiv \mathchoice {\textstyle \prod _{{\mathopen {}\left (b:\left \lVert B\right \rVert _{0}\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:\left \lVert B\right \rVert _{0}\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:\left \lVert B\right \rVert _{0}\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:\left \lVert B\right \rVert _{0}\right )\mathclose {}}}}\left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}\left \lVert f\right \rVert _{0}a=b\right \rVert _{-1} \) by definition
      \( \simeq \mathchoice {\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}} \left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:\left \lVert A\right \rVert _{0}\right )\mathclose {}}}}\left \lVert f\right \rVert _{0}a=\left \lvert b\right \rvert _{0}\right \rVert _{-1} \) by induction
      \( \simeq \mathchoice {\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}} \left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}\left \lvert fa\right \rvert _{0}=\left \lvert b\right \rvert _{0}\right \rVert _{-1} \) by Lemma
      \( \simeq \mathchoice {\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}} \left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}\left \lVert fa=b\right \rVert _{-1}\right \rVert _{-1} \) by HoTT Book, Theorem 7.3.12
      \( \simeq \mathchoice {\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\textstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}}{\scriptscriptstyle \prod _{{\mathopen {}\left (b:B\right )\mathclose {}}}} \left \lVert \mathchoice {\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\textstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}{\scriptscriptstyle \sum _{{\mathopen {}\left (a:A\right )\mathclose {}}}}fa=b\right \rVert _{-1} \) by HoTT Book, Theorem 7.3.9
      \( \equiv \mathsf {isSurjective}\,f \) by definition

      Incidentally, the appeal to Theorem 7.3.12 of the HoTT Book can be replaced by the more general Proposition 2.26 of Christensen et al., which applies to an arbitrary reflective subuniverse and the corresponding subuniverse of separated types.

      Backlinks

        Sending strict propositions to the Ripley cupboard [01IK]

        Please note: I am no longer confident in the conclusions of this post, and I believe that I have made some mistakes. When I have ironed out what is true and what is not true, I will write a follow-up and link to it from here.

        Conor Mc Bride likes to send hopeless ideas and design mistakes to their Ripley Cupboard, a reference to a scene in the highly underrated film Alien: Resurrection in which all the hopeless attempts to reconstruct Ellen Ripley from DNA are stored in a gruesome menagerie. I am afraid that in spite of their successful semantic rehabilitation, strict / definitionally proof-irrelevant propositions must nonetheless find their permanent residence in my own Ripley cupboard for syntactical reasons.

        One thing that I had noticed a couple nights ago was that there might be a problem finding a suitable generalisation of Miller’s pattern fragment for dependent type theory with strict propositions. I was not really precise about what my concern was, but thankfully Matthieu Sozeau managed to pin it down.

        In essence, the problem has to do with what syntacticians call “strengthening”. The thing that makes higher-order pattern unification work well is the ability to tell whether or not some term actually depends on a given variable up to definitional equality; this is important because if you can eliminate a syntactic dependency, two things might happen that could allow the unification process to proceed further (1) a blocked unification problem may suddenly fall into the pattern fragment, and (2) a failing “occurs check” may start to succeed.

        With definitional singleton types, this is all fine: we can reliably eliminate dependency on singletons in a number of different ways, but these ways all rely on the fact that singleton types are inhabited. For definitional subsingletons, i.e. strict propositions, it is another story. Imagine that you have a strict proposition \(P\) and a subterm \(M(x,y,z):P\) of a larger proof-relevant unification problem; in order to find out whether or not the whole problem depends on \(x,y,z\) you need to know whether or not a “shorter” proof of \(P\) is derivable, which is obviously an undecidable problem.

        The upshot is, as Matthieu put it, we are not going to be able to find most general unifiers in any fragment of the language that involves strict propositions. Completeness of unification within a well-defined fragment is, in my opinion, the mathematical shadow of a more important but intangible property of unification being reliable and predictable. Therefore, I think that this observation may imply that reliable and predictable unification is not compatible with having strict propositions in any form.

        The implication for Project Pterodactyl is that we will not be pursuing strict propositions in any form, including my recent proposal.

        (It would be very welcome if someone noticed a way to get around this apparent obstruction, but I am not optimistic. It seems pretty airtight to me at the moment.)

        Weeknotes 2025-W43 › Project Pterodactyl blogging: goodbye to definitional proof-irrelevance [01IL]

        A few weeks ago, I wrote a post entitled Shall we strictify some homotopy propositions? in which I described a semantically viable way to reconcile the convenience of definitional proof irrelevance with the richer notion of proposition emerging from univalent foundations. Unfortunately, though the idea works semantically, I have found a no-go result for the reliable implementation of definitional proof irrelevance.

        Of course, definitional proof irrelevance is not even remotely reliable at all in Lean. But that is the tip of the iceberg for Lean and I had assumed that a more refined and educated algorithm could lead to a better result. (This is one of many instances of the Lean community’s propaganda falling far short of reality.) Unfortunately, my assumption that definitional proof irrelevance could be saved with a bit of finesse was incorrect: although we can certainly do better than Lean by having a sound and complete definitional equivalence checker, reliable unification is almost certainly impossible in the presence of definitionally proof-irrelevant propositions. To be fair, many systems treat unification as a heuristic and so most general unifiers need not be a goal; I have, however, come to the conclusion that choosing non-general unifiers leads to unpredictable behaviour that harms reliability and usability. I’ve written up the obstruction to most general unifiers in the following post: Sending strict propositions to the Ripley cupboard.

        Weeknotes 2025-W41 › Project Pterodactyl: fuss-free universes and strictifying propositions [01ID]

        I’ve continued my blogging spree on my Pterodactyl worklog, with two new posts:

        1. Fuss-free universe hierarchies
        2. Shall we strictify some homotopy propositions?

        The first one is about how we might organise universe hierarchies to avoid painful bureaucracy. The second one is about whether or not we can incorporate a useful form of definitional proof irrelevance into univalent foundations. I think the universes thing is more likely to make it into Pterodactyl as-is, whereas the strictification idea needs some workshopping and experimentation (and some mathematics!).

        Related

          Person. Cameron Zwarich [cameronzwarich]

          Person. Carlo Angiuli [carloangiuli]

          Person. Daniel Gratzer [danielgratzer]

          I study programming languages, type theories, and logics. I am particularly interested in applying semantic methods to prove syntactic properties of modal type theories and programming languages. I am also involved in the development of program logics for concurrent programming languages through the Iris project.

          Person. Rafaël Bocquet [rafaëlbocquet]