You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
James Deikun (Mar 20 2025 at 12:45):[[Rezk completion]] seems like it should be a reflection since it comes with a canonical map forgetting the inherent equality by weakening it to isomorphism and a [[univalent category]] seems like it would be a local object wrt maps that just weaken the inherent equality. However, in that case it's kind of surprising this isn't mentioned on either nLab page. Is this an oversight or is it not a reflection after all?
Jonas Frey (Mar 20 2025 at 13:24):Yes, univalent (-)categories are reflective in pre-(-)categories (aka Segal spaces in the -case), and the reflection operation is Rezk completion.