May Update 2

This past week I made a great deal of progress on writing. The new version is up on my notes site. Notably, I reorganized the Unital Magmoids chapter to include the definition of categories (and hence its generalizations more closely), added most definitions to the Duploids chapter, and wrote most of the definitions for the “Adjunctions and Duploids” chapter, which includes definitions of the oblique and envelope duploids. I have also made some minor stylistic and notational changes.

I still have to write about the equalizing requirement, and how it makes the envelope duploid univalent; and the oblique duploid, when univalence is defined to include the polarization choice structure (see is_univalent_split_oblique_duploid). My remaining results are then the weak equivalence of each duploid to the envelope duploid on its shifts (weak_dupoid_equivalence_duploid_to_envelope_on_shifts), my beautiful 2-categorical UniMath formalization that adjunctions are preserved by pseudofunctors (map_left_adjoint_axioms), and then a handwave hint at the Rezk completion which is ever too painful to actually formalize. I also might have a handful of theorems missing here and there, and some of the existing ones are just tedious computations that have been evading nicer proofs than “Proof. This computation is an exercise for the reader. \(\square\)” It is the primary benefit of Rocq that I can do like induction x, y, z; reflexivity. and eat through a bunch of tedious cases…

Outside of technical results to write down, I have a great deal of prose (outline, conclusions, related work, future work, etc.) and exposition to write, and yet I am running out of space. In the next week or so I shall have to tackle these more seriously, now that most of the technical content is written up.