## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorjesse
• CommentTimeMay 1st 2017

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeMay 1st 2017

Hmm, I don’t know.

• CommentRowNumber3.
• CommentAuthorDavidRoberts
• CommentTimeMay 1st 2017

Why not both?

• CommentRowNumber4.
• CommentAuthorTodd_Trimble
• CommentTimeMay 2nd 2017

The wording of the definition in section 2 bothers me. I think it would be better to say “An equivalence consists of two functors $F: C \to D$ and $G: D \to C$ together with natural isomorphisms $e: F \circ G \cong Id_D$ and $h: Id_C \cong G \circ F$” – 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 $F, G$ in any such equivalence form a pair of adjoint functors! Instead you want to say that the chosen isomorphisms $e, h$ are the counit and unit of an adjunction.

One also says that a functor $F: C \to D$ is an equivalence (by abuse of language) if there are $G, e, h$ etc.

• CommentRowNumber5.
• CommentAuthorjesse
• CommentTimeMay 2nd 2017

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.

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeMay 2nd 2017

I have added the missing clause “assuming AC” in this prop.

• CommentRowNumber7.
• CommentAuthorTobyBartels
• CommentTimeMay 3rd 2017

That clause is not necessary; that's the point of the following remark.

• CommentRowNumber8.
• CommentAuthorTobyBartels
• CommentTimeMay 3rd 2017

Mike, I'm pretty sure that you had some argument that a mere equivalence of categories should consists only of appropriate $F$ and $G$, while an adjoint equivalence includes the natural isomoprhisms among the data. I'll try to find it.

• CommentRowNumber9.
• CommentAuthorTobyBartels
• CommentTimeMay 3rd 2017
• (edited May 3rd 2017)

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.

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeMay 4th 2017
• (edited May 4th 2017)

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.

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeMay 4th 2017

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.

• CommentRowNumber12.
• CommentAuthorMike Shulman
• CommentTimeMay 4th 2017

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.

• CommentRowNumber13.
• CommentAuthorUrs
• CommentTimeMay 4th 2017

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.

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeMay 4th 2017

Okay I have edited section “Definition” for clarity, and I have expanded the “Idea”-section to transport more of an idea.

• CommentRowNumber15.
• CommentAuthorUrs
• CommentTimeMay 4th 2017

Oh, and in the course of this I created a minimum at equivalence in a 2-category

• CommentRowNumber16.
• CommentAuthorMike Shulman
• CommentTimeMay 4th 2017

If it’s “just true”, it’s not an axiom.

• CommentRowNumber17.
• CommentAuthorTobyBartels
• CommentTimeMay 8th 2017

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.

• CommentRowNumber18.
• CommentAuthorTobyBartels
• CommentTimeMay 8th 2017

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.

• CommentRowNumber19.
• CommentAuthorMike Shulman
• CommentTimeMay 9th 2017

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. (-:

• CommentRowNumber20.
• CommentAuthorUrs
• CommentTimeMay 9th 2017

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 $n$Lab entry of its own: I have changed your link to point to the new entry internal categories in homotopy type theory.

1. adding proof in the context of homotopy type theory

Anonymous