Commit 2023-11-12 15:48 bac379fd

feat(CategoryTheory): a version of sheafCompose for functors preserving smaller limits (#8235) Introduces a new typeclass GrothendieckTopology.HasSheafCompose F which says that a sheaf postcomposed with the functor F is still a sheaf. The previous API proved that a functor preserving certain limits has this property, this PR also adds a proof that a functor preserving limits of a smaller size has this property.