Same as the case for specialization order there is material duplicated from topological space in the dependent type theory section in this article.

Also, the definition given here about dependent type theory is really about correctly defining partial orders in dependent type theory rather than Kolmogorov topological space so I moved the technical details over to partial order and simply defined

A

Kolmogorov topological spaceor$T_0$-spaceis a topological space which is a partial order with respect to the specialization order of the topological space.

But then the above definition isn’t really specific to dependent type theory, so I ended up getting rid of the dependent type theory section completely and moved the definition into the alternate characterizations section as a proposition:

Raymond

]]>added section on Kolmogorov topological spaces in dependent type theory

]]>Rather than make a meal of the suggestion of my previous comment, I replaced the wrong sentence with something that is correct: that $T_0$-ness is equivalent to having the unit component of the standard adjunction between $Frame^{op}$ and $Top$ be a monomorphism.

]]>Martin, I wonder if sense can be made of Proposition 2.1 if we consider the continuation monad unit as living in a cartesian closed category containing $Top$ as a full subcategory, such as the category of pseudotopological spaces? There is a kind of intuitive sense lurking there, that $T_0$-ness means “open sets separate points”, and this is what 2.1 is groping to express.

]]>Just for the record: The statement of Prop. 2.1 was added in revision 6.

This is occasion to re-iterate #2: Not to add bare statements without an indication of their justification and/or a reference.

]]>fixed spelling

]]>2.7. uses word “neighther”. Is this a legitimate English word/spelling ?

]]>I just came across

So let’s add a reference, if not the argument itself.

]]>A simple characterization I just came across in some synthetic domain theory.

]]>