October Update 1
I have done a little bit of unwriting since my last post. My most recent (and I expect ~penultimate) draft is down all the way to 18 pages from 22, which is the limit for FoSSaCS. Paper submission is due on the 15th.
I achieved this shortening primarily without changing the content at all, but by removing Rocq definition links, changing the font (pdflatex didn’t support the original font anyway), and plenty of rephrasing. I also removed a couple diagrams and un-displayed some maths, but hopefully the damage to legibility is minimal. I have also made some reorganisations and updated the introduction.
I removed definition links because they either look horrendous, take
up too much space, or both. One thing I tried was putting them in the
margin. However, some of my theorem names are really long, like
is_duploid_univalent_from_positive_thunkable_and_negative_linear_categories
and
split_essentially_surjective_negative_category_to_envelope_duploid
which spanned four lines in the margin even with \scriptsize. It is
made especially horrendous by hyperref highlighting with a blue
square, but I don’t think it’s looks as bad in print. \marginpar-s
also sometimes go on the wrong side of the page. I could potentially
put file and line number in the margin, or even just a rooster logo,
but it would pain me to have the content only accessible in digital
copies, or for the reference to be tied to a specific
version. Artifact submission would be later anyway, but perhaps I
ought to include an anonymized Zenodo reference already?
Upstreaming Duploids
I have begun preparing my formalization for submission into the main UniMath canon, now that it is moving away from being my blackboard.
The most fundamental change I am making is my treatment of the
linear/thunkable/intermediate subcategories. Writing up my thesis
inspired me to create a wide_submagmoid abstraction for the l/t/i
subscripts I put on morphisms/isomorphisms/unital magmoids to indicate
linearity, thunkability and intermediateness. wide_submagmoid is
essentially the same as a displayed unital magmoid whose object part
is unit and morphism part is propositional, and is thus still
considerably specialized to my use-case (in a good way, I think).
The abstraction should make the differing univalence conditions of (split) (pre)duploids and unital magmoids easier to state and use, and hopefully bring some code reuse in areas involving the submagmoids (e.g. inclusions, isomorphisms, and in the future natural transformations).
Universal Properties in Unital Magmoids
While shortening my proof of uniqueness of polarity shifts, I inadvertently proved a simple uniqueness property for universal properties in unital magmoids. I reproduce it here (but it is nicer in the typeset version c;).
Lemma 1. For a univalent unital magmoid \(\D\) and object \(a : \D\), the types \(\sum_{b:\Cn\D}(b \Cl\cong a)\) and \(\sum_{b:\Cp\D}(a \Ct\cong b)\) are propositions.
Proof. Let \(\langle b, b \Cl{\overset{e}\cong} a \rangle\) and \(\langle b’, b’ \Cl{\overset{e’}\cong} a \rangle\) of the former type. Then \(\langle b, e \mathbin; e’^{-1} \rangle =_{\ifan{\Clti\D}{b}} \langle b’, \id_{b’} \rangle\) by the fundamental theorem of identity types. It follows that \(b = b’\) and \(e = e’\).
Theorem 2. For a univalent preduploid \(\D\), the type “\(\D\) is a duploid” is a proposition.
Proof. The data \(\langle {\Uparrow}{a}, \mathsf{force}_a \rangle\) and \(\langle {\Downarrow}{a}, \mathsf{wrap}_a \rangle\) are of the types in Lemma 1.
Remark 3. In unital magmoids, natural isomorphisms \(\morsof\M{-}{a} \cong \morsof\M{-}{b}\) are linear isomorphisms \(a \Cl\cong b\). Thus, by contrast to representability in categories, Lemma 1 suggests that non-functorial maps \(F : \M^\op \to \Set\) may be uniquely represented by negative objects \(b : \Cn\D\) satisfying \(\morsof\M{-}{b} \cong F\), and dually for positive objects. In that sense, the polarity shift structure of duploids thus amounts to saying that all \(\morsof\D{-}{b}\) and \(\morsof\D{a}{-}\) are representable, by \(\langle {\Uparrow}{b}, \mathsf{force}_b \rangle\) and \(\langle {\Downarrow}{a}, \mathsf{wrap}_a \rangle\) respectively.
It may be questionable how useful and well-justified “representable” is with this definition, but it does line up fantastically with what polarities ought to mean. I have not discovered a truly marvelous proof of Yoneda’s lemma for unital magmoids which the margin is too narrow to contain. Nevertheless, I have a weird definition of (slightly) natural transformation and functor with which \(\mathrm{WeirdNatTrans}(\morsof\M{-}{x}, F) \simeq Fx\) holds for negative \(x : \Cn\M\) and \(F \colon \M^\op \to \Set\) (and in particular \(\mathrm{WeirdNatTrans}(\morsof\M{-}{x}, \morsof\M{-}{y}) \simeq \morsof\M{x}{y}\), for any \(y : \M\)). I do not like it at all. It involves functors \(F\) needing only to satisfy \(F(f \mathbin; g) = Ff \mathbin; Fg\) when \(g\) is thunkable (in \(\M\)), and natural transformations \(\alpha\) where \(\alpha_x \mathbin; Ff = Gf \mathbin; \alpha_y\) need only hold for thunkable \(f\). These are satisfied by \(\morsof\M{-}{x}\) and \(\morsof\M{-}{f}\). The equivalence needs negativeness of \(x\) since otherwise the weird natural transformation cannot be proven to be determined entirely by its action on \(\id_x\). There is a similar property for graph morphism adjunctions (Proposition 5.3 [1]) and I do not like that either.