May Update 1
I have written the bulk of the background chapter of my dissertation, these past few days spent writing the section titled “Mixed Evaluation Order.” I went back-and-forth on whether to put this section before or after the other two sections (currently titled “Preliminary Type Theory” and “Univalent Categories and Reflexive Graphs,” despite a stark lack of Reflexive Graphs in the latter…). I have decided to put it first, because it flows on nicer from the introduction and motivation, and means we can forget about the syntax of these non-associative languages as soon as we have mentioned them.
I have written all the sections of the background and introduction, but have not yet had the opportunity to rewrite them to fit a completely coherent narrative. I believe they are legible, mostly stand on their own (except the new section which I feel is a bit weak), and cover most of the background I think I should need. The version at time of writing may be read here. I still include many notes and TODOs, if you can forgive me.
Yoneda and Univalence of Unital Mamoids
I have finally found some use of the barely salvageable Yoneda lemma which so horribly fails for unital magmoids. In particular, I can use this to show that linear-and-thunkable-and-intermediate isomorphisms correspond to the indiscernibilities derived mechanically by Ahrens et al. [1]. I did this because I was dreading writing down the univalence principle for unital magmoids without being sufficiently reassured that it is the correct notion.
Part of the Yoneda lemma for categories is that the Yoneda/post-composition functor \(\yo(a : \C) \defequiv \morsof\C{-}{a} : [\C^\op, \Set]\) is fully-faithful. As a consequence, morphisms \(a \to b\) are in correspondence with natural transformations \(\morsof\C{-}{a} \Rightarrow \morsof\C{-}{b}\), and isomorphisms \(a \cong b\) are in correspondence with natural isomorphisms \(\morsof\C{-}{a} \cong \morsof\C{-}{b}\).
Unfortunately, in a unital magmoid most of this fails, but we can scrape back some useful corollaries even in the absence of a full (i.e. nicely stated) Yoneda lemma.
Lemma 1. In a unital magmoid \(\M\), the morphism \(f : \morsof\M{a}{b}\) is linear if and only if the post-composition transformation \((g \mapsto g \dcomp f) : \morsof\M{-}{a} \to \morsof\M{-}{b}\) between reflexive graph functors \(\morsof\M{-}{a} : \M^\op \to \Set\) is natural.
Proof. This is amounts to unfolding the definition of naturality.
Lemma 2. The Yoneda/post-composition functor restricted to linear morphisms \(\Cl\yo(a : \Cl\M) \defequiv \morsof\M{-}{a} : [\M^\op, \Set]\):
- Preserves composition (i.e. is a functor of unital magmoids, not just reflexive graphs).
- Has as codomain the category \([\M^\op, \Set]\) of reflexive graph functors \(\M^\op \to \Set\) and natural transformations.
- Is fully-faithful.
Proof. Following your nose (um_yoneda_linear_fully_faithful).
Remark 3. This is a little bit stronger than just applying Yoneda’s lemma to the linear subcategory \(\Cl\M\), because only one of the hom-sets in the entire equation is forced to be linear.
Corollary 4. Linear isomorphisms \(a \Cl\cong b\) in \(\M\) are equivalently natural isomorphisms \(\morsof\M{-}{a} \cong \morsof\M{-}{b}\).
Proof. This follows from usual properties of fully faithful functors.
Corollary 5. Thunkable isomorphisms \(a \Ct\cong b\) in \(\M\) are equivalently natural isomorphisms \(\morsof\M{a}{-} \cong \morsof\M{b}{-}\).
Proof. This is formally dual to the previous statement.
Theorem 6. Linear-and-thunkable-and-intermediate isomorphisms \(a \Clti\cong b\) in a unital magmoid \(\M\) correspond to indistinguishabilities \(a \asymp b\) obtained by following the procedure of Ahrens et al. [1].
Proof. Our diagram signature is exactly the same as categories, but we do not impose the associativity axiom. Therefore most of the extended example in chapter 3 [1] applies. One can verify that the data and properties (3.13–3.26) of indiscernibilities in section 3.4 correspond to a linear-and-thunkable-and-intermediate isomorphism. The data of an indiscernibility \(a \asymp b\) includes a natural isomorphism in the codomain (3.13, 3.16) \(\morsof\M{-}{a} \cong \morsof\M{-}{b}\), hence a linear isomorphism \(p : a \Cl\cong b\); and a natural isomorphism in the domain (3.14, 3.18) \(\morsof\M{a}{-} \cong \morsof\M{b}{-}\), hence a thunkable isomorphism \(q : a \Ct\cong b\). These are forced to be the same by the equation \((f \dcomp p) \dcomp (q^{-1} \dcomp g) = f \dcomp g\) for all \(x \xrightarrow{f} a \xrightarrow{g} z\) (3.17), and the same property also forces the isomorphism to be intermediate. Thus we have \(p = q : a \Clti\cong b\). The last bit of data is an identity-preserving isomorphism (3.15, 3.23) \(\morsof\M{a}{a} \cong \morsof\M{b}{b}\) which is forced to be \(f \mapsto p^{-1} \dcomp f \dcomp p\) (3.19–3.21). The remaining properties (3.22–3.23, 3.24–3.26) are automatic.
This justifies the following definition.
Definition 7. A unital magmoid \(\M\) is univalent when the linear-and-thunkable-and-intermediate subcategory \(\Clti\M\) is univalent.
We already know that this coincides with univalence for preduploids 🙂.