December Update
This update will be long, as I have struggled to sit down and actually write one of these. Hopefully over the course of the project I manage to get into a better rhythm of posting-my-thoughts-online, as it is not something I am accustomed to. In the interest of time, so that I do not delay this any longer, parts of this will be formatted less as prose and more as bullet-pointed notes.
Studying Category Theory
I spent some time over the past few weeks revising and further studying category theory, particularly by working through Categories for the working mathematician.. My main goal with this was to have a slightly stronger grasp of the concepts that semanticists throw around1. For example, I remember last year being dazed by the first sentence of a paper reading, “Given a complete and cocomplete symmetric monoidal closed category \(V\) and a symmetric monoidal \(V\)-category \(C\) with cotensors and a strong \(V\)-monad \(T\) on \(C\), …” [2]. I now know intuitively roughly what those might entail, and also that I can instead for the most part just imagine a category or two with some nice structure and all the equations one would hope to hold.
Another important focus was that I wanted to have a much better intuition for adjunctions, both in their own right and in their relation to monads. Although I could remember the hom-set definition (that an adjunction \(F \dashv G\) between functors \(F : \mathcal{C} \to \mathcal{D}\) and \(G : \mathcal{D} \to \mathcal C\) is a \(\mathbf{Set}\)-isomorphism \(\mathcal{D}(FX, Y) \cong \mathcal{C}(X, GY)\) natural in \(X : \mathcal{C}^{\mathrm{op}}\) and \(Y : \mathcal{D}\)) and perhaps even use the universal property definitions (when I looked them up), I had no real understanding or intuition beyond that, or of the relationship between those two definitions2. The textbook [1] gave a suitably gentle introduction via comma categories, universal arrows (aka reflections), the Yoneda lemma, adjunctions, and monads, where I stopped for the time being.
Topical Background Reading
I read through a great deal of the relevant background material; including univalent categories [3], Moggi’s computational lambda calculus [4], thunk-force categories [5], and call-by-push-value [6]. I also read through the first few chapters of Munch-Maccagnoni’s PhD thesis [7], in particular the chapter on duploids [8] which I started formalising within UniMath .
Formalising Duploids
I made a start on defining and proving some properties about duploids, whose current state of development can be found here. The definitions and names are preliminary while I figure out some of the issues and advantages of various approaches, and I include my thoughts below.
Definitions
Unlike Munch-Maccagnoni’s thesis [8], and following [9], I define initially the “single-sorted” duploids and related constructions, as follows:
-
A “single-sorted quasiduploid” \(\mathcal{C}\) (or “non-associative category” or “unital magmoid” [9] or “deductive system”) consists of the following data:
- A type \(\mathrm{ob}\ \mathcal{C}\) of objects. In the following, lower case letters \(a, b, c\) will be of type \(\mathrm{ob} \ \mathcal{C}\).
- A family of types \(\mathcal{C}\llbracket a, b \rrbracket\) of morphisms between \(a\) and \(b\). This will also be written \(a \to b\) where unambiguous. Morphisms will be called \(f, g, h, k\).
- For each two morphisms \(f : a \to b\) and \(g : b \to c\), a morphism which is their composition \(f \cdot g : a \to c\) (written in diagrammatic order, by UniMath convention).
- For each object \(a : \mathrm{ob}\ \mathcal{C}\), an identity morphism \(\mathrm{id}_a : a \to a\).
- Proofs that each \(\mathcal{C}\llbracket a, b \rrbracket\) is a set.
- Proofs that for any morphism \(f : a \to b\), the identity is the neutral element on the left: \(\mathrm{id}_a \cdot f = f\), and on the right: \(f \cdot \mathrm{id}_b = f\).
More briefly, this can also be described as the following:
- A category \(\mathcal{C}\) without the condition for associativity of composition: \(f \cdot (g \cdot h) \ne (f \cdot g) \cdot h\) (in general).
- A thunkable morphism \(f : a \to b\) is one for which
left-composition associates: \(f \cdot (g \cdot h) = (f \cdot g)
\cdot h\) (for all morphisms \(g\) and \(h\)). A negative object
\(a : \mathrm{ob}\ \mathcal{C}\) is one for which all incoming
morphisms \(f : b \to a\) (for any \(b : \mathrm{ob}
\mathcal{C}\)) are thunkable.- Dually, a linear morphism \(f : a \to b\) is one for which right-composition associates: \((h \cdot g) \cdot f = h \cdot (g \cdot f)\) (for all morphisms \(g\) and \(h\)), and a positive object \(a\) is one for which all outgoing morphisms \(f : a \to b\) (for any \(b : \mathrm{ob}\ \mathcal{C}\)) are linear.
- I note that identity morphisms are thunkable and linear, and
moreover that thunkable and linear morphisms are closed under
composition. Thus, we have the following subcategories of
\(\mathcal{C}\):
- The “linear category” \(\mathcal{C}_l\) consisting of all objects and linear
morphisms.
- Dually, the “thunkable category” \(\mathcal{C}_t\) consisting of all objects and thunkable morphisms.
- The “negative category” \(\mathcal{N}\) consisting of negative objects and all
morphisms between them (which are necessarily thunkable).
- Dually, the “positive category” \(\mathcal{P}\) consisting of positive objects and all morphisms between them (which are necessarily linear).
- The “negative linear category” \(\mathcal{N}_l\) consisting of negative objects and
linear (and necessarily also thunkable) morphisms.
- Dually, the “positive thunkable category” \(\mathcal{P}_t\) consisting of positive objects and thunkable (and necessarily also linear) morphisms.
- The “linear category” \(\mathcal{C}_l\) consisting of all objects and linear
morphisms.
- A “single-sorted preduploid” is a single-sorted quasiduploid \(\mathcal{C}\) with
the following property:
- Every object \(a : \mathrm{ob}\ \mathcal{C}\) is merely3 either positive or negative (or both).
- A “single-sorted duploid” is a single-sorted preduploid \(\mathcal{C}\) with the
following additional data:
- For every object \(a : \mathrm{ob}\ \mathcal{C}\), its upshift \({\Uparrow}a : \mathrm{ob}\ \mathcal{C}\), a proof that \({\Uparrow}a\) is negative, and an invertible linear morphism \(\mathrm{force}_a : {\Uparrow}a \to a\), whose inverse is called \(\mathrm{delay}_a : a \to {\Uparrow}a\).
- Dually, for every object \(a : \mathrm{ob}\ \mathcal{C}\), its downshift \({\Downarrow}a : \mathrm{ob}\ \mathcal{C}\), a proof that \({\Downarrow}a\) is positive, and an invertible thunkable morphism \(\mathrm{wrap}_a : a \to {\Downarrow}a\), whose inverse is called \(\mathrm{unwrap}_a : {\Downarrow}a \to a\).
- A “polarization choice” on a single-sorted quasiduploid
\(\mathrm{ob}\ \mathcal{C}\) consists of the following data:
- A function \(\mathrm{polarization} : \mathrm{ob}\ \mathcal{C} \to \texttt{bool}\).
- For each object \(a : \mathrm{ob}\ \mathcal{C}\), a proof that \(a\) is positive if \(\mathrm{polarization}\ a = \texttt{true}\), or negative otherwise.
-
A “split preduploid” is a single-sorted preduploid with a polarization choice on it. Likewise, a “split duploid” is a single-sorted duploid with a polarization choice.
The aim of these definitions is to bridge the single-sorted (pre)duploids to the (two-sorted) duploids as defined originally, which makes it much clearer what a functor of (pre)duploids should be.
Discussion
Using the definitions above, I formalised up to proposition II.24 in Munch-Maccagnoni’s thesis [7]. The important constructions so far include the duploid arising from an adjunction, and the adjunction \({\Downarrow} \dashv {\Uparrow} : \mathcal{C}_l \to \mathcal{C}_t\) arising from a duploid. It was at this point where I stopped, both because I have better things to do at this time of year, and because I had some hangups:
-
I was unable to prove that the functor \({\Uparrow} : \mathcal{C}_l \to \mathcal{N}_l\) given on morphisms \(f : a \to b\) by \({\Uparrow}f = \mathrm{force}_a \cdot f \cdot \mathrm{delay}_b\) is even well-defined at all (and the dual functor \({\Downarrow}\)). The omission of the parenthesis and the proof in the thesis is only coherent if \(\mathrm{delay}_b\) is linear, but I cannot convince myself of why this should be true, and it does not seem to be explicitly mentioned anywhere. Parenthesising as \({\Uparrow}f = (\mathrm{force}_a \cdot f) \cdot \mathrm{delay}_b\) and expanding the codomain as \({\Uparrow} : \mathcal{C}_l \to \mathcal{N}\) works just fine, but renders the statement and proof of proposition II.23 incoherent:
- Proposition II.23 [7] The functors \({\Uparrow} : \mathcal{C}_l \to \mathcal{N}_l\) and \({\Downarrow} : \mathcal{C}_t \to \mathcal{P}_t\) take part in adjoint equivalences of categories \(I \dashv_{(\mathrm{delay},\mathrm{force})} {\Uparrow} : \mathcal{C}_l \to \mathcal{N}_l\) and \(I \dashv_{(\mathrm{wrap},\mathrm{unwrap})} {\Downarrow} : \mathcal{C}_t \to \mathcal{P}_t\).
I hope the mistake lies with me. I will need to check if the prototypical duploid-arising-from-an-adjunction satisfies the required linearity, otherwise I am slightly worried about the consequences.
-
It is unclear to me what a functor of single-sorted (quasi/pre)duploids \(F : \mathcal{C} \to \mathcal{D}\) should be. One could say it “preserves polarities” [9], but should this mean that it takes negative-and-positive objects of \(\mathcal{C}\) to negative-and-positive objects of \(\mathcal{C}\)? This is, on the face of it, slightly stricter than a functor of split (pre)duploids that merely has to preserve the chosen polarization, so that a functor of split (pre)duploids would not necessarily be one on the underlying single-sorted (quasi/pre)duploids.
-
It is not yet written down what an “indistinguishability” would be for a single-sorted duploid, in the sense of [10], the way it is for the two-sorted kind. I’m sure one could follow the procedure therein to find it, but I have not read and internalised enough univalent foundations to grasp it (perhaps I shall do so if I get bored). The definition I have written down is that of a “pair of linear and thunkable inverses,” i.e. a pair of morphisms which are both linear, both thunkable, and inverses of each other on both sides. This corresponds to the definition by [9], and to the notion given in [10] for the two-sorted duploids. Requiring that the types of indistinguishabilities be equivalent to paths would hopefully give a satisfying definition of “univalence” for duploids, which is after all the point of my project.
-
The construction of a (split) duploid arising from an adjunction \(L \dashv R\), decomposes into positive and negative categories which are the Kleisli and CoKleisli category of the adjunction’s monad and comonad respectively. Unfortunately these are the non-univalent (Co)Kleisli categories given by positive/negative objects and morphisms \(a \to RLb\) and \(LRa \to b\), rather than the weakly-equivalent but univalent subcategory of the Eilenberg-Moore categories. Hopefully we can find an equivalent duploid which appropriately decomposes into the univalent (Co)Kleisli categories.
-
I have yet to use the polarization property of single-sorted preduploids, and I wonder if I will.
Those are my thoughts for the moment. If you are Jon, you may also be interested in my note on sleeping laptops.
References
Footnotes
1 A secondary goal was preparation for the “Advanced Topics in Category Theory” course I am conveniently taking next term.
2 The answer, as always, turns out to be (a corollary of) the Yoneda lemma.
3 Using the language of Ahrens et al. [3], merely suggests propositional truncation of the subsequent type.