Not signed in (Sign In)

Start a new discussion

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 deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor galois-theory 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 manifolds mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number 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 string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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).
    • Updating reference to cubical type theory. This page need more work.

      diff, v55, current

    • Just a stub for the moment to try to introduce the notion of differential category due to Blute, Cockett and Seely.

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • Added a section about families of sets in dependent type theory

      Anonymous

      diff, v5, current

    • at foundation of mathematics I have tried to start an Idea-section.

      Also, I am hereby moving a bunch of old discussion boxes from there to here:


      [ begin forwarded discussion ]

      +– {: .query} Urs asks: Concerning the last parenthetical remark: I suppose in this manner one could imagine (n+1)(n+1)-categories as a foundation for nn-categories? What happens when we let nn \to \infty?

      Toby answers: That goes in the last, as yet unwritten, section. =–

      +– {: .query} Urs asks: Can you say what the problem is?

      Toby answers: I'd say that it proved to be overkill; ETCS is simpler and no less conceptual. In ETCC (or whatever you call it), you can neatly define a group (for example) as a category with certain properties rather than as a set with certain structure. But then you still have to define a topological space (for example) as a set with certain structure (where a set is defined to be a discrete category, of course). I think that Lawvere himself still wants an ETCC, but everybody else seems to have decided to stick with ETCS.

      Roger Witte asks: Surely in ETCC, you define complete Heyting algebras as particular kinds of category and then work with Frames and Locales (ie follow Paul Taylor’s leaf and apply Stone Duality). You should be able to get to Top by examining relationships between Loc and Set. I thought Top might be the the comma category of forgetful functor from loc to set op and the contravariant powerset functor. Thus a Topological space would consist of a triple S, L, f where S is a set, L is a locale and f is a function from the objects of the locale to the powerset of S. A continuous function from S, L, f to S’, L’, f’ is a pair g, h where g is a function from the powerset of S’ to the powerset of S and g is a frame homomorphism from L’ to L and (I don’t know how to draw the commutation square). However I think this has too many spaces since lattice structures other than the inclusion lattice can be used to define open sets.

      Toby: It's straightforward to define a topological space as a set equipped with a subframe of its power set. So you can define it as a set SS, a frame FF, and a frame monomorphism f:FP(S)f\colon F \to P(S), or equivalently as a set SS, a locale LL, and an epimorphism f:LDisc(S)f\colon L \to Disc(S) of locales, where Disc(S)Disc(S) is the discrete space on SS as a locale. (Your ’However, […]’ sentence is because you didn't specify epimorphism/monomorphism.) This is a good perspective, but I don't think that it's any cleaner in ETCC than in ETCS.

      Roger Witte says Thanks, Toby. I agree with your last sentence but my point is that this approach is equally clean and easy in both systems. The clean thing about ETCC is the uniformity of meta theory and model theory as category theory. The clean thing about ETCS is that we have just been studying sets for 150 years, so we have a good intuition for them.

      I was responding to your point ’ETCC is less clean because you have to define some things (eg topological spaces) as sets with a structure’. But you can define and study the structure without referring to the sets and then ’bolt on’ the sets (almost like an afterthought).

      Mike Shulman: In particular cases, yes. I thought the point Toby was trying to make is that only some kinds of structure lend themselves to this naturally. Groups obviously do. Perhaps topological spaces were a poorly chosen example of something that doesn’t, since as you point out they can naturally be defined via frames. But consider, for instance, a metric space. Or a graph. Or a uniform space. Or a semigroup. All of these structures can be easily defined in terms of sets, but I don’t see a natural way to define them in terms of categories without going through discrete categories = sets.

      Toby: Roger, I don't understand how you intend to bolt on sets at the end. If I define a topological space as a set SS, a frame FF, and a frame monomorphism from FF to the power frame of SS, how do I remove the set from this to get something that I can bolt the set onto afterwards? With semigroups, I can see how, from a certain perspective, it's just as well to study the Lawvere theory of semigroups as a cartesian category, but I don't see what to do with topological spaces.

      Roger Witte says If we want to found mathematics in ETCC we want to work on nice categories rather than nice objects. Nice objects in not nice categories are hard work (and probably ’evil’ to somke extent). Thus the answer to Toby is that to do topology in ETCC you do as much as possible in Locale theory (ie pointless topology) and then when you finally need to do stuff with points, you create Top as a comma like construction (ie you never take away the points but you avoid introducing them as long as possible). Is it not true that the only reason you want to introduce points is so that you can test them for equality/inequality (as opposed to topological separation)?

      Mike, I spent about two weeks trying to figure out how to get around Toby’s objection ’topology’ and now you chuck four more examples at me. My gut feeling is that the category of directed graphs is found by taking the skeleton of CAT, that metric locales are regular locales with some extra condition to ensure a finite basis, that Toby can mak

      [ to be continued in next comment ]

    • added table of contents, headers, and added an overview page for how size issues are handled by using some notion of universe, and what those universes are in different foundations.

      Anonymous

      diff, v2, current

    • starting page on this notion of “class of all classes”

      Anonymous

      v1, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • I noticed that there was a neglected stub entry universe that failed to link to the fairly detailed (though left in an unpolished state full of forgotten discussions) Grothendieck universe.

      I renamed the former to universe > history and made “universe” redirect to “Grothendieck universe”

    • Added:

      References

      A definitive source (by one of the authors of the theory) is

      • Anthony P. Morse, A theory of sets, Pure and Applied Mathematics XVIII, Academic Press (1965), xxxi+130 pp. Second Edition, Pure and Applied Mathematics 108, Academic Press (1986), xxxii+179 pp. ISBN: 0-12-507952-4

      diff, v6, current

    • removed link to old philosophy paper

      steveawodey

      diff, v9, current

    • brief category:people-entry for hyperlinking references

      v1, current

    • starting something – my main motivation for the moment is to bring out references which admit that topological quantum computation by braiding of defect anyons is a form of adiabatic quantum computation

      v1, current

    • a stub entry, nothing here yet for the moment

      v1, current

    • all the ZFC axioms have structural counterparts, which means that one could come up with a structural set theory which is equivalent in strength to ZFC.

      Anonymous

      v1, current

    • starting article on the type of classes in type theory.

      Anonymous

      v1, current

    • Added reference to the paper

      Paul Blain Levy, Formulating Categorical Concepts using Classes, arXiv:1801.08528

      diff, v10, current

    • Page created, but author did not leave any comments.

      Anonymous

      v1, current

    • will expand on this article; I think some material from class should be moved here, especially as the term “class” isn’t really used in structural set theory or dependent type theory for “large set”.

      Anonymous

      diff, v2, current

    • starting section on how the foundations of mathematics affects the language and meaning/semantics used in mathematics.

      Anonymous

      diff, v8, current

    • Adding reference

      as a construction of the locale of real numbers can be found in section 5.3 of that article

      Anonymous

      diff, v20, current

    • started section on formal topologies in dependent type theory

      Anonymous

      diff, v16, current

    • The entry used to be a plain disambiguation between reflective subcategory and an empty list of other meaning of reflection.

      But since the only evident point that entries like rotation, translation, boost, etc. could point to for related concepts is an entry called reflection. So maybe that should be the main meaning here, and alternative meaning be secondary.

      I slightly edited accordingly. But besides the different link structure now, there is still no substantial content here.

      diff, v2, current

    • Page created, but author did not leave any comments.

      Anonymous

      v1, current

    • A×BA\times B is not the coproduct of AA and BB in Rel.

      Anonymous

      diff, v56, current

    • expanded the discussion at equivariant homotopy theory

      • expanded the statement of the classical Elmendorf theorem

      • added the statement of the general Elmendorf theorem in general model categories

      • added remarks on G-equivariant oo-stacks, as special cases of this

    • starting article on neutral constructive mathematics

      Anonymous

      v1, current

    • Urs has added Euler integration prompted by Tom’s post at nCafe; I wanted to do that and will contribute soon. I noticed there is no entry integral in nnLab, but it redirects to integration. I personally think that integral as a mathematical object is a slightly more canonical name for a mathematical entry than integration, if the two are not kept separated. Second, the entry is written as an (incomplete) disambiguation entry and with a subdivision into measure approach versus few odd entries. I was taught long time ago by a couple of experts in probability and measure theory that a complete subordination to the concept of integral to a concept of measure is pedagogically harmful, and lacks some important insights. This has also to do with the choice of the title: integration points to a process, and the underlying process may involve measure. Integral is about an object which is usually some sort of functional, or operator, on distributions which are to be acted upon.

      Thus I would like to rename the entry into integral (or to create a separate entry from integration) and make it into a real entry, the list of variants being just a section, unlike in the disambiguation only version. What do you think. Then I would add some real ideas about it.

    • moved the stuff about the relation between precompact spaces and totally bounded spaces to its own section

      Anonymous

      diff, v5, current

    • starting page on preuniform locales

      Anonymous

      v1, current