!4#5647 : colimits and yoneda

Stream: PR reviews

[Nikolas Kuhn]

I made the PR #5647, which relates cocones over a sieve S with families of objects for yoneda preshaves, and shows that a sieve over X realizes X as a colimit if and only if all yoneda presheaves are sheaves. This is needed for the results of the Copenhagen Masterclass.

[Riccardo Brasca]

I've left a couple of cosmetic comments, but LGTM, thanks!

[Nikolas Kuhn]

Thanks for the review! I implemented the suggestions.

[Nikolas Kuhn]

Ready to be merged if I get the go-ahead...