March Update 1
This week we resolved my issues from last week about the equalizing requirement for the upshift-downshift adjunction of a duploid. I briefly considered how to construct a Rezk completion from this, which turns out to be rather nontrivial. I include my not-yet-mechanized thoughts on this below.
The Upshift-Downshift Adjunction is Fully Equalizing
Given a duploid \(\D\), there is an adjunction \(\upshift \dashv \downshift : \Cnl\D \to \Cpt\D\), of which last week I struggled to prove the equalizing requirement. Given also the rich variety of more pressing things I have to do this week and in the near future, and the fact that it is not my own proof but one of Guillaume’s that I had failed to mechanize, I washed my hands of the issue. Fortunately there was no problem with the truth of the statement itself, as I received independently a complete proof from Jon and a less detailed rendition of a similar proof from Guillaume later. I reproduce below the mechanized proof I ended up using.
Lemma 1. Given an adjunction \(L \dashv R : \acat{P} \to \acat{N}\), the following are equivalent.
- \(L \dashv R\) satisfies the negative equalizing requirement.
- The inclusion functor \(\iota^\ominus : \acat{N} \to \Cnl{\acat{E}[L \dashv R]}\) is fully faithful.
- The inclusion functor \(\iota^\ominus : \acat{N} \to \Cnl{\acat{E}[L \dashv R]}\) is a (strong) equivalence of categories.
- For any objects \(n, m : \acat{N}\) and morphism \(f : LRn \to m\) satisfying \(LR\epsilon_n \cdot f = \epsilon_{LRn} \cdot f\), there is a unique morphism \(f’ : n \to m\) such that \(\epsilon_n \cdot f’ = f\).
- Both of the following statements.
- \(R\) is faithful. Equivalently, for all \(n : \acat{N}\), \(\epsilon_n\) is an epimorphism.
- For all \(n, m : \acat{N}\) and \(f : \morsof{\acat{O}}{R n}{m}\) satisfying \(LR\epsilon_n \cdot f^\flat = \epsilon_{LRn} \cdot f^\flat\), there exists \(f’ : n \to m\) such that \(\epsilon_n \cdot f’ = f^\flat\) or equivalently \(Rf’ = f^\sharp\).
Proof. \((1 \leftrightarrow 2)\) By definition.
\((3 \to 2)\) Equivalences are fully faithful, and \((2 \to 3)\) the inclusion functor \(\iota^\ominus\) is always essentially surjective on objects.
\((5 \leftrightarrow 4)\) The faithful/epimorphism equivalence of \((5.1)\) is textbook (Riehl, “Category Theory in Context” Ch. 4). For \((5.2)\) we have that \(\epsilon_n \cdot f’\) and \(Rf’\) are mates, as are \(f^\flat\) and \(f^\sharp\). Ultimately, it is easy to see that \((5.2)\) is equivalent to the existence part of \((4)\) and hence that \((5.1)\) is equivalent to the uniqueness part of \((4)\).
\((4 \leftrightarrow 2)\) First, note that morphisms \[f : LRn \to m\] and morphisms \[f^{\flat^{-1}} : \morsof{\Cn{\acat{E}[L \dashv R]}}{\iota^\ominus(n)}{\iota^\ominus(m)}\] are equivalent by \(\flat\), and that \[LR\epsilon_n \cdot f = \epsilon_{LRn} \cdot f\] is equivalent to \(f^{\flat^{-1}}\) being linear in \(\acat{E}[L \dashv R]\) by [the characterization lemma I haven’t written]. Note also that by definition, a functor is fully faithful if its action on morphisms is (pointwise) a weak equivalence of homsets. Thus it remains to check that \[\exists! (f’ : n \to m), \epsilon_n \cdot f’ = f\] is equivalent to the fiber \[\orgcode{fib}_{\lambda (f’ : n \to m). \iota^\ominus(f’)}(f^{\flat^{-1}})\] being contractible. Indeed we have \[\begin{aligned} \orgcode{iscontr}(\orgcode{fib}_{\lambda f’. \iota^\ominus(f’)}(f^{\flat^{-1}})) &\equiv \exists! (f’ : n \to m), \iota^\ominus(f’) = f^{\flat^{-1}} \\ &\stackrel{\flat}{\simeq} \exists! (f’ : n \to m), \iota^\ominus(f’)^\flat = f \\ &\equiv \exists! (f’ : n \to m), \epsilon_n \cdot f’ = f\,, \end{aligned}\] which is the same.
I am nice, so here is the dualization of the previous statement.
Corollary 2. Given an adjunction \(L \dashv R : \acat{P} \to \acat{N}\), the following are equivalent.
- \(L \dashv R\) satisfies the positive equalizing requirement.
- The inclusion functor \(\iota^\oplus : \acat{P} \to \Cpt{\acat{E}[L \dashv R]}\) is fully faithful.
- The inclusion functor \(\iota^\oplus : \acat{P} \to \Cpt{\acat{E}[L \dashv R]}\) is a (strong) equivalence of categories.
- For any objects \(p, q : \acat{P}\) and morphism \(f : p \to RLq\) satisfying \(f \cdot RL\eta_q = f \cdot \eta_{RLq}\), there is a unique morphism \(f’ : p \to q\) such that \(f’ \cdot \eta_q = f\).
- Both of the following statements.
- \(L\) is faithful. Equivalently, for all \(p : \acat{P}\), \(\eta_p\) is a monomorphism.
- For all \(p, q : \acat{P}\) and \(f : \morsof{\acat{O}}{p}{Lq}\) satisfying \(f^\sharp \cdot RL\eta_q = f^\sharp \cdot \eta_{RLq}\), there exists \(f’ : p \to q\) such that \(f’ \cdot \eta_n = f^\sharp\) or equivalently \(Lf’ = f^\flat\).
Proof. Dual to the previous lemma, thanks to the symmetry of my definition of oblique morphisms 😌.
I move on to prove the (negative) equalizing requirement for \(\upshift \dashv \downshift\).
Lemma 3. Let \(\D\) be a duploid, the counit of the adjunction \(\upshift \dashv \downshift : \Cnl\D \to \Cpt\D\), given by \(\epsilon_a = \force_{\downshift a} \cdot \unwrap_a\) has a pointwise thunkable section \(\nu_a : \wrap_a \cdot \delay_{\downshift a}\) in \(\D\) which is moreover natural in \(a : \D\). Hence \(\epsilon_a\) is (pointwise) a split epimorphism in \(\D\).
Proof. \(\nu_a\) is a section, and thus by definition \(\epsilon_a\) is a split epimorphism, as we have \[\begin{aligned} \nu_a \cdot \epsilon_a &\equiv (\wrap_a \cdot \delay_{\downshift a}) \cdot (\force_{\downshift a} \cdot \unwrap_{a}) \\&= \wrap_a \cdot (\delay_{\downshift a} \cdot (\force_{\downshift a} \cdot \unwrap_{a})) \\&= \wrap_a \cdot \unwrap_{a} \\&= \id_a \,.\end{aligned}\]
Naturality and thunkability of \(\nu\) follows from \(\delay\) being a linear-and-thunkable natural transformation, and \(\wrap\) being a thunkable natural transformation. I have not yet made precise under which conditions natural transformations actually manage to compose, but it is not automatic in the absence of associativity side conditions, so the manual proof follows. Let \(a,b : \D\) and \(f : a \to b\). We have \[\begin{aligned} \nu_a \cdot \upshift\downshift f &\equiv (\wrap_a \cdot \delay_{\downshift a}) \cdot \upshift\downshift f \\&= \wrap_a \cdot (\delay_{\downshift a} \cdot \upshift\downshift f) \\&= \wrap_a \cdot (\downshift f \cdot \delay_{\downshift b}) \\&= (\wrap_a \cdot \downshift f) \cdot \delay_{\downshift b} \\&= (f \cdot \wrap_b) \cdot \delay_{\downshift b} \\&= f \cdot (\wrap_b \cdot \delay_{\downshift b}) \equiv f \cdot \nu_b\,. \end{aligned}\]
Lemma 4. Let \(\D\) be a duploid. The adjunction \(\upshift \dashv \downshift : \Cnl\D \to \Cpt\D\) satisfies the negative equalizing requirement.
Proof. We have that the counit \(\epsilon_n\) of \(\upshift \dashv \downshift\) is an epimorphism by the previous lemma, thus it suffices to find, for each morphism \(f : \morsof{\acat{O}}{Rn}{m}\) satisfying \(\upshift\downshift\epsilon_n \cdot f^\flat = \epsilon_{\upshift\downshift n} \cdot f^\flat\), a morphism \(f’ : \morsof{\acat{\Cnl\D}}{n}{m}\) such that \(\epsilon_n \cdot f’ = f^\flat\). This morphism is given by \(\nu_n \cdot f^\flat : \morsof{\acat{\Cn\D}}{n}{m}\), but it remains to show that it satisfies the equation and that it is linear. Note that \(f^\flat : \morsof{\Cnl\D}{\upshift\downshift n}{n}\) is linear in \(\D\). Thus for the equation, we have \[\begin{aligned} f^\flat &= \nu_{\upshift\downshift n} \cdot \epsilon_{\upshift\downshift n} \cdot f^\flat \\&= \nu_{\upshift\downshift n} \cdot \upshift\downshift\epsilon_n \cdot f^\flat \\&= \epsilon_n \cdot \nu_n \cdot f^\flat \,. \end{aligned}\] For linearity, it suffices to show \[(\force_{\downshift n} \cdot \unwrap_n) \cdot (\nu_n \cdot f^\flat) = \force_{\downshift n} \cdot (\unwrap_n \cdot (\nu_n \cdot f^\flat))\,.\] On the left, we have \[\begin{aligned}&(\force_{\downshift n} \cdot \unwrap_n) \cdot (\nu_n \cdot f^\flat) \\&\equiv \epsilon_n \cdot (\nu_n \cdot f^\flat) \\&= f^\flat \end{aligned}\] by the above. On the right, note that \(\delay_{\downshift n}\) is linear and hence so too is \(\delay_{\downshift n} \cdot f^\flat\). Thus we have \[\begin{aligned} & \force_{\downshift n} \cdot (\unwrap_n \cdot (\nu_n \cdot f^\flat)) \\&\equiv \force_{\downshift n} \cdot (\unwrap_n \cdot (\wrap_n \cdot \delay_{\downshift n} \cdot f^\flat)) \\&= \force_{\downshift n} \cdot ((\unwrap_n \cdot \wrap_n) \cdot (\delay_{\downshift n} \cdot f^\flat)) \\&= \force_{\downshift n} \cdot \delay_{\downshift n} \cdot f^\flat \\&= f^\flat\,. \end{aligned}\]
PermalinkTheorem 5. Let \(\D\) be a duploid. The adjunction \(\upshift \dashv \downshift : \Cnl\D \to \Cpt\D\) is fully equalizing.
Proof. This follows from the lemma above and its dualization.
Rezk Completion
Given the univalence of the envelope duploid and the full equalizing requirement result above, we should, on paper, have everything to define the Rezk completion of a duploid. Unfortunately, life in UniMath is not so rosy. I outline the development about the Rezk completion of categories that exists in UniMath at the moment, and what appears to be lacking for the duploid equivalent to go smoothly.
Firstly, the goal is to construct given a duploid \(\D\), a univalent duploid \(\Rezk^{\Dupl}(\D)\) along with a duploid functor \(\rezk^{\Dupl}_\D : \D \to \mathfrak{R}^{\Dupl}(\D)\) which is a weak equivalence. The mapping \(\mathfrak{R}^{\Dupl}\) is called a Rezk completion of duploids. This is analogous to the existing Rezk completion of categories which given a category \(\C\), gives a univalent category \(\Rezk^{\Cat}(\C)\) and a weak equivalence of categories \(\rezk^{\Cat}_{\C} : \C \to \Rezk^{\Cat}(\C)\). I will begin dropping the superscripts \(\Dupl\) and \(\Cat\) where it is too verbose.
There is in general no way (constructive or not) to obtain an inverse \((\rezk_{\C})^{-1} : \Rezk(\C) \to \C\), since the equivalence is only weak. This makes it difficult at a glance to even construct the data of an adjunction \[L’ \dashv R’ : \Rezk(\acat{N}) \to \Rezk(\acat{P})\] given one \[L \dashv R : \acat{N} \to \acat{P}\,,\] which is a necessary first step to piecing together a Rezk completion from the envelope duploid. However, the Rezk completion of categories enjoys the following universal property.
Proposition 6. (rezk_completion_initial_functor_from)
Let \(\C\) be a category, \(\D\) be a univalent category, and \(F : \C \to \D\)
be a functor. Then there exists a unique functor \(\hat{F} :
\Rezk^{\Cat}(\C) \to \D\) such that \(\rezk^{\Cat}_\C \cdot
\hat{F} = F\). Graphically, this is the following diagram in \(\Cat\):
which commutes (“strictly”, because \(\D\) is univalent).
An astute observer may notice that I have notated \(\Rezk^\Cat\) to
look suspiciously like a (pseudo)functor of (bi)categories
\[\Rezk^\Cat : \Cat \to \wkcat{UnivCat}\,,\] and \(\rezk^\Cat\)
suspiciously like a (pseudo)natural transformation \[\rezk^\Cat :
\id_\Cat \Rightarrow U\Rezk^\Cat\] where \(U\) is the forgetful
(pseudo)functor \(U : \wkcat{UnivCat} \to \Cat\). I am employing a powerful
technique called “wishful thinking,” since this therefore looks
like it could form a left biadjoint1 \[\Rezk \dashv
U : \Cat \to \wkcat{UnivCat}\,,\] with unit \(\rezk\), since the above
is (almost) the definition of \(\prod_{\C : \Cat}(\Rezk^\Cat(\C),
\rezk^\Cat_\C)\) being a family of left-universal arrows (definition
left_universal_arrow in UniMath ) to \(U\). If the necessary
1-categorical argument generalizes to bicategories, then the family of
left-universal arrows is all that is needed to make \(\Rezk^\Cat\) a
pseudofunctor and left-biadjoint to \(U\).
An observer better-versed in higher category theory2 may note that \(\Rezk^\Cat\) being a pseudofunctor would, I believe, immediately give an adjunction \[\begin{aligned}&\Rezk^\Cat(L \dashv R : \acat{N} \to \acat{P}) \\&= \Rezk(L) \dashv \Rezk(R) : \Rezk(\acat{N}) \to \Rezk(\acat{P})\end{aligned}\] (with the necessary lifted unit and counit) as one would hope for homomorphisms between bicategories. It then remains to show this to be suitably equivalent to the original adjunction, to (therefore) satisfy the equalizing requirement, and to therefore have a (weakly) equivalent envelope duploid. All of these suggest considering seriously the bicategories of adjunctions and duploids3, and their univalent forms.
Unfortunately, I could find no result in UniMath that gives a
biadjunction from a left-universal arrow, or that pseudofunctors
preserve (internal) adjunctions (which both hold, right?). Or any
treatment of \(\Rezk\) specifically as a (pseudo)functor (I have only
really seen it used as left_universal_arrow univ_cats_to_cats). I
feel well out of my depth at the moment in these higher-category
waters, and have not yet had the time to sit down and study it
properly, so I did not prove any of the required results. Thus I am
planning to shelve the Rezk completion of duploids until a later date,
though I am open to discussion on the topic.
References
Footnotes
1 This makes the choice of letter \(\Rezk\) unfortunate, but I think \(\mathfrak{L}\) and \(\mathfrak{l}\) would be even more confusing.
2 As opposed to one whose main knowledge of anything in category theory is how to spot an adjunction.
3 Guillaume also flagged to me a concern with the single-sorted duploids that the main result of his thesis becomes a biequivalence and bireflection of these bicategories, pointing to [1]. I still do not know what the 2-cells of the bicategory of adjunctions should be, but I admittedly haven’t been looking very hard.