April Update 2
I have continued to write this week. I do not have much to say on this, except that I have now made it so that I can keep multiple dated versions of the rendered writeup available at https://notes.eutro.dev/cs/diss/output/.1 As well as writing, it seems inevitable that I will continue to ponder the outstanding mathematical problems. Fortunately, working with bicategories in UniMath is incredibly painful, so that keeps me away for the most part. My most significant achievement this week is that I have constructed a unital magmoid with a linear-and-thunkable isomorphism which is not intermediate.
A Linear-and-Thunkable Isomorphism which is Not Intermediate
One of my early concerns was this: what is a suitable notion of an “indistinguishability” in a unital magmoid? This would be a type of morphism \(p : a \cong_* b\) for which “indistinguishability induction” (handling only \(b \equiv a\) and \(p \equiv \id_a\)) is valid. In other words, a type for which an equivalence \((a = b) \cong (a \cong_* b)\) (taking \(\refl_a\) to \(\id_a\)) could feasibly exist. This is the same as asking, “what morphisms in a unital magmoid correspond to identifications when we consider a univalent unital magmoid?”
As is the case for isomorphisms in categories, an indistinguishability \(p : a \cong_* b\) in a unital magmoid must have an inverse \(p^{-1} : b \cong_* a\). However, this is not sufficient in a unital magmoid: we need to place further associativity conditions on \(p\) for it to be able to behave like an indistinguishability. That is, to have all the properties of \(\id_a\).
In a duploid, we have seen that being a linear-and-thunkable isomorphism seems to be the correct notion of an indistinguishability. We have also seen that all linear-and-thunkable isomorphisms in a preduploid are intermediate (see the definition below). However, this does not appear to be true in a unital magmoid in general, and I have been trying to pin down a counterexample. I present one today.
The terms “linear” and “thunkable” are the names Guillaume gave them, and “intermediate” is a name I made up. The following is a definition from my writeup. Note that I have taken to using \(f \dcomp g\) to denote composition in diagrammatic order, rather than taking \(f \cdot g\) from UniMath .
Definition 1. We say that a path of morphisms
\begin{equation} a_0 \xrightarrow{f_1} a_1 \xrightarrow{f_2} a_2 \rightarrow \cdots \rightarrow a_{n-1} \xrightarrow{f_n} a_n \end{equation}
in a unital magmoid associates when all ways of parenthesising their composite \(f_1 \dcomp f_2 \dcomp \cdots \dcomp f_n\) are equal. In the simplest case, a triple of morphisms \(a \xrightarrow{f} b \xrightarrow{g} c \xrightarrow{h} d\) associates if and only if we have \(f \dcomp (g \dcomp h) = (f \dcomp g) \dcomp h\).
We say that:
- \(f\) is thunkable when all triples \((f,g,h)\) associate.
- \(h\) is linear when all triples \((f,g,h)\) associate.
- \(g\) is intermediate when all triples \((f,g,h)\) associate.
- \(b\) is (semantically) negative when all morphisms into \(b\) are thunkable.
- \(c\) is (semantically) positive when all morphisms out of \(c\) are linear.
Notation 2. Let \(a, b : \M\) be objects in a unital magmoid \(\M\). We may write the subscripts from the Subcategories of a Unital Magmoid onto the binary operators \(a \rightarrow b\) (morphisms) or \(a \cong b\) (isomorphisms) to denote that the morphism or isomorphism resides in the corresponding subcategory of the unital magmoid. For example, \(a \Cl\rightarrow b\) denotes a linear morphism; \(a \Clt\cong b\) denotes a linear-and-thunkable isomorphism: an isomorphism which is linear-and-thunkable, and has a linear-and-thunkable inverse.
The question I wanted to answer is this:
Proposition 3. Let \(\M\) be a unital magmoid. Could there be a linear-and-thunkable isomorphism \(a \Clt\cong b\) in \(\M\) which is not intermediate?
I can answer this in the affirmative today with a small counterexample.
Definition 4. There is a unital magmoid \(\wkcat{Lini}\)2 generated by four objects: \(a,b,c,d:\wkcat{Lini}\) and the morphisms \[\begin{gathered} a \xrightarrow{f} b \xrightarrow{g} c \\ b \Clt{\xrightarrow{p}} d \Clt{\xrightarrow{q}} b \end{gathered}\] such that \(p \dcomp q = \id_b\) and \(q \dcomp p = \id_a\). In other words, \(p\) and \(q\) form a linear-and-thunkable isomorphism \(p : b \Clt\cong d\) such that \(p^{-1} = q\). This is depicted in the diagram below.
Theorem 5. The unital magmoid \(\wkcat{Lini}\) provides a counterexample to the above proposition. In particular, \(p : b \Clt\cong d\) is not intermediate.
Proof. The unital magmoid \(\wkcat{Lini}\) can be described explicitly in the following way. The type of objects \(\ob\wkcat{Lini}\) is, of course, the 4-element finite type \(\llbracket4\rrbracket\), whose elements I will write \(a,b,c,d:\wkcat{Lini}\). The hom-sets \(\morsof{\wkcat{Lini}}{x}{y}\) are given by the following table:
| \(\morsof{\wkcat{Lini}}{x}{y}\) | \(y=\) | \(a\) | \(b\) | \(c\) | \(d\) |
|---|---|---|---|---|---|
| \(x=\) | |||||
| \(a\) | \(\unit\) | \(\unit\) | \(\bool\) | \(\unit\) | |
| \(b\) | \(\ttempty\) | \(\unit\) | \(\unit\) | \(\unit\) | |
| \(c\) | \(\ttempty\) | \(\ttempty\) | \(\unit\) | \(\ttempty\) | |
| \(d\) | \(\ttempty\) | \(\unit\) | \(\unit\) | \(\unit\) |
This is rather opaque. We may instead write the elements more informatively as formal composites generated by \(f,g,p\) and \(q\).
| \(\morsof{\wkcat{Lini}}{x}{y}\) | \(y=\) | \(a\) | \(b\) | \(c\) | \(d\) |
|---|---|---|---|---|---|
| \(x=\) | |||||
| \(a\) | \(\{\id_a\}\) | \(\{f\}\) | \(\{[f\dcomp g], [[f\dcomp p]\dcomp[q\dcomp g]]\}\) | \(\{[f\dcomp p]\}\) | |
| \(b\) | \(\emptyset\) | \(\{\id_b\}\) | \(\{g\}\) | \(\{p\}\) | |
| \(c\) | \(\emptyset\) | \(\emptyset\) | \(\{\id_c\}\) | \(\emptyset\) | |
| \(d\) | \(\emptyset\) | \(\{q\}\) | \(\{[q \dcomp g]\}\) | \(\{\id_d\}\) |
The element \([f\dcomp g] : \morsof{\wkcat{Lini}}{a}{c}\) is just notation for, say \(\orgcode{false} : \bool\). Composition in \(\wkcat{Lini}\) is defined so that these formal composites do in fact denote the composition of the respective morphisms. In particular, we set \[\begin{aligned} f \dcomp g &\defequiv [f \dcomp g] : \morsof{\wkcat{Lini}}{a}{c} \end{aligned}\] and \[[f \dcomp p] \dcomp [q\dcomp g] \defequiv [[f \dcomp p] \dcomp [q\dcomp g]] : \morsof{\wkcat{Lini}}{a}{c}\] for the two non-\(\id\) cases which compose into \(\morsof{\wkcat{Lini}}{a}{c}\). All other composites are either vacuous or defined to be the single element \(\orgcode{tt} : \unit\), by whichever name it is given.
We may reassure ourselves that this does in fact construct \(\wkcat{Lini}\) as described initially, in that the morphisms of this construction are no more and no less than those generated by \(f\), \(g\) and linear-and-thunkable inverses \(p\) and \(q\). In most cases, it is easy to identify the composite in this construction with the corresponding formal-composite-of-morphisms-modulo-laws-and-assumptions. For example, we hypothesized that \(p\) and \(q\) are inverses in \(\wkcat{Lin}\), and we can compute that we have \[\begin{aligned} p \dcomp q &\equiv \id_b \\ q \dcomp p &\equiv \id_d\,. \end{aligned}\] More interestingly, we have \[\begin{aligned} [f \dcomp p] \dcomp q &\equiv f \\ p \dcomp [q \dcomp g] &\equiv g\,. \end{aligned}\] This too is as it should be for a construction of \(\wkcat{Lini}\). We must have \[(f \dcomp p) \dcomp q = f \dcomp (p \dcomp q)\] for \(q\) to be linear, and we must have \[f \dcomp (p \dcomp q) = f\] for \(p\) and \(q\) to be inverses. The case with \(g\) is analogous.
It is easy to verify that \(p\) and \(q\) are linear-and-thunkable. To do so,3 observe that for all \(x : \wkcat{Lini}\) we have that \(\morsof{\wkcat{Lini}}{b}{x}\) and \(\morsof{\wkcat{Lini}}{x}{d}\) are propositional (they are each either \(\ttempty\) or \(\unit\)). Thus all composites starting with \(p\) are equal, all composites ending with \(p\) are equal, and likewise for \(q\). Given this, we can see that \(p\) is a linear-and-thunkable isomorphism \(p : b \Clt\cong d\). Again, this is as it should be for a construction of \(\wkcat{Lini}\).
The linear-and-thunkable isomorphism \(p : b \Clt\cong d\) is not intermediate, however. This may be verified by the counterexample of the triple \[a \xrightarrow{f} b \xrightarrow{p} d \xrightarrow{[q \dcomp g]} c\] which does not associate. We can compute \[(f \dcomp p) \dcomp [q \dcomp g] \equiv [f \dcomp p] \dcomp [q \dcomp g] \equiv [[f \dcomp p] \dcomp [q \dcomp g]]\,,\] but \[f \dcomp (p \dcomp [q \dcomp g]) \equiv f \dcomp g \equiv [f \dcomp g]\,.\] These are the two distinct elements of \(\morsof{\wkcat{Lini}}{a}{c} \equiv \bool\). Thus the triple does not associate, and so \(p : b \Clt\cong d\) is not intermediate.
Footnotes
1 The name I use for myself on https://notes.eutro.dev is pronounced like the final syllable of my given name, but stressed.
2 An initialism of “Linear-and-thunkable Isomorphisms are Not (in general) Intermediate”
3 Sixty-four cases of computation are the easier solution on a computer.