Commit 2021-12-02 19:28 4cfe637b
View on Github →chore(category_theory/sites/*): Adjust some simp lemmas. (#10574)
The primary change is removing some simp tags from the definition of sheafify and friends, so that the sheafification related constructions are not unfolded to the plus constructions.
Also -- added coercion from Sheaves to presheaves, and some rfl simp lemmas which help some proofs move along.
Some proofs cleaned up as well.