Commit 2020-12-21 07:48 4778e165

chore(category_theory/sites/sheaf): rename sheaf to sheaf_of_types (#5458) I wanted to add sheaves with values in general categories, so I moved sheaf.lean to sheaf_of_types.lean and then added a new file sheaf.lean. Github then produced an incomprehensible diff file because sheaf.lean had completely changed. Hence I propose first moving sheaf.lean to sheaf_of_types.lean and then adding a new sheaf.lean later. As well as moving the file, I also slightly change it.