Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I just came across
So let’s add a reference, if not the argument itself.
2.7. uses word “neighther”. Is this a legitimate English word/spelling ?
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.
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 as a full subcategory, such as the category of pseudotopological spaces? There is a kind of intuitive sense lurking there, that -ness means “open sets separate points”, and this is what 2.1 is groping to express.
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 space or -space is 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
1 to 10 of 10