The correspondence betwen nets and filters seems very reminiscent of the correspondence between fibrations and presheaves, especially the construction of a filter net as a directed system of pointed sets seems very similar to the Grothendieck construction

Is there any way to make this analogy more precise?

]]>I have been expanding at *net* a fair bit, also reformatting (more numbered environments) and re-arranging (more subsections, the order of some paragraphs reversed, where it seemed to help the reader).

Mainly I wanted to, and did, add statement and detailed proof of these four facts:

(The last of these statements I also copied to a stand-alone entry *compact spaces equivalently have converging subnet of every net*. )

Most of the other edits to the entry that I did were meant to make the statement of these proofs flow nicely. To that end for example I made explicit the classes of examples of directed sets that are needed in the proofs, in a Backgrounds-subsection “Directed sets”.

And since I added all these proofs in the subsection “Relation to topology” (now “Properties – Relation to topology”) I moved the plain definition of convergence of nets in topological spaces, which used to be there, to the section *Definition – Nets*.

At other places I simply expanded out the originally somewhat terse discussion to (hopefully) more easily readible text, such as in the section *Nets and filters*.

Finally, I considerably expanded the Idea-section.

All in all, while I did edit a lot, I tried to retain everything that used to be there, if maybe slightly re-arranged. But Toby should please check if he can live with the edits.

]]>I have touched *net*, just adding some more hyperlinks and cross-references within the page. Also *filter*, where I made *eventuality filter* come out as a link.