(Since these are anonymous edits, their author may not be reading the forum.)

]]>I have added a quick construction of the contravariant functor from finite sets to filters associated with a uniform structure, to the section “Categorical Intrepretation”.

Anonymous

]]>Added arXiv link to the recently added paper by Gavrilovich

]]>This last comment is pretty confusing to me. Why include the reference if you consider it not good?

]]>I have added a remark that
”
The original definition in Bourbaki can be seen as describing a contravariant functor from the category of finite sets to a category of filters of subsets.
”
and a reference to a paper describing the construction.
”
* {#naive_tame_topology} M. Gavrilovich, *A naive diagram-chasing approach to formalisation of tame topology* \S3.1.2, \S3.1.6.
“

Perhaps this has to be said differently because the reference is not good: the construction of the functor is trivial, but the sections cited are not self-contained and lack detail.

Anonymous

]]>Mention two closed monoidal structures on $Unif$, one symmetric and one not.

]]>On the assumption that this was a mistake (or left over from an initial attempt), I renamed it.

]]>Why is the title of this page “uniform space draft” and not “uniform space”?

]]>I found a reference that describes how to do quasiuniformities with covers: you have to use covers by pairs of sets. For instance, this paper contains a version of the definition for locales. I’ve added to uniform space a citation to what is apparently the original paper that does this, although I haven’t read it.

]]>Hmm… I thought I remembered there was a way to do quasiuniformities with covers, but I can’t find the book I thought it was in, and I can’t think right now of how you would do it. I edited the page to clarify.

]]>I was probably thinking of quasiuniformities, and I don't know how to do those with covers.

]]>uniform space says “The definition described above is based on entourages… There is an equivalent (but less directly generalisable) definition based on uniform covers.” In what way is the uniform cover definition less directly generalizable? Is it quasi-uniformities you had in mind? (There is a way to do those with covers, isn’t there, even if it’s more awkward?)

]]>@Mike #12:

Well, it is if you use enough adjectives. A point–point apartness space is a set equipped with a point–point apartness relation, a point–set apartness space is a set equipped with a point–set apartness relation; a set–set apartness space is a set equipped with a set–set apartness relation. Only the defaults are different (and even those defaults might vary with the author).

]]>Has anyone studied a constructive notion of an “antiuniform space”, i.e. a set equipped with a collection of “anti-entourages” that behave like the complements of the entourages in a classical uniform space?

]]>It’s very unfortunate that an “apartness space” is not the same as a set equipped with an “apartness relation”!

]]>http://dx.doi.org/10.1002/1521-3870%28200210%2948:1%2B%3C16::AID-MALQ16%3E3.0.CO;2-7

But while Mike #8 is about point–point apartness relations, Bridges is talking about point–set apartness and set–set apartness. I would say to see apartness space, but nobody has written that yet, so see proximity space and look for the apartness symbol ‘⋈’.

]]>This led me to the older paper

Bridges, D., Schuster, P. and Vîţă, L. (2002),

Apartness, Topology, and Uniformity: a Constructive View. Mathematical Logic Quarterly, 48: 16–28.

which has the ugliest and worst DOI I’ve ever seen. Link for cut/paste: `http://dx.doi.org/10.1002/1521-3870(200210)48:1+<16::AID-MALQ16>3.0.CO;2-7`

(I’m too lazy to look up the HTML codes for ) or `>`

, both of which appear in that url and would be used in either of the markdown link syntaxes. The raw text also breaks xml as the forum processes it >:-( [end rant] )

On looking up the constructivenews list, Google pointed me also at Bridges’ webpages (I didn’t know he was in New Zealand!), where I found his 2011 book Apartness and Uniformity, which might be of interest.

Publisher summary:

]]>The theory presented in this book is developed constructively, is based on a few axioms encapsulating the notion of objects (points and sets) being apart, and encompasses both point-set topology and the theory of uniform spaces. While the classical-logic-based theory of proximity spaces provides some guidance for the theory of apartness, the notion of nearness/proximity does not embody enough algorithmic information for a deep constructive development. The use of constructive (intuitionistic) logic in this book requires much more technical ingenuity than one finds in classical proximity theory – algorithmic information does not come cheaply – but it often reveals distinctions that are rendered invisible by classical logic.

In the first chapter the authors outline informal constructive logic and set theory, and, briefly, the basic notions and notations for metric and topological spaces. In the second they introduce axioms for a point-set apartness and then explore some of the consequences of those axioms. In particular, they examine a natural topology associated with an apartness space, and relations between various types of continuity of mappings. In the third chapter the authors extend the notion of point-set (pre-)apartness axiomatically to one of (pre-)apartness between subsets of an inhabited set. They then provide axioms for a quasiuniform space, perhaps the most important type of set-set apartness space. Quasiuniform spaces play a major role in the remainder of the chapter, which covers such topics as the connection between uniform and strong continuity (arguably the most technically difficult part of the book), apartness and convergence in function spaces, types of completeness, and neat compactness. Each chapter has a Notes section, in which are found comments on the definitions, results, and proofs, as well as occasional pointers to future work. The book ends with a Postlude that refers to other constructive approaches to topology, with emphasis on the relation between apartness spaces and formal topology.

Largely an exposition of the authors’ own research, this is the first book dealing with the apartness approach to constructive topology, and is a valuable addition to the literature on constructive mathematics and on topology in computer science. It is aimed at graduate students and advanced researchers in theoretical computer science, mathematics, and logic who are interested in constructive/algorithmic aspects of topology.

Moreover, if the uniform space is “located” as discussed in that thread, then the inequality is an apartness. I added a proof to uniform space, and a remark about this example to apartness relation.

]]>Now I see that Toby actually mentioned it here, but it didn’t make it onto the lab at that point.

]]>Interesting; that had not occurred to me before.

]]>I added a remark that every uniform space comes with an inequality relation.

]]>Looks great, thank you!

]]>Well, for now I’ve written in Axiom 0 by secretly translating it into the entourage language. There may be a slicker way to say it.

]]>