February Update 3

This week I spent a little time looking at and proving some of the last few theorems from Guillaume’s thesis. I put this off initially in order to get a better grasp of how duploids feel in my hands. This post today is less detailed and organized than I would like it to be due to time constraints, so it may require Guillaume’s thesis in hand, and a little peeking at the code for detailed definitions and proofs, which is hopefully not too burdensome.

The Adjunctions of a Duploid

I finally managed a satisfying way of proving the numerous adjunctions within a duploid.

First, given categories and graph homomorphisms (functors without axioms) \((L_1 : \D_1 \to \C_1)\ (R_1 : \D_2 \to C_1)\ (L_2 : \D_1 \to \C_2)\ (R_2 : \D_2 \to \C_2)\), I defined explicitly a type of “hom-type natural isomorphisms” \(\orgcode{natural\_bi\_hom\_weq} \ L_1\ R_1\ L_2\ R_2 : \prod_{a : \D_1, b : \D_2} \morsof{\C_1}{L_1 a}{R_1 b} \cong \morsof{\C_2}{L_2 a}{R_2 b}\) where \(\cong\) denotes an isomorphism in \(\Set\) natural covariantly in \(a\) and contravariantly in \(b\). One recovers the definition of an adjunction, specifically the “transpose” natural isomorphism of an adjunction, by setting \(R_1\) and \(L_2\) to identities. This definition has nice properties, yielding a groupoid structure on pairs of graph homomorphisms sharing a codomain \(\D_1 \xrightarrow{L} \C \xleftarrow{R} \D_2\). The possibility of inverses in particular makes the proofs easily dualize between the upshift and downshift cases for duploids. There is also some weird horizontal composition sort of thing that let me do one weird trick at some point, but I’ll get into that some other time probably.

Second, I was unsatisfied with the units and counits that the adjunctions derived this way were providing. There were spurious identity morphisms and they also took an obscene amount of time to normalize during proofs. I solved this by writing a definition to just replaces the (components of the) units and counits of an existing adjunction, so long as I can prove that they are equal. I still get naturality of the units/counits for free, and of course the triangle laws transport across just fine. This solves both the horrendous computation times and the distasteful identity morphisms.

The crucial information I want to include in this section is the specific natural isomorphisms and the definitions of the transposes.

\[\begin{aligned} \varphi_{(a : \D),(b : \D)} &: \morsof{\D}{\downshift a}{b} \cong \morsof{\D}{a}{b} \\ \varphi_{a,b}(f) &= \wrap_a \cdot f \\ \varphi_{a,b}^{-1}(g) &= \unwrap_a \cdot f \end{aligned}\]

\[\begin{aligned} \psi_{(a : \D),(b : \D)} &: \morsof{\D}{a}{\upshift b} \cong \morsof{\D}{a}{b} \\ \psi_{a,b}(f) &= f \cdot \force_b \\ \psi_{a,b}^{-1}(g) &= f \cdot \delay_b \end{aligned}\]

\[\begin{aligned} \chi_{(a : \D),(b : \D)} &: \morsof{\D}{\downshift a}{b} \cong \morsof{\D}{a}{\upshift b} \\ &= \varphi_{a,b} \cdot \psi_{a,b}^{-1} \\ \chi_{a,b}(f) &= \wrap_a \cdot f \cdot \delay_b \\ \chi_{a,b}^{-1}(g) &= \unwrap_a \cdot f \cdot \force_b \end{aligned}\]

(The lack of parentheses is justified by \(\wrap\)/\(\unwrap\) being thunkable, and \(\delay\)/\(\force\) being linear.)

These become proper adjunctions once restricted to \(a\) and \(b\) on which they are functorial.

The other important adjunction is the one \(\upshift \dashv \downshift : \Cnl\D \to \Cpt\D\). This has transpose given below:

\[\begin{aligned} \xi_{(a : \Cpt\D),(b : \Cnl\D)} &: \morsof{\Cnl\D}{\upshift a}{b} \cong \morsof{\Cpt\D}{a}{\downshift b} \\ \xi_{a,b} &= \delay_a \cdot f \cdot \wrap_b \\ \xi_{a,b}^{-1} &= \force_a \cdot f \cdot \unwrap_b \end{aligned}\]

(The lack of parentheses here is justified by \(\upshift a\) being negative and \(\downshift b\) being positive.)

The Structure Theorem for Envelope Duploids (Part 1)

A couple weeks ago I introduced the envelope duploid, this week I proved part of the “structure theorem” chapter: that \(\acat{E}[\upshift \dashv \downshift : \Cnl\D \to \Cpt\D] \cong \D\) for a duploid \(\D\). First I make the following destructive change to the definition of an oblique morphism.

Definition 1. Given an adjunction \(L \dashv R : \acat{N} \to \acat{P}\) witnessed by the transposition natural transformation \(\varphi_{p,n} : \morsof{\acat{N}}{L p}{n} \cong \morsof{\acat{P}}{p}{R n}\), an oblique morphism from \(p : \acat{P}\) to \(n : \acat{N}\), written \(f : \morsof{\acat{O}_{L \dashv R}}{p}{n}\), is defined as a pair of a morphism \(f^\flat : \morsof{\acat{N}}{L p}{n}\) and a morphism \(f^\sharp : \morsof{\acat{P}}{p}{R n}\) such that \(\varphi_{p,n}(f^\flat) = f^\sharp\). Where the adjunction is obvious I will freely omit it from \(\acat{O}\), and transpositions or projections \(\flat\)/\(\sharp\) may be elided so that a morphism \(\morsof{\acat{O}}{p}{n}\) may equally be considered a morphism in \(\acat{N}\) or \(\acat{P}\).

Recall that before I made an arbitrary choice to identify \(\morsof{\acat{O}}{p}{n}\) with \(\morsof{\acat{N}}{L p}{n}\). The informal mathematics is largely unaffected, but this change should hopefully at least make the notation slightly clearer. Formally, this change is semantically the same: it is easy to prove \[\morsof{\acat{O}}{p}{n} \stackrel{\flat}{\simeq} \morsof{\acat{\acat{N}}}{L p}{n} \stackrel{\varphi}{\simeq} \morsof{\acat{\acat{P}}}{p}{R n} \stackrel{\sharp^{-1}}{\simeq} \morsof{\acat{O}}{p}{n}\,,\] but carrying both morphisms around explicitly allows morphisms to be specified by \(f^\sharp \triangleq \text{blah}\) and then have \(f^\sharp\) compute definitionally to \(\text{blah}\), which therefore also allows \(f =_{\morsof{\acat{O}}{p}{n}} g\) to be proven with \(f^\sharp =_{\morsof{\acat{P}}{p}{R n}} g^\sharp\) without having to explicitly invoke injectivity of \(\varphi^{-1}\) or cancellations \(\varphi^{-1}(\varphi(h)) = h\). This was also very helpful when doing proofs where \(\varphi\) itself was known and unfolded even when I did not want it to, since the proofs of \(\varphi\) and \(\varphi^{-1}\) being inverses are not trivial.

Remark 2. For any adjunction \(L \dashv R : \acat{N} \to \acat{P}\), there are inclusion functors \(\iota^\ominus : \acat{N} \to \acat{E}[L \dashv R]\) and \(\iota^\oplus : \acat{P} \to \acat{E}[L \dashv R]\) whose image only contains linear and thunkable morphisms. These are given on objects by \[\begin{aligned}\iota^\ominus(n) &= (Rn, n, (\id_{Rn})^{\sharp^{-1}}) \\ \iota^\oplus(p) &= (p, Lp, (\id_{Lp})^{\flat^{-1}})\,.\end{aligned}\]. When restricted to the negative-linear and positive-thunkable subcategories as \(\iota^\ominus : \acat{N} \to \Cnl{\acat{E}[L \dashv R]}\) and \(\iota^\oplus : \acat{P} \to \Cpt{\acat{E}[L \dashv R]}\), they are split essentially-surjective with the evident inverse.

This allows the following definition of shifts in the envelope duploid.

Lemma 3. The envelope preduploid \(\acat{E}[L \dashv R]\) has a negative shift structure given by \[\begin{aligned}\upshift (p,n,\alpha) &\triangleq \iota^\ominus(n) \\ \wrap_{(p,n,\alpha)} &\triangleq (\id_{Lp})^{\flat^{-1}} \\ \unwrap_{(p,n,\alpha)} &\triangleq \alpha\,.\end{aligned}\] Dually it has a positive shift structure given by \[\begin{aligned}\downshift (p,n,\alpha) &\triangleq \iota^\oplus(p) \\ \force_{(p,n,\alpha)} &\triangleq (\id_{Rn})^{\sharp^{-1}} \\ \unwrap_{(p,n,\alpha)} &\triangleq \alpha\,.\end{aligned}\]

PermalinkTheorem 4. Let \(\D\) be a single-sorted duploid. The single-sorted envelope duploid on the upshift-downshift adjunction \(\D’ \triangleq \acat{E}[\upshift \dashv \downshift : \Cnl\D \to \Cpt\D]\) is weakly equivalent to \(\D\), in that there is a fully-faithful functor \(F : \D \to \D’\) that is merely surjective on objects up to linear-and-thunkable isomorphism. (Not formalized) this weak equivalence can be upgraded to a strong equivalence (split surjection) using the law of the excluded middle, or (as with all weak equivalences) if \(\D\) is univalent.

Proof. Recall that an object of \(\D’\) consists of a triple \((p : \Cpt\D, n : \Cnl\D, \alpha : \morsof{\acat{O}}{p}{n})\) where either \(\alpha^\flat\) or \(\alpha^\sharp\) is an isomorphism. Define \(F\) on objects as:

\[\begin{aligned} F(a : \D) &\triangleq (\downshift a, \upshift a, \alpha_a) \\ \alpha_a^\flat &\triangleq \upshift(\unwrap_a) : \morsof{\Cnl\D}{\upshift\downshift a}{\upshift a} \\ \alpha_a^\sharp &\triangleq \downshift(\delay_a) : \morsof{\Cpt\D}{\downshift a}{\downshift\upshift a} \end{aligned}\]

The equation \(\xi_{\downshift a,\upshift a}(\alpha_a^\flat) = \alpha_a^\sharp\) (where \(\xi\) is as given above) is the equation \(\delay_{\downshift a} \cdot \upshift(\unwrap_a) \cdot \wrap_{\upshift a} = \downshift(\delay_a)\) which amounts to naturality of \(\delay : 1_\D \to \upshift\) and unfolding the definition \(\downshift (f : a \to b) = \unwrap_a \cdot f \cdot \wrap_b\).

When \(a\) is positive, \(\unwrap_a : a \to \upshift a\) becomes linear, and so an isomorphism in \(\Cl\D\), which gets preserved by the functor \(\upshift : \Cl\D \to \Cpt\D\) so that \(\alpha^\flat = \upshift(\unwrap_a)\) is an isomorphism in \(\Cpt\D\). The case is symmetric for \(\alpha^\sharp\)¹.

On morphisms, \(F\) is defined as follows:

\[\begin{aligned} F(f : a \to b) &: \morsof{\acat{O}}{\downshift a}{\upshift b} \\ (Ff)^\flat &= \upshift(\unwrap_a \cdot f) \\ (Ff)^\sharp &= \downshift(f \cdot \delay_b) \end{aligned}\]

Just trust me that this is well defined for now.

This functor is fully-faithful: the action on morphisms is precisely \[\morsof{\D}{a}{b} \stackrel{\varphi_{a,b}^{-1}}{\simeq} \morsof{\Cl\D}{\downshift a}{b} \stackrel{\upshift}{\simeq} \morsof{\Cnl\D}{\upshift \downshift a}{\upshift b} \stackrel{\flat^{-1}}{\simeq} \morsof{\acat{O}}{\downshift a}{\upshift b}\] where \(\varphi\) is as for the adjunction above and \(\upshift : \Cl\D \to \Cnl\D\) is fully faithful due to being an equivalence.

It remains to show that for any object \((p : \Cpt\D, n : \Cnl\D, \beta) : \D’\), there merely exists an object \(a : \D\) such that \((\downshift a, \upshift a, \alpha_a) \cong_{lt} (p, n, \beta)\). For this, note that \(a \cong_{lt} \upshift a\) by \(\delay_a\) and \(\force_a\) if and only if \(a\) is negative, and \(a \cong_{lt} \downshift a\) by \(\wrap_a\) and \(\unwrap_a\) if and only if \(a\) is positive. Thus we merely need to choose one of \(p\) or \(n\) by deciding (either with choice or under propositional truncation) whether \((p,n,\beta)\) is positive or negative. Suppose without loss of generality that \((p,n,\beta)\) is positive. We have \[\begin{aligned}(\downshift p, \upshift p, \alpha_p) &\stackrel{\wrap}{\cong_{lt}} \downshift(\downshift p, \upshift p, \alpha_p) \\ &\stackrel{\text{def}}\equiv (\downshift p, \upshift \downshift p, {\cdots}) \\ &\stackrel{\iota^\ominus(\unwrap)}{\cong_{lt}} (p, \upshift p, {\cdots}) \\ &\stackrel{\text{def}}{\equiv} \downshift(p, n, \beta) \\ &\stackrel{\unwrap}{\cong_{lt}} (p, n, \beta)\,. \end{aligned}\]

\(\square\)

It remains for me to address the equivalence with the category of adjunctions, or more precisely those satisfying the equalizing requirement, which I have not gotten to yet. I am having the embarrassing realization that the equalizing requirement is probably something I should have pondered and internalized a little sooner, because it might solve the problems related to univalence that I was seeing.

PermalinkDefinition 5. An adjunction \(L \dashv R : \acat{N} \to \acat{P}\) is said to satisfy the positive equalizing requirement or to be positive equalizing if the restricted inclusion functor \(\iota^\oplus : \acat{P} \to \Cpt{\acat{E}[L \dashv R]}\) is fully faithful, and hence a strong equivalence. Dually, it satisfies the negative equalizing requirement or to be negative equalizing if \(\iota^\ominus : \acat{N} \to \Cnl{\acat{E}[L \dashv R]}\) is fully faithful, and hence a strong equivalence. The adjunction is said to satisfy the full equalizing requirement or to be fully equalizing, if it satisfies both the positive and negative equalizing requirements.

This is slightly different but ends up being equivalent to Guillaume’s original statement of the equalizing requirement.

It follows that, in the envelope duploid over a negative equalizing adjunction, the linear-and-thunkable isomorphisms between negative objects become isomorphisms between their negative projections, and dually for positive equalizing adjunctions.

I will have to explore how this interacts with univalence, particularly for objects which are both negative and positive. It could easily be that the envelope duploid of a fully equalizing adjunction between univalent categories is already univalent². This would really be a nice result and finally give me a good place to put down Proof General and start writing the thesis properly.

Footnotes

¹ This is what made me give up and go back to make the oblique morphisms compute nicer.

² In fact, the oblique duploid probably is, but only as a split duploid in a way that I have not yet developed the theory for.