March Update 2
This week my most critical obligation is to organise my writings into a more dissertation-like format than this blog. Although the Rezk completion and 2-categories of duploids and adjunctions hang in the back of my mind, the complexities of formalising those thankfully keep me away from at least one proof assistant. I will start with an update on the dissertation text, and end with some thoughts I have had (despite my best efforts) about the outstanding technical problems.
A Plan?
Although I certainly have a great deal of technical content written down already in this blog, I found myself missing an essential organisational component for my dissertation: a gripping narrative. By which I mean of course a natural thread of exposition, logic, and motivation leading each thought to the next. Unfortunately such narratives scarcely grow on trees, so home-made will have to do. Let me start by detailing the important ingredients, the characters and plot points if you will, that I believe this narrative might need to include. These are in note format rather than prose, because they are, in fact, lifted from my running notes.
- Results to Include
- I have formalized a substantial portion of the existing theory of
single-sorted duploids.
- I got through most of Guillaume’s thesis’ duploids chapter
[1], up to proving that every duploid arises from
an adjunction.
- As mentioned in a footnote last week, the rest of the chapter apparently weakens, in the single-sorted case, to a statement about the 2-categories of adjunctions and duploids, so this is at the very least an appropriate place to end up.
- The equivalence of the definition of shifts that I have given to the universal property definition of shifts written down by Mangel et al. [2] is a proof that I have not yet seen written down elsewhere, even if it no doubt exists in the minds of all who have cared to look at it.
- I got through most of Guillaume’s thesis’ duploids chapter
[1], up to proving that every duploid arises from
an adjunction.
- I have also formalized a few results that are novel.
- I defined univalence for duploids (as univalence of its
linear-and-thunkable subcategory), and showed that it is
equivalent to univalence of its negative-linear and
positive-thunkable subcategories separately, which is cool and
nontrivial.
- This is specifically in the single-sorted case, with those subcategories having polarity defined semantically. In the two-sorted case, univalence of the syntactically-positive-thunkable and syntactically-negative-linear categories would probably be the definition of univalence, as per Ahrens et al. [3].
- I proved that having shifts becomes a property in a univalent duploid.
- The “envelope duploid” I constructed is a homotopy-type-theoretically well-behaved definition for the single-sorted duploid arising from an adjunction, which ends up being weakly equivalent to the “oblique duploid” constructed in Guillaume’s thesis, and strongly equivalent with only LEM.
- I gave an alternative definition for the equalizing requirement in terms of the inclusion functors into the envelope duploid.
- I proved univalence of the envelope duploid when its constituent categories are univalent and the adjunction is fully equalizing. This will likely the “main result” of my dissertation, at least unless my dreams from the second part of this post come true.
- I defined univalence for duploids (as univalence of its
linear-and-thunkable subcategory), and showed that it is
equivalent to univalence of its negative-linear and
positive-thunkable subcategories separately, which is cool and
nontrivial.
- I have formalized a substantial portion of the existing theory of
single-sorted duploids.
- Topics and Potential (?) Order
- I ought to mention how non-associative computation arises. Even if not the main focus of my work (which is in fact literally just maths), it will be good motivation for dropping the associativity law from categories.
- This would lead into non-associative categories, aka unital
magmoids.
- I am not sure how much to dwell on the distinction between “precategories” and “categories” and “unital premagmoids” and “unital magmoids” where the difference is that the latters’ hom-types are sets. We do not actually care about unital magmoids enriched in higher groupoids in this work, and it is likely that we would prefer to explore duploids enriched in different ways instead anyway e.g. in presheaves. Thus it seems like it would be a good idea to ignore it and ask for us to have sets from the start, at least for the dissertation text.
- From here we can introduce the extra structure (which eventually
turns out not to be structure at all) of a (pre)duploid on top of
a unital magmoid. This will be the definitions that I use in the
formalization, but I should make reference to the universal
property definitions and mention that they are equivalent.
- It will probably be nice to note observations about linear/thunkable/linear-and-thunkable isomorphisms here, or just before. An important lemma that fails for unital magmoids but works for preduploids is that linear-and-thunkable isomorphisms associate in the middle.
- In fact, it is likely that the definition of duploids can come before most of the lemmas which do generalize to unital magmoids. This is mostly because unital magmoids are awful while duploids have just enough properties to be acceptable.
- A motivating point for duploids is that they correspond to some
subcategory of the adjunctions, so we should likely introduce the
ordinary construction of the oblique duploid around here.
- This can involve looking at the “collage category,” which is literally just the oblique duploid but omitting the offending non-associative morphisms. We then add back those morphisms to obtain the oblique duploid.
- I can discuss the univalence condition, how it arises, and how my
hangups about linear-and-thunkable isomorphisms might make it fail
for unital magmoids.
- We can then easily see that the oblique duploid fails to be univalent as a single-sorted duploid.
- We can then look at the envelope duploid, which I promise behaves
better than the oblique duploid.
- We can appeal to the construction of the oblique duploid earlier: in the collage category, objects are literally from either \(\acat{P}\) or \(\acat{N}\) and are automatically equipped with an oblique morphism (that is the identity in one of the categories), but if we weaken the identity to any inverse for the oblique morphism and propositionally truncate it away, that is how we get the envelope duploid.
I have also rewritten some definitions and theorems in my notes, particular earlier ones from this blog, so that they adhere to the conventions I intend to use. I will make the text of my dissertation available online as it takes shape.
The 2-Category of Adjunctions
I have found what I believe to be a delightfully pragmatic definition for the bicategory of adjunctions as a pseudofunctor category.
Definition 1. The walking adjunction \(\WAdj\) is the bicategory freely generated by an internal adjunction \(\ttL \dashv_{(\tteta,\tteps)} \ttR : \ttN \to \ttP\) (so that its 0-cells are \(\ttN\) and \(\ttP\), 1-cells the identities, \(\ttL\), \(\ttR\) and their composites, and 2-cells include \(\tteta\) and \(\tteps\), satisfying the snake equations). Given a strict 2-category \(\C\)1, the (strict) pseudofunctor bicategory \([\WAdj, \C]\) can be characterized in the following way.
- The 0-cells \(A : [\WAdj, \C]\) are given by adjunctions \(A\ttL \dashv_{(A\tteta,A\tteps)} A\ttR : A\ttP \to A\ttN\) internal to \(\C\). Note that e.g. \(A\tteta\) is the \(\C\)-2-cell that \(A\) maps \(\tteta\) to, rather than the ill-typed reading “\(A\) whiskered with \(\eta\)”.
-
The 1-cells \(A \xrightarrow{\sigma} B\) are given by pairs of \(\C\)-1-cells \[\begin{gathered}A\ttP \xrightarrow{\sigma_\ttP} B\ttP \\ A\ttN \xrightarrow{\sigma_\ttN} B\ttN\end{gathered}\] along with a pair of invertible “pseudonaturality” \(\C\)-2-cells \(\sigma_\ttL\) and \(\sigma_\ttR\) as depicted below, up to which \(\sigma\) preserves the unit and counit.
Let me write vertical composition of 2-cells as \(\bullet\) (in diagrammatic order), and whiskering with a triangle \(\triangleright\) whose point faces the lower-dimensional cell. The requirement is \[\begin{aligned} A\tteta \triangleright \sigma_\ttP &= (\sigma_\ttP \triangleleft B\tteta) \bullet (\sigma_\ttR \triangleright B\ttL) \bullet (A\ttR \triangleleft \sigma_\ttL) \\ \sigma_\ttN \triangleleft B\tteps &= (\sigma_\ttL \triangleright B\ttR) \bullet (A\ttL \triangleleft \sigma_\ttR) \bullet (A\tteps \triangleright \sigma_\ttN)\,.\end{aligned}\]
- The 2-cells \(\sigma \xRightarrow{m} \tau\) are pairs of \(\C\)-2-cells \[\sigma_\ttN \xRightarrow{m_\ttN} \tau_\ttN \qquad \sigma_\ttP \xRightarrow{m_\ttP} \tau_\ttP\] such that they commute with \(\sigma\) and \(\tau\) as follows \[\begin{aligned} \sigma_\ttL \bullet (A\ttL \triangleleft m_\ttP) &= (m_\ttN \triangleright B\ttL) \bullet \tau_\ttL \\ \sigma_\ttR \bullet (A\ttR \triangleleft m_\ttN) &= (m_\ttP \triangleright B\ttR) \bullet \tau_\ttR\,. \end{aligned}\]
The 1-cells appear to be the same as the pseudo-maps of adjunctions as defined by Jacobs [4] (Def. 3.2) and used in Guillaume’s thesis [1], but generalized to \(\C\), which justifies the use of this bicategory of adjunctions. They look similar modulo superficial differences in variable names and written composition order, but I have managed to clear the low bar of convincing myself that they really are the same (my scribbles and string diagrams are at https://beta.homotopy.io/p/2603.00001 2 – we even get cool 3D graphical interpretations for the equations!) The 1-cells more clearly coincide with MacLane’s [5] (Ch. IV. Sec. 7) transformations of adjoints when \(\sigma_\ttL\) and \(\sigma_\ttR\) are the identities.
An idea is that it may be possible to define the equalizing requirement “categorically” within \([\WAdj, \C]\), such as by asking some 1-cells to take part in an adjoint equivalence. This may involve the (trivial) positive and negative adjunctions as defined below, but I do not wish to dwell on it too much.
Example 2. Given a 2-category \(\C\) and an adjunction \(A : [\WAdj, \C]\), define the positive adjunction \[A^\ttP \triangleq \WAdj \xrightarrow{!} 1 \xrightarrow{\ttP} \WAdj \xrightarrow{A} \C\] and the negative adjunction \[A^\ttN \triangleq \WAdj \xrightarrow{!} 1 \xrightarrow{\ttN} \WAdj \xrightarrow{A} \C\] as the corresponding constant functors. That is, the identity adjunctions on \(A\ttP\) and \(A\ttN\) respectively.
I conjecture that (possibly only considering \(\C \in \{\Cat, \UnivCat\}\) or other nice bicategory) we can take the “center/fixed point” of the adjunction \(A\), say \(\mathrm{Inv}(A)\), and obtain “projections” \(\mathrm{Inv}(A) \xrightarrow{\pi^\ttP} A^\ttP\) and \(\mathrm{Inv}(A) \xrightarrow{\pi^\ttN} A^\ttN\). Then we ought to be able to obtain “injections” \(A^\ttP \xrightarrow{\iota^\ttP} A\) and \(A^\ttN \xrightarrow{\iota^\ttN} A\) whenever \(A\) is fully equalizing, such that the square \(\pi^\ttN \cdot \iota^\ttN = \pi^\ttP \cdot \iota^\ttP\) at the very least commutes, if it is not also a 2-pullback or even 2-pushout. My reasoning is by reference to the envelope duploid. The “projections” surely ought to exist, since \(\mathrm{Inv}(A)\) ought to essentially be the full subobject (imagine subcategory) in \(\C\) of \(A\ttP\) or equivalently \(A\ttN\) on which \(A\) as an adjunction restricts to an adjoint equivalence. The injections \(\iota^\ttP/\iota^\ttN\) also ought to exist by reference to the envelope duploid on which they are easily defined.
The dream is that we can consider the (not-yet-fully-defined) envelope-duploid functor \([\WAdj, \Cat] \xrightarrow{\acat{E}} \Dupl\) and the (equally not-yet-fully-defined) duploid-upshift-downshift-adjunction functor \(\Dupl \xrightarrow{\upshift \dashv \downshift} [\WAdj, \Cat]\), (co)restrict them to the full subcategory of fully equalizing adjunctions \([\WAdj, \Cat]_\eq\) (this category we are perfectly able to define even today) and to univalent categories/duploids, and obtain the following diagram of bicategories and pseudofunctors.
Our Rezk completion of duploids \(\Rezk^\Dupl\) is then simply the line of pseudofunctors at the top. All of these pseudofunctors bar \(- \cdot\Rezk^\Cat\) should be well-defined on 0-cells and possibly even 1-cells today, by Guillaume’s thesis, with the only interesting outstanding proof obligation being that postcomposition with \(\Rezk^\Cat\) preserves the equalizing requirement (surely there is no way it does not). How to prove that this ends up being weakly equivalent to the original duploid is another question – maybe it is enough to prove that the pseudofunctor is a left-adjoint?
References
Footnotes
1 We will only care about \(\Cat\) and \(\UnivCat\) for the moment, so strict is fine.
2 I actually used my fork that basically adds copy+paste, hosted at https://homotopy.io.eutro.dev/.