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.

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:

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

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!

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.

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.

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
  }
}

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.

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?

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.

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

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

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

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

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 13^th century, though most what stands today was rebuilt in the 15^th and 16^th centuries. Like essentially all churches of this age, it was originally Catholic until the dissolution of the monasteries by Henry VIII.

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.

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.

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

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.

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.

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.

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.

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.

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.

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

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

• October 7, 2025
• Jon Sterling

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

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

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

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

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

Proof. 

• October 7, 2025
• Jon Sterling

We consider the general scenario:

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

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

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

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

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.

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.

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.

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.

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

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

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}

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

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}
  // ...

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.

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

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.

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

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.

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.

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.

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.

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

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.

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.

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.

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.

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.

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:

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

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:

In the second branch, we can abstract the variable.

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

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

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.

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:

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:

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.

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.

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

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.

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.

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

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

• June 12, 2025
• Jon Sterling

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.

App development post iOS 7

• June 12, 2025
• Jon Sterling

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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

defaults write com.freron.MailMate MmFormatFlowedEnabled -bool true

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

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\):

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

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.

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\):

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

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.

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

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.

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]

• August 28, 2023
• Jon Sterling
• https://git.sr.ht/~jonsterling/bike-convertors/tree/main/item/example.bike

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

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.

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.

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

brew install saxon

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.

<?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="*" />

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

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

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

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

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

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

<?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'

# 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'

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.

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.

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

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.