I seem to remember that at some point Ali Caglyan had created a whole lot of entries on the HoTT wiki which contained essentially nothing but classical definitions. Please do not mechanically copy these all over.

]]>Wait, there is nothing specific to homotopy type theory in what you just added. You are essentially just re-stating the usual definition.

It’s great that you are copying material from the HoTT-wiki, but let’s do it a little less mechanically, more with an eye towards retaining logic and cosistency of existing entries.

]]>adding additional text from HoTT wiki

Anonymous

]]>added text properly belongs in weak equivalence

Anonymous

]]>adding text from HoTT wiki

Anonymous

]]>Typo

Anonymous

]]>Right, this looks great. Thanks also for correcting my incorrect wording “weak factorization system”.

]]>Side point: the factorization system involving eso functors is not a weak factorization system in the sense usually meant, rather a “2-categorical” or “up-to-isomorphism” factorization system.

I added another paragraph to the page; does this at least partially say what you are getting at?

]]>Of course, but my intention was more, to treat both the strict factorization and weak factorization together and the difference is played precisely by insertint the mentioned equivalence. If b.o. and fully faithful make a strict factorization system then factorizing the same morphism as e.s.o. followed by the fully faithful is not unique as it amounts precisely to the replacement in the previous strict factorization system of the b.o. by any equivalent e.s.o. I agree that the surjectivity of $s$ is not needed above, but it is needed to make the factorization unique.

If I am just complicating what in others’ thoughts is useless exercise of trivivialities, never mind.

]]>We could say “any functor which is equivalent to a b.o. functor is e.s.o.”?

]]>Well the intention is that b.o. is e.s.o. up to equivalence and that was just making more precise version of one of the directions. I am not sure what is the best thing to organize.

]]>Okay, now I agree that it’s true. (-: I wouldn’t be inclined to include it as a “property of essentially surjective functors”, though, since it decomposes into two more “basic” properties: (1) if $f = j s$ and $f$ is essentially surjective, then so is $j$, and (2) an essentially surjective and fully faithful functor is an equivalence. Note that surjectivity of $s$ is not needed.

]]>I meant

if an essentially surjective functor $f$ factorizes as $j s$ where $s$ is surjective on objects AND $j$ fully faithful, then $j$ is an equivalence of categories.

Agreeing now ?

By the way – typo in the link in your post above – “bjective”.

]]>Thanks! I reorganized, added links to extant pages, and moved the material about bijective-on-objects functors to bjective on objects functor and bo-ff factorization system. I also removed

if an essentially surjective functor $f$ factorizes as $j s$ where $s$ is surjective on objects then $j$ is an equivalence of categories.

which doesn’t seem right at all to me, but I’m not sure what you meant to say.

]]>New entry in my personal lab, somewhat related to the above: compatible idempotent monads (zoranskoda)

]]>I added more details in essentially surjective functor. Please check for details (Mike?).

]]>