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.
For morphisms between -groupoids, essential surjectivity is equivalent to (-1)-connectivity. So one needs the -topos-version of -connectiveness, I’d think.
A functor between -categories is essentially surjective iff the induced functor between their cores is an effective epimorphism.
Isn’t the reference to simplicially enriched categories is superfluous here? Since the point is to invoke the homotopy category construction to reduce the question from -categories to that of -categories. I guess that passes the buck to whether you’re happy with the definitions of and defining “essentially surjective” for (1,1)-categories
Somebody like Mike Shulman or Emily Riehl might know more about the situation but I don’t think anybody has formally defined the homotopy category construction in simplicial type theory yet. Don’t know anything about infinity-cosmos theory so can’t comment on that.
1 to 5 of 5