4 minute read

I have done a great deal of writing since my last post. The most recent draft is at abridged.pdf, or with the date pinned at abridged-2026-09-13.pdf. I have done a lot of cutting down and making things more concise, so that the draft now sits at 22 pages (down from 49 at dissertation submission), but it may now be missing some important context and content.

I have also adopted an LNCS \(\LaTeX\) template, which is much more bare-bones than KOMA-Script and other niceties I let myself enjoy. I am still scared typeset the files with pdflatex rather than lualatex, as would be necessary for, say, arXiv.

Most of the gains in the current draft are from reducing the introduction and background from 16 pages down to about 3, with about 30-40% reductions everywhere else from either reduced content or more concise mathematics or prose.

Updated Introduction

I have culled almost the entirety of the background section in my dissertation, assimilating some relevant parts of it into a new introduction. I have erred on the side of cutting things out, especially material related to programming language semantics. The new introduction covers some necessary background on duploids and univalent categories, including some borderline philosophy on equality.

I don’t think I do enough to describe my own work and techniques just yet. I should at least mention the formalization itself, briefly, like I did originally. I should also give a nod to my use of reflexive graphs (that I have started upstreaming!), but I do not wish to elaborate too much on the specifics, at least in the main body. The other powerful technique I used extensively was regular-expression-based dualization, but I am not sure how best to present this as a serious technique to serious people. I must warn that the code is updated now so that earlier entries in eutro-dualize-alist can override shorter ones later in the list correctly:

(defcustom eutro-dualize-alist
  `(;; 41 entries at time of writing
    )
  "Alist of replacements to make in `eutro-dualize-region'."
  :type '(alist :key string :value string)
  :group 'eutro)

(defun eutro-dualize-region (start end)
  "Dualize the region according to `eutro-dualize-alist'."
  (interactive (progn
                 (cl-assert (use-region-p) nil "No region selected")
                 (list (region-beginning) (region-end))))
  (require 'regexpl)
  (save-excursion
    (goto-char start)
    (save-restriction
      (narrow-to-region start end)
      (regexpl-search-replace-list
       (mapcan (pcase-lambda (`(,x . ,y))
                 `((,(regexp-quote x) . ,(regexp-quote y))
                   (,(regexp-quote y) . ,(regexp-quote x))))
               eutro-dualize-alist)))))

Rewritten Chapters

I have rewritten most of the unital magmoids chapter and envelope duploid construction section. They now have more exposition in prose rather than just being theorem/definition spam, and have less repetition of material that I expect the reader to be familiar with (i.e. category theory). I also now define the oblique duploid using the envelope duploid, rather than doing a whole separate construction.

I am quite happy with the exposition for the envelope duploid construction. The fact that the polarity choice is irrelevant for composition is now proven by simply pasting the two diagrams (so long as the reader can assure themselves that they commute in the first place), for example.

Next Steps

Beyond more editing and writing, I plan to try upstreaming my work to UniMath, cleaning things up on the way. One thing that bugs me is that I use a⁺ in the code for what I have written as \(\mathop{\pi^\oplus}{a}\) in \(\LaTeX\). It is also subject to a million coercion and unification issues. I plan to fix this problem and others like it.

Towards a Rezk Completion for Unital Magmoids

As I was pondering how to motivate linear-and-thunkable-and-intermediate isomorphisms for unital magmoids, what came to mind was the hypothetical eliminator for a higher-inductive Rezk completion of Unital Magmoids. What I am thinking is that the HIT eliminator would of course need all of the properties of the isomorphism in order to define hom-sets, composition, etc. I wrestled Nix to get the 1lab compiling on my machine, and could even get Emacs working. So maybe I will have a HIT Rezk completion for unital magmoids at some point.

More interestingly for book HoTT fans, I was wondering if the presheaf-based Rezk completion of categories could satisfy a HIT-like eliminator, even if not definitionally. This would no doubt be miserable to work with, but could be fun to try. Eliminating from propositional truncation into groupoids is a massive pain, but it can be done. I have a non-dependent eliminator implemented, available on request:

Context (A : category).
Let ℜA := Rezk_completion_univalent_category A.

Definition rezk_completion_rec
  (B : UU)
  (isg : isofhlevel 3 B)
  (incl : A -> B)
  (glue : ∏ (a b : A) (p : z_iso a b), incl a = incl b)
  (coh : ∏ (a b c : A) (p : z_iso a b) (q : z_iso b c),
      glue a b p @ glue b c q = glue a c (z_iso_comp p q))
  : ℜA -> B.

Updated: