February Update 2
This week I had a stab at stating the univalence condition for duploids, and seeing what I can do with it.
Univalence of Duploids
I am reasonably certain about a good definition of univalence in Duploids, so let’s state it. In the below, let \(\M\) be a unital magmoid, and \(a, b\) be objects of \(\M\), unless otherwise bound.
Inverses and Isomorphisms
Definition 1. A morphism \(f : a \to b\) has an inverse if there is a morphism \(g : b \to a\) such that \(f \cdot g = \id_a\) and \(f \cdot g = \id_a\). For \(P\) one of linear, thunkable or linear-and-thunkable, we say that \(f\) “has a \(P\) inverse” when \(g\) is moreover \(P\).
Proposition 2. Though “having an inverse” is not a mere proposition, “having a \(P\) inverse” in the definition above is a mere proposition.
Definition 3. For \(P\) one of linear, thunkable or linear-and-thunkable, a morphism \(f : a \to b\) is a \(P\)-isomorphism whenever \(f\) is \(P\) and has a \(P\) inverse. Equivalently, when \(f\) is an isomorphism in the \(P\) subcategory of \(\M\).
\(P\)-isomorphisms being isomorphisms in a category is helpful: it is immediately obvious that “being a \(P\)-isomorphism” is a mere proposition, and that \(P\)-isomorphisms are closed under identities, composition and taking inverses.
Linear-and-thunkable isomorphisms are particularly well-behaved in a couple of respects, as witnessed by the lemmas below. Let \(a \cong_{lt} b\) denote the type of linear-and-thunkable isomorphisms between \(a\) and \(b\) for any \(a\) and \(b\), and for \(p : a \cong_{lt} b\) let \(p^{-1} : b \cong_{lt} a\) denote its inverse.
Lemma 4. Given a linear-and-thunkable isomorphism \(p : a \cong_{lt} b\), \(a\) is positive if and only if \(b\) is positive, and \(a\) is negative if and only if \(b\) is negative.
Proof. Without loss of generality, we need only prove that \(a\) being positive implies that \(b\) is positive. By definition, this is that for any object \(c\) any morphism \(f : b \to c\) is linear. We have \(f = \left(b \xrightarrow{p^{-1}} a \xrightarrow{p} b\right) \xrightarrow{f} c = b \xrightarrow{p^{-1}} \left(a \xrightarrow{p} b \xrightarrow{f} c\right)\), which reassociates because \(p^{-1}\) is thunkable, and is linear because \(p^{-1}\) is linear and \(a\) is positive.
Lemma 5. Let \(\D\) be a preduploid and \(a \xrightarrow{f} b \xrightarrow{p} c \xrightarrow{g} d\) be objects and morphisms in \(\D\). If \(p\) is a linear-and-thunkable isomorphism, then the triple \((f,p,g)\) associates, in the sense that \(\left(a \xrightarrow{f} b \xrightarrow{p} c\right) \xrightarrow{g} d = a \xrightarrow{f} \left(b \xrightarrow{p} c \xrightarrow{g} d\right)\).
Proof. Recall that in a preduploid, each object is merely positive or negative (or both). Equality of morphisms is a proposition, so we can analyse the cases of the polarities of \(b\) and \(c\). The only case where the triple does not automatically associate is when \(b\) is positive and \(c\) is negative. But by the above lemma, this implies that \(b\) and \(c\) are both negative-and-positive, which provides associativity again.
The above lemmas are reassuring when defining a univalence condition for (pre)duploids, since it informally suggests that we have captured enough of the duploid’s properties so that linear-and-thunkable isomorphisms behave similarly to identities, and linear-and-thunkably-isomorphic objects behave similarly to each other. The latter lemma also differentiates preduploids from unital magmoids, in that linear-and-thunkable isomorphisms do not appear to have this property in general unital magmoids. This is exciting, because I finally know what the property is useful for, but disappointing because it makes the theory of unital magmoids even less nice than I would like.
Definition of Univalence
PermalinkDefinition 6. A single-sorted preduploid \(\D\) is univalent if the canonical map \(\orgcode{id\_to\_lt\_iso} : \prod_{a,b:\ob\D} a =_{\ob\D} b \to a \cong_{lt} b\) given by path induction is an equivalence.
Lemma 7. Given a single-sorted preduploid \(\D\), the following are equivalent:
- \(\D\) is univalent.
- The linear-and-thunkable subcategory \(\Clt\D\) is univalent.
- The subcategories \(\Cpt\D\) and \(\Cnl\D\) are univalent.
Proof. \((1 \leftrightarrow 2)\): 2 is just a restatement of what it is to be a linear-and-thunkable isomorphism.
\((2 \to 3)\): the inclusion functor \(\Cpt\D \to \Clt\D\) is fully faithful, so in particular the isomorphisms \(a \cong b\) in \(\Cpt\D\) are precisely the isomorphisms in \(a \cong b\) in \(\Clt\D\).
\((3 \to 2)\) (sketch of the horrors) being an equivalence is a
proposition, so we can case-analyse the polarity of \(a\). Suppose
without loss of generality that \(a\) is positive. When we see an
isomorphism \(a \cong_{lt} b\) we can conclude that \(b\) is also
positive. This means any isomorphism \(a \cong_{lt} b\) in \(\Clt\D\)
is also in \(\Cpt\D\), which is univalent. The horrors arose from
trying to obtain the linear-and-thunkable isomorphism nicely, and
fending off weird transports over the polarity proofs (??). I got out
of this hell using reflexive graphs and one of my favourite-named
lemmas, isaprop_assume_it_is : (X -> isaprop X) -> isaprop X, with
this beautiful two-column layout proof 1.
Consequences of Univalence
There are a few things we would immediately like to be true in a univalent duploid. The first is that universal properties such as polarity shifts should become mere propositions. The second is that (adjoint) equivalences between duploids should be equivalent paths between the duploids. These results both turn out to be true, as we would hope.
Propositionality of Shifts
Definition 8. A negative shift on a unital magmoid \(\M\) is given by, for each object \(a : \M\), a negative object \(\upshift a\), a linear morphism \(\force_a\) and a linear inverse to \(\force_a\) called \(\delay_a\). Dually, a positive shift is given, for each object \(a : \M\), by a positive object \(\downshift a\), a thunkable morphism \(\wrap_a\) and a thunkable inverse to \(\wrap_a\) called \(\unwrap_a\).
By definition, \(\upshift a\) being negative makes \(\delay_a\) thunkable, and \(\downshift a\) being positive makes \(\unwrap_a\) linear, moreover \(\force a\) is thunkable if and only if \(a\) is negative, and \(\wrap a\) is linear if and only if \(a\) is positive.
Lemma 9. Polarity shifts are unique up to linear-and-thunkable isomorphism.
Proof. Without loss of generality, I prove only the negative shift case. Let \(\M\) be a unital magmoid, and let \((\upshift,\force,\delay)\) and \((\upshift’,\force’,\delay’)\) be two negative shift structures on \(\M\). Then for any object \(a : \M\) we have \(\upshift a \cong_{lt} \upshift’ a\), witnessed by \(\upshift a \xrightarrow{\force_a} a \xrightarrow{\delay’_a} \upshift’ a\) and \(\upshift’ a \xrightarrow{\force’_a} a \xrightarrow{\delay_a} \upshift a\).
This is good news, since linear-and-thunkable isomorphisms become paths in the univalent duploid! We thus have the following result.
Lemma 10. Having polarity shifts is a mere property of a univalent preduploid.
Proof. Once again, without loss of generality, I prove only the negative shift case. The linearity, negativity, and having-a-linear-inverse properties of the negative shift are mere propositions even without univalence, only \((\upshift, \force)\) and \((\upshift’, \force’)\) remain to be identified. Fixing an object \(a\), \(\upshift a\) and \(\upshift’ a\) are identified immediately by the lemma above and univalence. Transporting across the resulting path amounts to (pre)composing \(\force_a\) with the isomorphism, reducing to \(\left(\upshift’ a \xrightarrow{\force’_a} a \xrightarrow{\delay_a} \upshift a\right) \xrightarrow{\force_a} a = \upshift’ a \xrightarrow{\force’_a} a\), which evidently holds.
This is helpful, because it means that duploids have the same structure as categories, just with different properties.
Characterizing Paths Between Univalent Duploids
We would now like to characterise the paths between univalent
duploids. Isomorphisms of the underlying objects, morphisms,
identities and composition, which already exist in UniMath
(e.g. catiso) should be usable out of the box for univalent
duploids. Right?
Definition 11. An equivalence of duploids is a fully-faithful functor \(F : \D \to \D’\) which is surjective on objects up to linear-and-thunkable isomorphism.
Proposition 12. An equivalence of duploids \(F : \D \to \D’\) can be inverted to another equivalence of duploids \(F : \D’ \to \D\).
The construction goes off without a hitch the same as it does in ordinary category theory, the linear-and-thunkable isomorphisms essentially make everything associate.
PermalinkDefinition 13. An isomorphism of categories (catiso) is a fully-faithful functor
which is an equivalence on objects.
(In fact, this is an isomorphism of the structure of the category, the
precategory_data. An isomorphism of “pointed magmoids”, if you
will.)
Definition 14. A pointed magmoid (precategory_data) is a category without
identity or associativity laws for composition. It is equivalently a
magmoid with a distinguished loop at each object, or a reflexive graph
with a binary operator.
Lemma 15. Isomorphisms of categories are equivalent to equivalences of duploids, when restricted to univalent duploids.
Proof. A functor being an isomorphism of categories is always a mere proposition, and being an equivalence of duploids is a mere proposition when the duploids are univalent. Thus we need only show that a fully-faithful functor being surjective up to linear-and-thunkable isomorphism is logically equivalent to being an equivalence on objects.
\(({\rightarrow})\) Being surjective up to linear-and-thunkable isomorphism allows obtaining the inverse equivalence, which makes it an isomorphism on objects.
\(({\leftarrow})\) Being an equivalence makes the functor surjective, and hence surjective up to linear-and-thunkable isomorphism.
To complete the characterization, we need one more step.
Proposition 16. Isomorphisms of categories correspond to paths on the underlying pointed magmoid.
This should be routine, but I did not find a usable proof within
UniMath . I eventually built up the precategory_data from
univalent reflexive graphs, and then the edges are obtained from
reassociating the data of the catiso, none of which causes
issues. The hardest part was commuting and associating the various
properties of duploids that make other things properties. The type
univalent_duploid currently looks about like this:
Goal univalent_duploid = ∑ D : ∑ M : ∑ M : ∑ M : ∑ y,
is_unital_premagmoid (y : precategory_data),
has_homsets (pr1 M),
has_polarities (pr1 M),
has_polarity_shifts (pr1 M),
is_duploid_univalent (pr11 D).
reflexivity.
Qed.
Now, this does not work immediately as a reflexive graph:
is_unital_premagmoid is not a proposition until we know it
has_homsets, so they need to be commuted to make the univalent
reflexive graph of unital_magmoid-s. has_polarities is fine where
it is since it’s always a proposition, but has_polarity_shifts is of
course only a proposition once we know that it is_duploid_univalent,
so that needs to be commuted too. Fortunately, we are perfectly able
to construct the univalent reflexive graph with the displayed nonsense
in the correct order to make everything a proposition at the right
time. Then we can construct the univalent_duploid reflexive graph
that is equivalent (as a reflexive graph) to that one, which is
therefore univalent using the univalent reflexive graph of reflexive
graphs (in the next universe up of course, but in current
UniMath I do not need to fight the type checker over this, for
better or for worse).
This does mean I now have a formalization of part of reflexive graphs in UniMath . This should make some proofs about univalence easier, both by using displayed and total reflexive graphs to avoid transports, and by the fundamental theorem of identification types making it easier to prove properties about things that are univalent, even when not built up out of reflexive graphs. For example, every category contains the reflexive graph of its objects and isomorphisms, whose univalence condition as a reflexive graph is (definitionally!) equal to the univalence condition for the category. This made it less painful to prove that a duploid is univalent from its subcategories being univalent, for example.
Next Steps
- I have clearly not actually defined any sort of adjoint equivalences, because I haven’t even stated my 2-cells yet! The existing equivalences as fully-faithful essentially surjective functors are plenty to play around with for now, and the correspondence to a 2-category equivalence should intuitively work out. I would love to explicitly formalize and study the 2-category of duploids at some point.
- I called polarity shifts universal properties earlier, even though
the definition contains no
∃!. I have made this precise by defining them by the universal property found in [1] too, and proving them equivalent, but I have not written this up yet. The universal properties look like they should be more amenable for proving the shift functor adjunctions, so I will probably write about those when I get back to those. - Thinking continues about how to construct a univalent duploid from an adjunction. Characterizing and observing univalence for a duploid in more ways may be helpful to discover what the construction might need to look like (although, circularly, thinking about a possible univalent construction also gives interesting ideas for what univalence should look like).
References
Footnotes
1 The two sides of the proof would of course dualize just as beautifully with regular expressions, but I chose a DRYer way to amuse myself today.