Commit 2024-12-13 10:51 df86f595
View on Github →feat(CategoryTheory/Sites): the property of being a sheaf of types is invariant under natural equivalences (#19921)
If P₁ : Cᵒᵖ ⥤ Type w and P₂ : Cᵒᵖ ⥤ Type w' are naturally equivalent presheaves of types (in possibly different universes), then P₁ is a sheaf for a Grothendieck topology iff P₂ is.