Commit 2021-04-03 11:15 76a3b82d

feat(topology/sheaves/sheaf_condition): Sheaf condition in terms of unique gluing (#6940) As in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Sheaf.20condition.20for.20type-valued.20sheaf This PR adds an equivalent sheaf condition for type-valued presheaves, which is hopefully more "hands-on" and easier to work with for concrete type-valued presheaves. I tried to roughly follow the design of the other sheaf conditions.