mathlib

8bb0b6f7 - feat(category_theory/sites/plus): If P is a sheaf, then the map from P to P^+ is an isomorphism. (#10297)

feat(category_theory/sites/plus): If P is a sheaf, then the map from P to P^+ is an isomorphism. (#10297) Also adds some simple results about (co)limits where the morphisms in the diagram are isomorphisms. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>