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.
Quick page, analogous to walking isomorphism.
Just because I’m marking exams and can’t think about this right now: might it be worth doing the walking adjoint equivalence? It would presumably be a quotient of Adj, and there might be an interesting relationship between the walking equivalence and the walking adjoint equivalence, seeing at equivalences can (generally?) be upgraded to an adjoint equivalence (see Theorem 3.3 as numbered in the current version), at the cost of perhaps changing part of the data.
Thanks for chiming in! Absolutely! My recent edits are mainly building up to adding some material to the new page Lack fibration and some material on canonical model structures on higher categories; I think the walking adjoint equivalence will be needed for this.
I actually think that “the walking equivalence” should be an adjoint equivalence. I can’t think of any context in which one would want to use the walking non-adjoint equivalence. However, for the moment I refrained from making that change myself.
Thanks for the corrections! Writing very fast, as I have to due to circumstances, apologies!
Yes, if we could wait until I’m finished with the stuff I plan to add to Lack fibration before changing things with regard to walking equivalence vs walking adjoint equivalence, that would be great.
The walking equivalence is definitely worth a mention, though, even if the ’correct’ notion is the walking adjoint equivalence. Even if to point out it only works in some cases. Also, there’s connection to the HoTT definition of equivalence, where the information is packaged differently (an a priori distinct left and a right quasi-inverse etc), or some of the Riehl–Verity ideas around coherent adjunctions.
Yes, I agree, we should definitely mention it somehow. I guess Mike was thinking about what should be the default meaning of the term ’walking equivalence’; let’s disuss that a little further down the road!
Back to #5: I agree that as I stated it the representing functor is not unique, but I think we should strengthen the hypotheses a little to make it unique, at least up-to-something. I’ll have a think myself about how to do this a little later if nobody else gets to it; but if anyone has a preference for how to state it, please just go ahead,
Deleted the following remark as redundant, after the updating of the definition, which now states and are 2-isomorphisms up front.
The 2-arrows and are 2-isomorphisms, whose inverses are the 2-arrows and .
Regarding #5 and #10: I do feel that the definition is kind of cheating now! The purpose of the definition as I initially gave it was to give an explicit-as-possible description. What I wrote was not far from correct, just missing a couple of additional clarifications. We could give both phrasings, of course.
Re #12 yes, that seems good.
The walking non-adjoint equivalence is worth mentioning, but I don’t think it deserves its own page. The alternative definitions mentioned in #8 are all different constructions of the walking adjoint equivalence.
Re #9, the representing functor is by construction unique if we specify to begin with the entire (non-adjoint) equivalence data (a morphism, its quasi-inverse, and two witnessing 2-isomorphisms). If the original data is just a morphism with the property of being an equivalence, then the representing functor is not unique even up to anything I can think of – but if we used the walking adjoint equivalence then it would be unique up to unique isomorphism.
Tweaked the definition a bit to express it slightly more formally as a quotient of a free strict 2-category. Strengthened the hypotheses of the proposition about representability so that the representing functor is unique. Added the walking semi-strict equivalence. Observed that the walking semi-strict equivalence defines an interval which can be equipped with all the structures of my thesis, and hence that we obtain a ’canonical model structure’ on the category of strict 2-categories in which every object is both fibrant and cofibrant, where the fibrations and cofibrations are ’Hurewicz’ fibrations and cofibrations respectively with respect to the interval defined by the free-standing semi-strict equivalence. I will add more on this to a different page later.
This isn’t right either. Your contains composites like , but its underlying reflexive globular set doesn’t remember that these are in fact composites. So your contains the “” from as a generator, but also a new 1-cell that is actually the composite of the generators and in . And so on.
I think a more standard name for your “semi-strict equivalence” would be a “retract equivalence” (the categorical version of a deformation retract).
Can you describe explicitly the cofibrations, fibrations, and weak equivalences in this model structure?
1 to 17 of 17