9 minute read

This week I made some progress on defining a truly single-sorted duploid from an adjunction, which does not need use a coproduct for the structure of the objects. Although I don’t believe this quite yields a univalent construction just yet, it feels like a more natural single-sorted duploid where there is at least some hope of identifying indistinguishable objects.

The Single-Sorted Duploid arising from an Adjunction

Definition 1. Given an adjunction \(L \dashv R : \acat{N} \to \acat{P}\), the oblique morphisms from \(p : \acat{P}\) to \(n : \acat{N}\), written \(\morsof{\acat{O}_{L \dashv R}}{p}{n}\), are defined as \(\morsof{\acat{N}}{L p}{n}\). They may equally be considered as morphisms \(\morsof{\acat{P}}{p}{R n}\) by taking the transpose in the adjunction. Where the adjunction is obvious I will freely omit it from \(\acat{O}\), and transpositions may be elided so that a morphism \(\morsof{\acat{O}}{p}{n}\) may equally be considered a morphism in \(\acat{N}\) or \(\acat{P}\).

Definition 2. Given an adjunction \(L \dashv R : \acat{N} \to \acat{P}\) the oblique duploid over \(L \dashv R\), written \(\acat{O}[L \dashv R]\) is the standard split duploid arising from the adjunction, with objects either positive objects \(p : \acat{P}\) or negative objects \(n : \acat{N}\).

Defining the operators \((-)^\oplus : \acat{O}[L \dashv R] \to \acat{P}\) and \((-)^\ominus : \acat{O}[L \dashv R] \to \acat{N}\) as below, the morphisms are given by \(\morsof{\acat{O}[L \dashv R]}{a}{b} \triangleq \morsof{\acat{O}_{L \dashv R}}{a^\oplus}{b^\ominus}\).

\[\begin{align*} (p : \acat{P})^\oplus &\triangleq p & (n : \acat{N})^\oplus &\triangleq Rn \\ (p : \acat{P})^\ominus &\triangleq Lp & (n : \acat{N})^\ominus &\triangleq n\end{align*}\]

PermalinkDefinition 3. Given an adjunction \(L \dashv R : \acat{N} \to \acat{P}\) the split envelope duploid over \(L \dashv R\), written \(\acat{E}[L \dashv R]^*\) is given by objects of the form \((p : \acat{P}, n : \acat{N}, \alpha : \morsof{\acat{O}}{p}{n})\) along with for each object a choice of inverse witnessing that \(\alpha\) is an isomorphism either in \(\acat{N}\) or \(\acat{P}\). That is, the inverse provides that \(\alpha\) witnesses one of \(p \cong Rn : \acat{P}\) or \(Lp \cong n : \acat{N}\). Morphisms are defined by \(\morsof{[L \dashv R]^*}{(p,n,\alpha)}{(q,m,\beta)} = \morsof{\acat{O}}{p}{m}\).

Composition of \((p,n,\alpha) \xrightarrow{f} (q,m,\beta) \xrightarrow{g} (r,o,\gamma)\), as depicted in the following diagram, is given by composing with \(\beta^{-1}\) in the middle in either \(\acat{N}\) or \(\acat{P}\) depending on the choice of inverse.

The rest of the data, and the fact that this gives a well-defined split duploid, is found here as an exercise for the Rocq kernel1.

The fact that the inverse must be a choice for each object makes this definition necessarily “split”, in that if both inverses exist, the choice of inverse would prevent identification of two objects that are otherwise the same. However, when an object’s oblique morphism has inverses in both \(\acat{N}\) and \(\acat{P}\) then that object is in the fixed point of the adjunction, and it turns out that the choice of inverse becomes irrelevant.

Theorem 4. Given an adjunction \(L \dashv R : \acat{N} \to \acat{P}\), let \(f\) and \(g\) be two morphisms \((p,n,\alpha) \xrightarrow{f} (q,m,\beta) \xrightarrow{g} (r,o,\gamma)\) in \(\acat{E}[L \dashv R]^*\). When \(\beta\) is an isomorphism in both \(\acat{N}\) and \(\acat{P}\), the two possible compositions of \(f \cdot g\) in \(\acat{E}[L \dashv R]^*\) coincide.

Proof. Pinky promise.

\(\square\)

This justifies the following definition.

PermalinkDefinition 5. Given an adjunction \(L \dashv R : \acat{N} \to \acat{P}\), the (single-sorted) envelope duploid, written \(\acat{E}[L \dashv R]\), is given by the same data as the split envelope duploid, but the choice of inverse is truncated to a proposition and eliminated using the theorem above.

Theorem 6. The envelope duploid arising from an adjunction \(L \dashv R : \acat{N} \to \acat{P}\) is weakly equivalent to the oblique duploid, in that there is a fully-faithful functor \(F : \acat{O}[L \dashv R] \to \acat{E}[L \dashv R]\) which is (merely) surjective up to linear and thunkable isomorphism. With the law of the excluded middle, the surjection can be upgraded to a split one.

Proof. The functor is defined on objects as below.

\[\begin{align*} F(p : \acat{P}) &\triangleq (p,Lp,\id_{Lp} : \morsof{\acat{N}}{Lp}{Lp}) \\ F(n : \acat{N}) &\triangleq (Rn,n,\id_{Rn} : \morsof{\acat{P}}{Rn}{Rn}) \end{align*}\]

In the image of \(F\), the homsets of \(\acat{O}[L \dashv R]\) and \(\acat{E}[L \dashv R]\) are identical, and so \(F\) is the identity on morphisms and trivially fully faithful.

For the surjection, fix an object \((p,n,\alpha) : \acat{E}[L \dashv R]\). If \((p,n,\alpha)\) is positive, then \(p : \acat{O}[L \dashv R]\) has \(F(p) \stackrel{\text{def}}{\equiv} (p,Lp,\id_{Lp}) \stackrel{\text{def}}{\equiv} \downshift(p,n,\alpha) \stackrel{\unwrap}{\cong} (p,n,\alpha)\),2 and dually if negative.

Without LEM the decision of whether the object is positive or negative must be done under the propositional truncation, hence the surjection is merely inhabited. With LEM however, we can always “decide” arbitrarily for positive-and-negative objects to take the negative inverse.

\(\square\)

Thoughts (Unstructured)

  • The construction above is in part thanks to Jem suggesting that positive-and-negative objects may be related to the fixed points of the adjunctions (those where \(\varepsilon_n\) or \(\eta_p\) are isomorphisms). They don’t seem to be quite the same. Positive-and-negative objects in the oblique duploid are characterised by having either \(LR\varepsilon_n = \varepsilon LR_n\) or \(RL \eta_p = \eta RL_p\), which appears to be weaker than \(\varepsilon_n\) or \(\eta_p\) being isomorphisms. This has the effect that in the envelope duploid, merely being positive or being negative does not appear to give rise to the associated choice of inverse. If nothing else, this shoots down univalence of the envelope duploid, but it does suggest what a univalent construction might need to look like.

    The “envelope duploid” name I have used is tentative, which I gave after the “envelope (category) of an adjunction”, but I do not know if it actually resembles anything else that category theorists might call envelopes. Based on a somewhat hand-wavy idea of what a pullback is, I guess that the fixed point of the adjunction might be a pullback in \(\wkcat{Dupl}\) of the diagram \(\acat{P} \hookrightarrow \acat{E}[L \dashv R] \hookleftarrow \acat{N}\) (or equivalently \(\acat{P} \hookrightarrow \acat{O}[L \dashv R] \hookleftarrow \acat{N}\)), similarly to the envelope category.

  • In a (pre)duploid, being surjective up to linear-and-thunkable isomorphism is sufficient to preserve polarities, so the functor above is automatically a duploid functor.

    While formalising this I realised that being only linear-and-thunkable isomorphism might actually be too weak in a unital magmoid! In particular, a linear-and-thunkable isomorphism \(g\) does not appear to make triples of the form \(a \xrightarrow{f} b \xrightarrow{g} c \xrightarrow{h} d\) associate within a unital magmoid, which I thought they did. This is not a problem in a preduploid: \(b\) and \(c\) obtain the same polarity from having a linear-and-thunkable isomorphism between them and so the triple associates from that.

  • There have been rumours of \(\wkcat{Dupl}\) and \(\wkcat{Adj}\) being 2-categories. In [1], the former is defined with duploid functors and linear-and-thunkable natural transformations. Another text, that I have since lost, helpfully defined the 2-cells of the latter as “the obvious ones.” In any case, I do believe the linear-and-thunkable natural transformations might form 2-cells in the category \(\wkcat{UMgmd}\) of unital magmoids and their functors, although I wonder how commonly those linear-and-thunkable natural transformations might actually arise.

  • I don’t think I will be returning to the theory of unital magmoids for the time being, not least because they are far too unsatisfying. If category theory “has no theorems” because they are so trivial, then unital magmoids are devoid of theorems for the opposite reason. This is probably an opportunity to properly write up the important lemmas about unital magmoids into what will become the actual text of my dissertation.

  • I think I have come to a resolution for my worries about split vs. single-sorted duploids. I was especially worried about the “positive-as-a-property” subcategory and the “chosen-positive” subcategory (that with objects taken to \(\oplus\) by the polarity mapping) of a split duploid might not be the same, since the former could have “more objects,” the ones mapped to \(\ominus\) that happen to be positive nonetheless. But here is an informal proof that the two categories are equivalent.

    Proof. Let \(\D\) be a duploid, \(\Cp\D\) is its positive subcategory, and let the chosen-positive category \(\Cp{\D\omega}\) of the split duploid \(\D\) with polarity mapping \(\omega\) be the full subcategory of \(\Cp\D\) where objects \(a : \Cp\D\) have \(\omega(a) = \oplus\). Then the fully-faithful inclusion functor \(I : \Cp{\D\omega} \hookrightarrow \Cp\D\) is split-essentially-surjective on objects with inverse given by \((a : \Cp\D) \mapsto (\downshift a : \Cp{\D\omega})\), for which we have the linear-and-thunkable isomorphism \(\wrap : a \cong \downshift a : \Cp{\D\omega}\). The same proof works for \(\Cpt\D\) and \(\Cpt{\D\omega}\), and dually for the negative variants.

    \(\square\)

Next Steps

  • I am, surprisingly, largely on schedule for the (super secret) work plan submitted as part of the phase 2 proposal. I have spent more time on original constructions and theorems, and less on existing results, than I had written down, but I do not believe this is a problem in any way. I wrote down, due Feb. 2, the sensibly vague “Milestone: mechanised proofs from literature,” which I guess is certainly something that I have done by now.

    The next work block includes “Exploration of univalence and its consequences,” which happens to be exactly the thing I would like to start doing. Looking forward I even have “Ensure existing proofs are written up in dissertation” written down for two weeks from now, which is something I am also planning on. I am impressed by how sensible the me of November was.

  • I do wonder how easy it would be to glue on co/algebras onto the envelope duploid. One idea I had was for \((p,n,\alpha) : \acat{E}[L \dashv R]\) to always have morphisms \(Rn \to p\) and \(n \to Lp\) that are at least retractions or sections to \(\alpha\) in the appropriate category, so that they satisfy the unit law of a monad algebra in the upshift/downshift cases \((p,Lp,\id_{Lp})\) and \((Rn,n,\id_{Rn})\). Then all we have to do is find the right morphisms and just add enough equations to make it restrict to the appropriate (co)Kleisli category if we take the positive and negative subcategories! What could go wrong?

  • I am going to have to explore univalence for duploids, oh dear. I have a feeling it might be very grim to prove these structures univalent, since I’m not sure if displayed unital magmoids are going to help me much when the base unital magmoid can’t be univalent. It might help to develop some theory of displayed reflexive graphs in UniMath , or maybe just to build entire displayed categories? Seems like a lot of work. Maybe I will look around for how other parts of UniMath are doing it, or get over my fear of talking to people ask around, or just suffer through a handful of transports.

  • I still have as outstanding work to write satisfying proofs for the adjunctions within a duploid, and the crucial equivalence \(\acat{O}[\upshift \dashv \downshift : \Cnl\D \to \Cpt\D] \cong \D\) for a duploid \(\D\). If I can get a univalent construction for (another duploid equivalent to) \(\acat{O}[\upshift \dashv \downshift]\) then it might be worth holding off with that until I do.

This update turned out a little longer than I expected it to be! I am getting started on writing these notes (or at least the technical content) such that they might be more easily copyable into the text of my dissertation. So now my markup also includes some hacked-together amsthm environments. Great. I hope they look nice?

References

[1]
É. Mangel, P.-A. Melliès, and G. Munch-Maccagnoni, “Classical notions of computation and the Hasegawa-Thielecke theorem,” Proc. acm program. lang., vol. 10, no. POPL, Jan. 2026, doi: 10.1145/3776715.

Footnotes

1 I actually went straight to defining the single-sorted variant.

2 Surprise! This is the definition of upshift.

Updated: