August Update 1
In the past few weeks I prodded a little more at bicategorical proofs about left universal arrows. However, in the interest of time, I’m turning my attention more to (re)writing.
The Abridged Version
The abridged draft of my dissertation, to be suitable for publication in a conference, will be available at https://notes.eutro.dev/cs/diss/output/abridged.pdf shortly. Currently, the Preliminary Type Theory section has been considerably reduced, but I intend to reintroduce pointers to relevant material. I am thinking about how best to treat the introduction and Semantics and Evaluation Order sections. I have also cut various proofs and explicit definitions, where I’ll be reading through to make sure things are still coherent. The body is currently at 36 pages, down from 49 for the dissertation, but I’ll have to make sure there is enough information for things to be clear.
The Introduction
I am wondering if the introduction I wrote for my dissertation is the best introduction to the actual content, viewed as a mathematics paper. (The introduction walks through call-by-name and call-by-value giving rise to (an example of) non-associative composition.) From my perspective, thinking about programming language semantics is entirely irrelevant to the mathematics I did, even though it is a substantial motivator for duploids. On the other hand, the context is important, especially in referencing the related work like Levy’s contextual isomorphisms.
Comparing to other papers, the introduction of Mangel et al. [1] conveys somewhat similar information to my dissertation. This makes sense, because their paper is actually about duploids and semantics, which mine is not. By contrast, the work of van der Weide [2] on monads in Univalent Foundations does little more than mention the uses of monads, without belabouring the details. This also makes sense, in part because the use of monads is well-established.
In my paper I believe it will be sufficient to mention programming language semantics only in passing, so I can focus more on the specific motivation of my own work instead. I’m not sure how much I need to motivate duploids themselves, though. I will see how it goes.