Commit 2021-04-06 01:49 4ddbdc1b

refactor(topology/sheaves): Refactor sheaf condition proofs (#6962) This PR adds two convenience Lemmas for working with the sheaf condition in terms of unique gluing and then uses them to greatly simplify the proofs of the sheaf condition for sheaves of functions (with and without a local predicate). Basically, all the categorical jargon gets outsourced and the actual proofs of the sheaf condition can now work in a very concrete setting. This drastically reduced the size of the proofs and eliminated any uses of simp. Note that I'm effectively translating the sheaf condition from Type into a Prop, i.e. using ∃! instead of using an instance of unique. I guess this diverts slightly from the original design in which the sheaf condition was always a Type. I found this to work quite well but maybe there is a way to phrase it differently.