February Update 4
This week I proved univalence for the single-sorted duploid arising from a (fully equalizing) adjunction between univalent categories, however I struggled to prove that the upshift-downshift adjunction satisfies the full equalizing requirement. I will try to keep today’s note short, since I have mostly been getting on with other work.
Univalence of the Envelope Duploid
The main result is as follows.
PermalinkTheorem 1. Given a fully equalizing adjunction \(L \dashv R : \acat{N} \to \acat{P}\) between univalent categories \(\acat{N}\) and \(\acat{P}\), the envelope duploid \(\acat{E}[L \dashv R]\) is univalent.
Proof. It suffices to prove that \(\Cnl{\acat{E}[L \dashv R]}\) and \(\Cpt{\acat{E}[L \dashv R]}\) are univalent, which I do below.
Before we can tackle those subproofs, we first need some preliminary definitions and lemmas, from which we get the above as a simple corollary. For the following, let \(L \dashv R : \acat{N} \to \acat{P}\) be an adjunction.
Definition 2. An object \(n : \acat{N}\), is a negative pre-fixed point of the adjunction if \(LR\epsilon_n = \epsilon_{LRn}\), and a negative fixed point if \(\epsilon_n\) is an isomorphism. Dually, an object \(p : \acat{P}\), is a positive pre-fixed point if \(RL\eta_p = \eta_{RLp}\), and a positive fixed point if \(\eta_p\) is an isomorphism. For an object from either \(\acat{N}\) or \(\acat{P}\), we may drop the polarity from the name, so that it may simply be called a pre-fixed point or a fixed point of the adjunction.
The name pre-fixed point and my addition of polarities is something I made up, but here is a reminder that I occasionally do use names of things that already exist:
Remark 3. (textbook) The fixed points give the full subcategories of \(\acat{N}\) and \(\acat{P}\) on which \(L \dashv R : \acat{N} \to \acat{P}\) restricts to an adjoint equivalence.
Lemma 4. Any fixed point of \(L \dashv R\) is also a pre-fixed point of \(L \dashv R\).
Proof. Without loss of generality, let \(n : \acat{N}\) such that \(\epsilon_n\) is an isomorphism. We need that \(LR\epsilon_n = \epsilon_{LRn}\). Since \(\epsilon_n\) is an isomorphism, it suffices to prove: \[\begin{aligned} LR\epsilon_n^{-1} \cdot LR\epsilon_{n} &= LR(\epsilon_n^{-1} \cdot \epsilon_{n}) \\ &= \id_{LRn} \\ &= \epsilon_{n}^{-1} \cdot \epsilon_{n} \\ &= LR\epsilon_n^{-1} \cdot \epsilon_{LRn}\,. \end{aligned}\]
Lemma 5. If \(L \dashv R\) satisfies the negative equalizing requirement, then the negative fixed points and negative pre-fixed points coincide, and dually for the positive case.
Proof. The previous lemma gives pre-fixed point from fixed point, so we need only fixed point from pre-fixed point. Without loss of generality, let \(n : \acat{N}\) such that \(LR\epsilon_n = \epsilon_{LRn}\), for which we need to prove that \(\epsilon_n\) is an isomorphism. The negative equalizing requirement gives a unique \(f’ : \morsof{\acat{N}}{n}{LRn}\) such that \(\epsilon_n \cdot f’ = \id_{LRn}\), moreover we have that \(\epsilon_n\) is an epimorphism from the equalizing requirement. Thus, from \(\epsilon_n \cdot f’ \cdot \epsilon_n = \epsilon_n \cdot \id_{n}\) we have \(f’ \cdot \epsilon_n = \id_n\). Therefore \(\epsilon_n\) is an isomorphism with inverse \(f’\).
Relating this all back to the envelope duploid, we get the following important result, which specializes the above to the envelope duploid.
Lemma 6. Given an object \(\left(p \xrightarrow{\alpha} n\right) : \acat{E}[L \dashv R]\), if \(L \dashv R\) satisfies the negative equalizing requirement then \(\alpha^\flat : \morsof{\acat{N}}{Lp}{n}\) is an isomorphism if and only if \((p,n,\alpha)\) is positive. If \(L \dashv R\) satisfies the positive equalizing requirement then \(\alpha^\sharp : \morsof{\acat{P}}{p}{Rn}\) is an isomorphism if and only if \((p,n,\alpha)\) is negative.
Proof. The forward implications are already proven in constructing the envelope duploid, so we need only the backward directions. Without loss of generality, I prove only the latter case. Assume that \((p,n,\alpha)\) is negative. We already have that either \(\alpha^\flat\) or \(\alpha^\sharp\) must be an isomorphism: if \(\alpha^\sharp\) we are done, otherwise assume that \(\alpha^\flat\) is an isomorphism, hence \((p,n,\alpha)\) is also positive. A negative-and-positive object has \(p\) a positive pre-fixed point, which is also a positive fixed point from the positive equalizing requirement, so we have \(\eta_p\) an isomorphism. Finally, we have \[\alpha^\sharp = \varphi_{L \dashv R}(\alpha^\flat) = \eta_p \cdot R\alpha^\flat\,,\] which is an isomorphism since \(\eta_p\) and \(\alpha^\flat\) are.
This gives the following proof for the main result:
Lemma 7. If \(\acat{N}\) and \(\acat{P}\) are univalent and \(L \dashv R\) satisfies the full equalizing requirement, then every negative object \((p,n,\alpha) : \acat{E}[L \dashv R]\) is of the form \(\iota^\ominus(n)\). Dually, every positive object \((p,n,\alpha) : \acat{E}[L \dashv R]\) is of the form \(\iota^\oplus(p)\).
Proof. Informally, for the \(\iota^\ominus(n) \equiv (Rn,n,(\id_{Rn})^{\sharp^{-1}}) \stackrel{?}{=} (p,n,\alpha)\) case, by path induction on \(p \stackrel{\alpha^\sharp}{\cong} Rn\) using univalence of \(\acat{P}\). Formally, this is constructed with reflexive graphs which bundles univalence of \(\acat{N}\) into the proof.
Lemma 8. If \(\acat{N}\) and \(\acat{P}\) are univalent and \(L \dashv R\) satisfies the full equalizing requirement, then \(\acat{N} = \Cnl{\acat{E}[L \dashv R]}\) and \(\acat{P} = \Cpt{\acat{E}[L \dashv R]}\).
Proof. The inclusion functor \(\iota^\ominus : \acat{N} \to \Cnl{\acat{E}[L
\dashv R]}\) is fully faithful by the equalizing requirement, and the
previous lemma makes it an equivalence on objects, thus it is a
catiso and hence a path by the univalence axiom.
Corollary 9. If \(\acat{N}\) and \(\acat{P}\) are univalent and \(L \dashv R\) satisfies the full equalizing requirement, then \(\Cnl{\acat{E}[L \dashv R]}\) and \(\Cpt{\acat{E}[L \dashv R]}\) are univalent.
Proof. \(\acat{N}\) is univalent and \(\acat{N} = \Cnl{\acat{E}[L \dashv R]}\), likewise for \(\acat{P} = \Cpt{\acat{E}[L \dashv R]}\).
The Upshift-Downshift Adjunction
Given a duploid \(\D\), there is an adjunction \(\upshift \dashv \downshift : \Cnl\D \to \Cpt\D\). This adjunction is important, because \(\D\) is in fact (weakly) equivalent to the duploid arising from this adjunction, whether that be the single-sorted envelope duploid \(\acat{E}[\upshift \dashv \downshift]\) or the two-sorted/split oblique duploid \(\acat{O}[\upshift \dashv \downshift]\). If this adjunction is fully equalizing, then using the univalence result above, we could take any duploid \(\D\) and obtain an equivalent univalent duploid — a Rezk completion for duploids. Take the adjunction \(\upshift \dashv \downshift : \Cnl\D \to \Cpt\D\), obtain univalent categories equivalent to \(\Cnl\D\) and \(\Cpt\D\) by Rezk completion, and then take the duploid \(\acat{E}[\upshift \dashv \downshift]\) (transporting over the equivalences), and then prove that to be equivalent to \(\D\) (by transporting over the equivalences).
Unfortunately I was unable to prove the equalizing requirement for this adjunction. For the negative equalizing requirement, given an \(f^\flat : \morsof{\Cnl\D}{\upshift\downshift n}{m}\) such that \(\epsilon_{\upshift\downshift n} \circ f^\flat = \upshift\downshift\epsilon_{n} \circ f^\flat\), I was unable to construct a linear morphism \(f’ : \morsof{\Cnl\D}{n}{m}\) which needs to be unique such that \(\epsilon_n \cdot f’ = f^\flat\), or equivalently \(\downshift f’ = f^\sharp\). Recall that \[\begin{aligned} \morsof{\Cnl\D}{\upshift\downshift n}{m} &\stackrel{\varphi_{\upshift \dashv \downshift}}{\cong} \morsof{\Cpt\D}{\downshift n}{\downshift m} \\&\stackrel{\downshift^{-1}}{\cong} \morsof{\Ct\D}{n}{m} \\&\stackrel{\text{subcat}}{\cong} \morsof{\Cn\D}{n}{m} \end{aligned}\] using our zoo of adjunctions and equivalences, giving us \(f’ : \morsof{\Cn\D}{n}{m}\) from \(f^\flat\) unique such that \(\downshift f’ = f^\sharp\), but I do not see how it could be linear. I hope that this is what kids these days call a “skill issue,” so I emailed Guillaume in the hope that it really is. Until he replies I will try very hard not to let this bother me, since I have enough to write about as is.