# 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

## Site Tag Cloud

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

• Updating reference to cubical type theory. This page need more work.

• stub

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

• I had accidentally duplicated this page, but merging it now into the new one: Robert B. Griffiths

• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

• Chris Nagele, Oliver Janssen, Matthew Kleban, Decoherence: A Numerical Study (arXiv:2010.04803)
• brief category:people-entry for hyperlinking references

• brief category:people-entry for hyperlinking references

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

Anonymous

Anonymous

• 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)$-categories as a foundation for $n$-categories? What happens when we let $n \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 $S$, a frame $F$, and a frame monomorphism $f\colon F \to P(S)$, or equivalently as a set $S$, a locale $L$, and an epimorphism $f\colon L \to Disc(S)$ of locales, where $Disc(S)$ is the discrete space on $S$ 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 $S$, a frame $F$, and a frame monomorphism from $F$ to the power frame of $S$, 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 ]

• Page created.

• Created a page.

M Carmona

Anonymous

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

Anonymous

• brief category:people-entry for hyperlinking references

• 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”

## 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
• removed link to old philosophy paper

steveawodey

• brief category:people-entry for hyperlinking references

• 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

• a stub entry, nothing here yet for the moment

• a bare list of references, to be !includ-ed into the list of references of relevant entries, such as at quantum computing and quantum programming, for ease of updating and syncing

• 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

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

Anonymous

• Added reference to the paper

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

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

Anonymous

• 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

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

Anonymous

• Definition and characterization as monoids

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

Anonymous

• started section on formal topologies in dependent type theory

Anonymous

• 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.

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

Anonymous

• moving text from reflection to its own separate page

Anonymous

• $A\times B$ is not the coproduct of $A$ and $B$ in Rel.

Anonymous

• starting article on set theories with three sorts, an example of which is structural ZFC.

Anonymous

• 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

• 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 $n$Lab, 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.

• adding accents to the page name, to make Dmitri’s requested links work at localic group

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

Anonymous

• moving section on precompact spaces under properties section instead of definition section

Anonymous

• starting page on preuniform locales

Anonymous