3 minute read

These past few weeks I have spent some time working on the Rezk completion for duploids. Otherwise, I would like to collect my thoughts on what I wish to do, now that I have submitted the final version of the part III project and graduated.

I intend to write a post here presenting the final version of my dissertation,1 but that is not yet written. In the meantime, please find it at https://notes.eutro.dev/cs/diss/output/writeup.pdf2

Future Work

These are some ideas for what I could do going forward. This also serves as a reminder of what my unfinished/future work was, and the progress I made on them nevertheless.

  • Clean up of my UniMath fork, for niceness and potential upstreaming. This involves:
    • Cleaning up existing code. (e.g. exploring nice abstractions for “wide subcategories” of morphisms, moving things around.)
    • Clean up my commit history. (e.g. hoist commits for reflexive graphs.)
  • Refine the text of my dissertation into a potential publication.
  • Explore the 2-category of duploids and duploid functors.
    • Explore their relationship with the 2-category (or categories) of adjunctions.
    • (We can work with the functors and natural transformations unbundled if necessary, especially if defining the 2-categories is too annoying.)
  • Explore the envelope-duploid Rezk completion of duploids. One path (as I mentioned in March) may be:
    • Defining the action of a pseudofunctor on an adjunction.
    • Defining a pseudofunctor from a “left universal arrow”
      • …which would give us a Rezk completion pseudofunctor \(\UnivCat \to \Cat\).
      • This should be possible following Fiore [1]. (The proof also includes that it is a left biadjoint, but we shall see if that ends up being necessary.)
    • Showing that the Rezk completion pseudofunctor preserves the equalizing requirement.
      • There ought to be a 2-categorical way to show this, which might make things easier. (Although it might also require more effort than it is worth.)
    • Showing that the resulting duploid is equivalent to the original
      • It may be worth exploring the 2-category of duploids and adjunctions more first.

Progress

I have made some progress formalizing the pseudofunctor from a left universal arrow of 2-categories.

Definition 1. Let \(R : \C \to \D\) be a pseudofunctor. A left universal arrow \((L_0x, \eta_x)\) from \(x : \D\) to \(R\) consists of:

  • An object \(L_0x : \C\).
  • A 1-cell \(x \xrightarrow{\eta_x} RL_0x\).
  • These must satisfy that, for each \(y : \C\), the following functor is an adjoint equivalence: \[\begin{aligned} \varphi_y &: \morsof\C{L_0x}{y} \to \morsof\D{x}{Ry} \\ \varphi_y\left(L_0x \xrightarrow{g} y\right) &\defequiv \left(x \xrightarrow{\eta_x} RL_0x \xrightarrow{Rg} Ry\right) \\ \varphi_y\left(f \xRightarrow{\nu} g\right) &\defequiv \left(\eta_x \mathop; Rf \xRightarrow{\eta_x \triangleleft R\nu} \eta_x \mathop; Rg\right) \end{aligned}\]

Proposition 2. A family \((L_0x, \eta_x)_{x : \D}\) of left universal arrows to \(R : \C \to \D\) assembles into a pseudofunctor \(L : \D \to \C\).

The proof of Thomas Fiore’s Theorem 9.17 [1] should somewhat be usable. However, it is complicated by UniMath using weak 2-categories (i.e. bicategories) rather than strict 2-categories as Fiore does.

I am… getting through it. I have got the data of the pseudofunctor, have proven that its identitor and compositor are invertible, and have proven a couple easier laws. It remains to prove the more difficult laws, for which I’m better served by some pen-on-paper diagram chasing than by the proof assistant.

References

[1]
T. M. Fiore, “Pseudo limits, biadjoints, and pseudo algebras: categorical foundations of conformal field theory,” Memoirs of the AMS, vol. 182, no. 860, 2006, doi: 10.1090/memo/0860. [Online]. Available: https://www.ams.org/memo/0860. [Accessed: Jul. 13, 2026]

Footnotes

1 Sorry, “part III project”.

2 The newest version of writeup.pdf is a different rendering to that submitted for marking. It links directly to GitHub for source links. The links from the submitted rendering claim to redirect, but they do not.

Updated: