Commit 2024-11-26 23:14 ba018bd9

refactor(CategoryTheory/Sites): remove SheafOfTypes (#19510) This PR removes the category SheafOfTypes.{u} J which was equivalent to Sheaf J (Type u), where J is a Grothendieck topology. This avoids some duplication of code, as SheafOfTypes was essentially a special case of Sheaf: the only difference was that the sheaf condition was phrased differently.