mathlib3
4778e165 - chore(category_theory/sites/sheaf): rename sheaf to sheaf_of_types (#5458)

Commit
5 years ago
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.
Author
Parents
Loading