Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
At equivalence of categories I added a simple example of a non-adjoint equivalence. Maybe it belongs in the page adjoint equivalence instead?
Hmm, I don’t know.
Why not both?
The wording of the definition in section 2 bothers me. I think it would be better to say “An equivalence consists of two functors and together with natural isomorphisms and ” – in other words make the natural isomorphisms part of the structure.
By defining it as a pair of functors satisfying a property, the next line about adjoint equivalences doesn’t really make sense, or is an empty statement that would imply that every equivalence is an adjoint equivalence. Because of course the data in any such equivalence form a pair of adjoint functors! Instead you want to say that the chosen isomorphisms are the counit and unit of an adjunction.
One also says that a functor is an equivalence (by abuse of language) if there are etc.
I agree with Todd; I hope no one minds that I modified the wording so that the data includes a specification of unit and counit.
I have added the missing clause “assuming AC” in this prop.
That clause is not necessary; that's the point of the following remark.
Mike, I'm pretty sure that you had some argument that a mere equivalence of categories should consists only of appropriate and , while an adjoint equivalence includes the natural isomoprhisms among the data. I'll try to find it.
Actually, it's right there in the page; search for the text ‘fraught with peril’, although the argument as it's written is weak. And apparently that was there in the original version, credited to me. But I don't think that I wrote it; I think that I must have borrowed it from somewhere. ETA: Mind you, the phrasing was probably mine, but I don't think that the idea was.
That remark still applies, with “axiom of choice” interpreted accordingly in the chosen foundation.
But what I am concerned with is that while you and me know this and can see that it is captured by this remark, a reader who is not already expert on these matters is bound to misunderstand what the entry says.
I am busy right now, but I’ll try to edit further later today, to make the entry satisfy both concerns.
That remark still applies, with “axiom of choice” interpreted accordingly in the chosen foundation.
No it doesn’t. The most radical version of this is that in HoTT the theorem is true if equivalence means “strong equivalence” but not assuming any axiom of choice. The point of the “Variants” section is that in other foundations it is true for weak equivalences (by definition) and anaequivalences (by construction) in arbitrary foundations without assuming any axiom of choice.
However, I agree that the remark doesn’t actually convey the desired information.
One example of the peril of considering a non-adjoint equivalence to be data is Steve Lack’s paper “A Quillen model structure for 2-categories”, in which his definition of the “equivalence-lifting property” for fibrations in 2Cat, and the generating acyclic cofibrations of the model structure, was incorrect due to this mistake. In “A Quillen model structure for bicategories” he corrected it.
That remark still applies, with “axiom of choice” interpreted accordingly in the chosen foundation.
No it doesn’t. The most radical version of this is that in HoTT the theorem is true if equivalence means “strong equivalence” but not assuming any axiom of choice.
Exactly, because the relevant axiom of choice is just true in that case.
Okay I have edited section “Definition” for clarity, and I have expanded the “Idea”-section to transport more of an idea.
Oh, and in the course of this I created a minimum at equivalence in a 2-category
If it’s “just true”, it’s not an axiom.
How far we have come in our postmodern relativism to say that something is not an axiom because it's just true!
But seriously, it is sometimes useful to use a redundant list of axioms, so something isn't barred from being added as an axiom because it's already a theorem. In HAF, Eric Schechter brings up the axiom of Finite Choice (that a finite family of inhabited sets has a choice function) for pedagogical purposes. And I sometimes find it helpful to notice that Excluded Middle is equivalent (in a strong enough set theory, that is one with full separation) to Kuratowski-Finite Choice (that a finitely indexed family of inhabited sets has a choice function), even though it is just true if you're already using classical logic (and even hard to distinguish from Finite Choice if you're not already used to noticing applications of Excluded Middle). So it makes sense to say that certain forms of the axiom of Choice are just true without having to strip them of the title of ‘axiom’ first.
Attempting to flesh out the context for the equivalence between equivalence and FF ESO, I searched for category theory in homotopy type theory and found a 2013 Café post by Mike about a contemporary paper with Benedikt Ahrens and Chris Kapulkin. So I linked to that, on the grounds that if there's anything better, then Mike would know.
If I’m talking about something that I know to be just true but that is a case of something otherwise called an axiom, I often call it a “principle” instead. For instance, the principle of unique choice, aka the principle of function comprehension, is true in set theory and in HoTT (though in CiC and logic-enriched type theory it is an axiom). Here the relevant principle is “functor comprehension”, which is likewise true in the relevant contexts and I would prefer not to call it an axiom. But even if you still call it an axiom, I think one should not say “assuming the axiom of choice” if one is in a context where it does not need to be assumed.
The present version of the theorem, though somewhat wordy, looks correct to me. (-:
Toby, please don’t put direct external links to references. For convenience of the reader and for robustness under link rot, cross references, errata etc., references should always be collected in a list in the References-section, and hyperlinks to resources included there. Even more so if the reference in question really deserves an Lab entry of its own: I have changed your link to point to the new entry internal categories in homotopy type theory.
1 to 21 of 21