equivalences of quasi-categories

Stream: Infinity-Cosmos

[Rida Hamadani]

Is anybody working on defining equivalences of quasi-categories and proving Lemma 1.2.36? I plan to formalize this with help from Dalton Sakthivadivel and we want to check that nobody is working on it to avoid effort duplication.

[Emily Riehl]

Hi @Rida Hamadani; sorry to be slow.

We have an experimental definition of equivalence (of sorts) that can be found here. The idea of it would be to specialize to a particular interval (the coherent iso) and to the case where A and B are quasi-categories.

Whether it is a good idea to factor that specific notion of equivalence through this general framework is unclear to me, so feel free to ignore and start from scratch.

No one is working on lemma 1.2.36 I believe so that's all yours! Good luck and let us know if there's anything you want to discuss.