2 ms·
I found this pretty unclear to be honest. I was a little thrown off by the model for a Minecraft world (subset of Z3*N is a bad model because it allows invalid
by dan-robertson 5y ago
I found this pretty unclear to be honest.
I was a little thrown off by the model for a Minecraft world (subset of Z3*N is a bad model because it allows invalid worlds where two blocks occupy the same space. A better model is elements of N^Z3) but whatever.
And for the rest I struggled to motivate the definitions because it seemed something much simpler would do (the simple thing being something like “take the function f: B -> P(E) from the basis to sets of entities plus the injectivity-like condition that f(U) meets f(V) only if U=V, and then extend it to a function from the whole space in the obvious way”). Perhaps the machinery is only necessary when the topology is more interesting (the one in the article being a coarse discrete topology where everything is countable and countable intersections of open sets give open sets) or if the “data” has a more interesting structure than sets with inclusion.
I was also pretty confused about the need for F to be a functor. The article says it is a functor and then that it could be a function but also that it couldn’t. I found it most unclear. I think the article was trying to go on a counterfactual where F is not a functor, then define res_U^V and then reveal that it is just the image of the inclusion U->V under the functor, but it wasn’t clear to me which of its properties are just due to it being a functor and which are separate.
I was also thrown off by some errors (eg getting a subset relation the wrong way round) and I think the choice of variables was not great for subtle reasons:
1. I think it is often not great to have V’ < V (or vice versa) as I think there isn’t a natural order for the two names. Better to have something alphabetical like U < V or hierarchical like U_i < U. But this might just be my personal preference.
2. V was doing double-duty talking sometimes about elements in the domain of F and other times about elements in the image. I think it would be better if e.g. U was always in the domain and V in the image.
I also found the sentence structure confusing in a few cases but it may just be that I am not used to it. For example instead of “if x holds P(x) then Q(x)” I would have preferred “let x. If P(x) then Q(x)” or “given x such that P(x), we have Q(x).”