I found the organization at *Zorn’s lemma* a bit rough, so I have tried to smoothen it out a bit

For instance

at one point it had suddenly said “proof of the converse” without a clear statement of the other direction having appeared before. I have created two Theorem-environments and tried to make the statements clearer.

the Idea-section had started out saying that “Zorn’s lemma is a trick”. I think that’s misleading or at least misses the important nature of the thing, so I rewrote that and expanded a bit.

But the foundationalists among you please check!

]]>added to [[Set]] the statement that is the terminal topos.

]]>I have briefly recorded the equivalence of FinSet${}^{op}$ with finite Booplean algebras at *FinSet – Properties – Opposite category*. Then I linked to this from various related entries, such as *finite set*, *power set*, *Stone duality*, *opposite category*.

(I thought we long had that information on the $n$Lab, but it seems we didn’t)

]]>At *interactions of images and pre-images with unions and intersections* I have added pointer to Lawvere 69 and there at *Adjointness in Foundations* I added a bit more text and cross-references.

created *Bishop set* to go with the discussion in another thread here

(I have tried to cross-link this to the relant entries, but maybe Toby should look over this. I suppose some further existing nLab discussion of Bishop’s work could be cross linked here)

]]>I have edited *support* to say that in topology the support of a function is usually to be the topological closure of the naive support.

I gave *Sets for Mathematics* a category:reference entry and linked to it from *ETCS* and from *set theory*, to start with.

David Corfield kindly alerts me, which I had missed before, that appendix C.1 there has a clear statement of Lawvere’s proposal from 94 of how to think of categorical logic as formalizing objective and subjective logic (to which enty I have now added the relevant quotes).

]]>Created ZFA, about ZF with atoms. I’ve added it to the foundations side bar under material set theories and a stack of links.

]]>at *complete Boolean algebra* I fixed the missing ${}^{op}$ and then added a pointer to *Set – Properties – Opposite category and Boolean algebras*.

Prompted by discussion in the thread on “internal sets” (badly named so) I have added to *h-set* a comment in *Properties - Relation to internal set*.

I have cross-linked the entries *forcing* and *classifying topos* just a tad more by

adding a half-sentence at the end of the paragraph in the Idea-section at “forcing” which mentions the word “classifying topos”

adding to “classifying topos” the references (grabbed from “forcing”) on the relation between the two: here.

I imagine any categorical logician who would write a pedagogical exposition at *forcing* on how this concept appears from the point of view of topos theory could have some effect on the community. The issue keeps coming up in discussions I see, and so if we had a point to send people to really learn about the relation (instead of just being bluntly old that there is one) that might have an effect.

At *well-ordering theorem* there had been a request for “transfinite arithmetic”. I have now made that a redirect to *ordinal arithmetic*, but this entry is nothing but a stub at the moment.

In cross-linking, I realized that presently “arithmetic” redirects to *number theory*. Is that a good idea?

in the course of writing out proofs in elementary topology, i found it useful to be able to easily link to elementary statements in elementary set theory. So I created entries like

]]>i have split off (copied over) the paragraph on the first uncountable ordinal from *countable ordinal* to *first uncountable ordinal*, just in order to make it possible to link to “first uncountable ordinal” more directly. Cross-linked with *long line*.

At *limits and colimits by example* an entry for *Kuratowski pair* was requested, so I created it. The place where this should really be linked to is the entry *ordered pair*, so I added a link there. Also, I made that entry mention *Cartesian product*, which it didn’t.

created some minimum at *saturated subset*, in order to be able to link to it.

When I made *inhabitant* redirect to *term* a few minutes ago, I noticed a bunch of orphaned related entries.

For instance *inhabited type* since long ago redirect to *inhabited set*. I haven’t changed that yet, but I added some cross links and comments to make clear that and how the three

are related. The state of these entries deserves to be improved on, but I won’t do anything further right now.

]]>created *predicative topos* (for the entry *Bishop set* to link to).

I happened upon our entry *ETCS* again (which is mostly a pointer to further entries and further resources) and found that it could do with a little bit more of an Idea-section, before it leaves the reader alone with the decision whether to follow any one of the many further links offered.

I have expanded a bit, and now it reads as follows. Please feel invited to criticize and change. (And a question: didn’t we have an entry on ETCC, too? Where?)

The **Elementary Theory of the Category of Sets** (Lawvere 65), or *ETCS* for short, is a formulation of set-theoretic foundations in a category-theoretic spirit. As such, it is the prototypical structural set theory.

More in detail, ETCS is a first-order theory axiomatizing elementary toposes and specifically those which are well-pointed, have a natural numbers object and satisfy the axiom of choice. The idea is, first of all, that traditional mathematics naturally takes place “inside” such a topos, and second that by varying the axioms much of mathematics may be done inside more general toposes: for instance omitting the well-pointedness and the axiom of choice but adding the Kock-Lawvere axiom gives a smooth topos inside which synthetic differential geometry takes place.

Modern mathematics with emphasis on concepts of homotopy theory would more directly be founded in this spirit by an axiomatization not just of elementary toposes but by elementary (∞,1)-toposes. This is roughly what univalent homotopy type theory accomplishes, for more on this see at *relation between type theory and category theory – Univalent HoTT and Elementary infinity-toposes*.

Instead of increasing the higher categorical dimension (n,r) in the first argument, one may also, in this context of elementary foundations, consider raising the second argument. The case $(2,2)$ is the elementary theory of the 2-category of categories (ETCC).

]]>

I discovered via MO that we have an entry *hereditarily finite set*, which was a bit lonesome. So I have now tried to cross-link it a bit with related entries.

In particular at *finite object* in “Related entries” I started a list with related entries – probably incomplete, please expand. In the course of this I created als a brief entry *finite (infinity,1)-category* by splitting off a paragraph form finite (infinity,1)-limit.

On some pages it is desireable to have cardinalities “$\aleph$” be provided with a link to their explanation. I have cerated a redirect-page ℵ for that purpose.

]]>When making *inhabitant* redirect to *term* a few minutes back I also found the entry *term* to be in an unfortunate state. I tried to improve it a bit by giving it more of an Idea section, and at least a vague indication of the formal definition.