July Update 2

This week I spent more time bashing my head against UniMath’s bicategories. This has resulted in me proving 2.5 more coherence laws for the pseudofunctor-from-left-universal-arrows, leaving only 1.5 more to go. Mind, the computationally relevant data of the pseudofunctor is already well-defined, so this grunt work is unnecessary if my interest is in using Rocq as a blackboard¹.

A 2-categorical way to define the equalizing requirement is helpful for studying adjunctions and their relation to duploids. Every adjunction \(L \dashv R : \NN \to \PP\) gives rise to a comparison functor \(K^{RL} \colon \NN \to \PP^{RL}\) to the Eilenberg-Moore category of the monad \(RL\). It is known that an adjunction is negative equalizing if and only if \(K^{RL}\) is fully-faithful, and I have now proven this in UniMath. Likewise, this can be dualized to comonads for the positive side. This functor and its fully-faithfulness can both be expressed 2-categorically, which (I hope) will be easier to work with for the 2-categorically-defined image-of-an-adjunction-in-a-pseudofunctor.

It is clear that the 2-categorical Rezk completion via adjunctions and the envelope duploid still has lots of work to be done. Given this, I may take a fresh stab at defining a Rezk completion of duploids directly. Such a construction may provide more insight anyhow, and it will force me to refactor some existing code too (e.g. the cursed Yoneda stuff).

Footnotes

¹ Someone else proved these theorems on paper for 2-categories so it must be true! I can safely use admit, right?