Here is a bit of hyperbole. Hopefully entertaining. Suppose, hypothetically, that category theorist X had a close look at the definition of "inverse": morphisms f : A -> B and g : B -> A are inverses if fg = id_B and gf = id_A. Suppose that she makes the following argument: "The definition of inverse is really too strict. It requires an equation between objects, namely, the domain of f must equal the codomain of g, and vice versa. A natural thing to do would be to weaken the definition to replace this equality by an isomorphism." So what definition would she come up with? Definition. Let f : A -> B be a morphism. A *weak inverse* of f is given by the following data: (1) Objects A', B', and a morphism g : B' -> A' (2) an isomorphism a : A' -> A (3) an isomorphism b : B' -> B (4) such that the following diagram commutes: g A' <------- B' a | | b v f v A --------> B Everybody can see that this is nonsense. First, one must have a prior definition of isomorphism before one can define inverse in this way. But the definition of isomorphism depends on inverses, so this is circular. Second, each "weak inverse" in the above sense already gives rise to an ordinary inverse, namely a o g o (b^{-1}). Perhaps category theorist X would like to formulate this as a Coherence Lemma ("each weak inverse is canonically equivalent to a strict inverse"). But it is clearly nonsense nevertheless. Naive attempts to define a weak version of dagger structure fall into the same category. Recall the definition of a dagger structure on a category, namely a contravariant, involutive, identity-on-objects functor. Or in elementary terms: to each f : A -> B, associate some f+ : B -> A, such that f++ = f, (fg)+ = (g+)(f+), and id+ = id. Each category theorist (including myself) who sees this definition immediately dislikes the identity-on-objects part. The first instinct is to try to weaken it. But what would one come up with? After one or two failed attempts, it seems that the "correct" definition is the following: a contravariant functor (-)+, and for each object A a chosen unitary isomorphism a_A : A+ -> A, such that one has the following diagram (but note that it doesn't have to commute): f+ A+ <------- B+ a_A | | a_B [not assumed to commute] v f v A --------> B Plus, there should be some further requirement to replace the "involutive" condition (i.e., the obvious diagram involving f and f++ should commute), and perhaps a coherence condition or two. Note that a_A and a_B must be assumed to be unitary. The analogous definition where they are just isomorphisms does not work for a variety of reasons. For example, this is supposed to be a weakening of the strict situation, and identities are always unitary. The problem with any such definition is the same as for the "weak inverses" hyperbole above. First, to define dagger in this way, one must have a prior definition of "unitary", but the definition of "unitary" depends on "dagger", so this is circular. Second, given any weak dagger structure in this sense, it already induces a strict dagger structure, namely by using a_A o f+ o (a_B^{-1}) : B -> A as the strict dagger. One could again regard this as a coherence lemma, but it's clearly a pointless one. Actually, my leading example of "weak inverses", while ludicrous, is not entirely besides the point. One of the main reasons for considering dagger structure is so that we can define a morphism u : A -> B to be unitary if u+ is the inverse of u. Trying to say this with the "weak" dagger structure inevitably leads to weak inverses. In light of all this, I completely agree with Mark Weber that dagger structure should be strict and that is what we should live with. -- Peter