feat(category_theory/sites): category of sheaves on the trivial topology  (#5651)
feat(category_theory/sites): category of sheaves on the trivial topology  (#5651)

Shows that the category of sheaves on the trivial topology is just the category of presheaves.




leanprover-community/mathlib,leanprover-community/mathlib