Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 13th 2012

    The category of prosets is a coreflective subcategory of the category of topological spaces. I edited in this observation at specialization order, and am removing a query box:

    +–{.query} There's an adjunction here; I should think about which way it goes and whether it's a reflection or something. —Toby Mike: If it exists, it’s either a reflection or a coreflection, since the functor ProsTop\Pros \to \Top is fully faithful. =–

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeSep 13th 2012

    Thanks!

  1. The second of the two equivalent conditions was reversed by mistake. Now it’s been corrected.

    Anonymous

    diff, v9, current

  2. Retract the previous edit.

    Anonymous

    diff, v9, current

  3. Fixed minor typo.

    Anonymous

    diff, v10, current

    • CommentRowNumber6.
    • CommentAuthorPatrick Rabau
    • CommentTimeJan 31st 2023

    fix inconsistent name of category of prosets

    diff, v12, current

    • CommentRowNumber7.
    • CommentAuthorGuest
    • CommentTimeMay 23rd 2023

    added definition of specialization order in dependent type theory and a proof that the specialization order is a preorder

    diff, v13, current

    • CommentRowNumber8.
    • CommentAuthorGuest
    • CommentTimeMay 23rd 2023
    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 4th 2023

    I’d like to inquire: what is the point of this rendering into the language of dependent type theory? (This is one of many such edits I’ve seen.)

    The way it appears to me, it looks analogous to a student exercise of taking simple sentences in English and translating them into Dutch. It might be a worthwhile exercise for the student of Dutch. I, even though I don’t speak Dutch, can easily tell what the Dutch sentences mean and how they correlate with the English ones, because they look rather similar, but I don’t see how it serves anyone in any real sense, except possibly other students of Dutch (or people fluent in Dutch).

    A ruder take is that it looks pretentious, dressing up prosaic mathematics in hypermodern language, and overall that’s probably not a good thing, unless there’s some compelling reason for it that eludes me.

  4. I’m not sure if this is the situation with the dependent type theory stuff on this page, but last year there were anonymous posters mass posting material from the HoTT wiki over to the nLab wiki, so among other things the nLab ended up with various pages with both a logic-over-set-theory definition and a type theory definition. (cf revision 40 of filter on June 9, 2022, and the corresponding edit on the HoTT wiki)

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 5th 2023

    Thanks for the information, Madeleine. Naturally, I’d want to know: why? Is the HOTT wiki deprecated?

    (My offhand guess is that not much thought went into how the transplantation would be enacted, though.)

    With regard to the current page, maybe some material could be shuffled around. The type-theoretic construction of specialization, and the demonstration of Theorem 3.1: all that would go under a separate section. Since that is somewhat for specialists, if it were up to me, I’d place it more toward the end.

  5. Naturally, I’d want to know: why? Is the HOTT wiki deprecated?

    There is a message on the home page of the HoTT wiki saying that it is depreciated.

    With regard to the current page, maybe some material could be shuffled around. The type-theoretic construction of specialization, and the demonstration of Theorem 3.1: all that would go under a separate section. Since that is somewhat for specialists, if it were up to me, I’d place it more toward the end.

    Personally I would try to find a proof of Theorem 3.1 which does not rely on dependent type theory, since it seems to be a fairly well known theorem for topological spaces - the theorem is mentioned as fact elsewhere in the nLab such as in separation axiom. But otherwise I agree, the specifically type theoretic material on the page should be moved to its own section towards the end, similar to how the page on skeleton is organized.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2023

    Some of the back story and the beginning of the merger of the HoTT wiki into the nLab can be gleaned from the original thread.

    This was a major event and a fair bit of headache for several weeks. (For me anyways, the so-called “steering committee” may not even have noticed anything.)

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 5th 2023

    Thanks, Madeleine. I assume there was a good reason for it. Perhaps all those “Anonymous” edits, that water down the quality of the nLab generally, had something to do with it.

    (Generally, there’s no end to the number of entries one can generate through the semi-mindless exercise of writing ordinary prosaic definitions and propositions in this fashionable language. More real contentful mathematics, please.)

    Getting back to the current page: the “Theorem” (I’d sooner demote it to Proposition) is a special case of something extremely general throughout mathematics: if R(x,y)R(x, y) is any binary predicate, then a reflexive transitive relation T(x,y)T(x, y) can be defined by the formula zR(x,z)R(y,z)\forall_z\; R(x, z) \Rightarrow R(y, z). It goes under many names.

    • CommentRowNumber15.
    • CommentAuthorGuest
    • CommentTimeJun 5th 2023

    moving Theorem 3.1 and its proof from specialization order to preorder because the proof applies to all binary relations, not just that of the membership relation between elements and open sets of a topological space.

    diff, v16, current

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 5th 2023
    • (edited Jun 5th 2023)

    Please identify yourself, Guest, with a name or pseudonym that enables us to distinguish you from other “Guests”.

    (I thought this feature had been eliminated?!)

    • CommentRowNumber17.
    • CommentAuthorGuest
    • CommentTimeJun 5th 2023

    moving dependent type theory section to the bottom.

    diff, v16, current

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2023
    • (edited Jun 5th 2023)

    We have had a problem on many other pages with anonymous editors adding unnecessary type-theoretic stuff. I wish that I had the time to go through and fix all these pages myself, but I just don’t. In any case I agree with Todd: there’s no purpose to rephrasing an essentially foundation-independent definition in type-theoretic language. It’s worth including discussion of alternative foundations when the difference matters, but in this case there’s no evidence presented that it does matter. So I would suggest the section be simply removed from this page.

  6. the text in the dependent type theory section used to define the membership relation is a duplicate of text found in topological space, so I replaced the duplicated text with a link to the topological space article.

    Raymond

    diff, v17, current

  7. the remainder of the dependent type theory section is just a duplicate of the 2nd definition in this article, so removed the dependent type theory section entirely

    Raymond

    diff, v17, current