daniel gratzer on Nostr: nprofile1q…d6kk0 I would be inclined to agree but it's really used *all the time* ...
nprofile1qy2hwumn8ghj7un9d3shjtnddaehgu3wwp6kyqpqjd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208raysyd6kk0 (nprofile…6kk0) I would be inclined to agree but it's really used *all the time* in oo-categorical proofs. It's so frequent that terminology for at least one direction is necessary (in the paper I'm reading now, something like 8 proofs in a row use various reductions of colimits using cofinal functors)