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.
In response to discussions at set theory, created structural set theory with a tentative formal definition of when a set theory is "structural."
I have moved the notion of “structural presentation” of a set theory to its own page, structurally presented set theory.
Also, I am pasting here for future reference the discussions that have been sitting around at the bottom of structural set theory and removing them.
Arnold Neumaier: To me this looks more like a theory of copies of cardinal numbers that like a set theory. I think you should change the name “set” to “universe” or “collection”, or so. For your sets have very different properties from Cantor’s sets, whose terminology surely has priority. Cantor’s sets allow unions and intersections, your sets don’t. You do not even have the set {0,1,2}. Thus it is impossible to rewrite standard mathematics on your alternative foundation without changing the semantics of everything.
The name subset, on the other hand, is ok, since it shares enough properties of a set to be recognizable as a close relative. On the other hand, there are no functions from a subset to another subset, which again makes it quite cumbersome using this for ordinary mathematics.
How would you form something that substitutes for sets of relations, or subsets of subsets? What do you say in place of “A is a subset of A$\cup$B”? I think in SEAR, expressing ordinary mathematics becomes exceedingly tedious.
SEAR and ZF, “This process is described at pure set”. This is a sham. There it says “A pure set is a set of pure sets”. But with set understood as a SEAR-set, pure sets cannot be compared for equality. But this is an intrinsic part of ZF.
Toby: It is very astute of you to say that this is really a theory of cardinal numbers!
AN: I did not say that; it isn’t. I said that SEAR is a theory of copies of cardinals. For there is a unique cardinal 1 in set theory. But if A,B are two SEAR sets with exactly one element, one is not able to conclude that A and B are the same SEAR set. Thus one can have many meta-distinct copies of the same cardinal around, although it is impossible to express this on the formal level.
AN: I’d say this is abstracting away the equality relation and replace it by isomorphy.
Toby continues: Lawvere has long said that his ’abstract sets’ and Cantor's ’Kardinalzahl’ are the same thing. But in fact the word ’set’ (’Menge’) is not only used in Cantor's original sense of a subset of some fixed universe (originally the collection of real numbers, eventually the entire von Neumann hierarchy) today. Whenever someone says ’A group is a set equipped with […]’, the only thing that matters for group theory is the abstract set, the Kardinalzahl. It is very easy to rewrite standard mathematics on this foundation;
AN: If it were very easy, it would have been done already. I see many obstacles in actually doing that.
Toby: It has been done already, and has been since at least the '60s.
AN: Then please show me the result in the form of a treatise comparable to Bourbaki’s Elements of mathematics. Its existence would mean it has been done. But there is not even a textbook on calculus that is rewritten on this foundation!
Toby: There is no need to rewrite an ordinary calculus textbook on this foundation, any more than we needed to rewrite elementary geometry after Hilbert. The material in basic calculus is mostly from the 19th century, after Weierstrass but before Dedekind and Cantor; more advanced material requires care (and indeed, led Dedekind and Cantor to develop set theory), but high school calculus does not. You may as well rewrite a textbook on the history of the Soviet Union for all the difference that it would make; the latter might at least mention set theory if it went deep enough. The ’sets’ of calculus are subsets of $\mathbf{R}$ (or $\mathbf{R}^n$); the ’functions’ are partial functions from $\mathbf{R}$ to $\mathbf{R}$, which may be formalised as functional relations. They are not exactly the same as the ’sets’ and ’functions’ of either $\mathbf{SEAR}$ or $\mathbf{ZF}$, but we can understand them.
All that said, calculus has been written down in an explicitly structural way, in Errett Bishop's book on constructive analysis. However, the book that you want is probably Sets for Mathematics, by Lawvere & Rosebrugh. Of course, it is not comparable to Bourbaki; nothing is. You will find it far too brief, but it shows how to get started.
Toby continues: The point of $\mathbf{SEAR}$ is to do it in a less category-inspired, hopefully more familiar, way. Show me an obstacle in applications of set theory to ordinary mathematics, if you have one.
…
…
AN: The example of the exercise below shows that you need to interpret all sets of which unions or intersections are taken as subsets of a more universal set. Thus the SEAR notion of set is in fact that of a universe (and nothing like the standard concept of a set), while the notion of a SEAR subset is more or less that of an ordinary set.
Toby: If by ’universe’ you mean set² and by ’ordinary set’ you mean set¹, then you are right. But you are wrong about what is the standard conception among mathematicians. There are many of us structural mathematicians; we find each other on the Internet (and found each other before, but I am too young for that); how did that happen? are we suffering from a mass delusion? or perhaps we are not really mathematicians (we have a tendency to work on category theory, after all)?
Of course, one can embed all mathematics into SEAR (with the right existence axioms) by doing everything inside a single universe (= a SEAR set whose cardinality is inaccessible). This is what I would do if I were forced to work in SEAR (which fortunately I am not); then I have materiasl equality of sets (= subsets of the universe). Then one can use standard language and standard notation without difficulty and doesn’t have to rewrite anything, except perhaps add to the strength of SEAR a condition that allows this universe to exists and the collection of its subsets to satisfy the ZF axioms.
But you’d have to rewrite everything if you want to enforce the terminology of SEAR upon mathematics (relabel lots of sttandard sets as subsets or tabulations, etc.. I don’t believe mathematical language will take this turn.
Toby: No, you wouldn't! There is no need to strengthen $\mathbf{SEAR}$ to include an uncountable inaccessible cardinal and then talk only about subsets of a universe with that cardinality; indeed, it would be foolish to, since then more things would be true than you had wanted. Instead, you just write normally, with the abuses of language being slightly different abuses. See below, where I am more radical than Mike, for more on this.
Toby continues: while in a sense the semantics has changed, it is the claim of structural set theorists that we are getting at what was the real meaning all along. You might as well say that Dedekind changed the semantics of algebra and analysis when he identified ideal numbers and real (possibly irrational) numbers with certain sets, and in a way he did, but he also clarified those ideas. And it is not just us, coming along more than a hundred years after Cantor to change the language; people have been doing structural set theory for some time, and it pops up in many places. Errett Bishop, for example, who wanted a constructive theory (not particularly a structural theory), wrote down a structural theory in his handbook of analysis all the same, even defining a subset of $X$ as a set $A$ equipped with an injection to $X$ (an unfamiliarity which the point of $\mathbf{SEAR}$ is largely to avoid). Any application of set theory in which we do not care what our sets' elements' elements are is inherently structural and translates directly into structural terms. Any time that someone says ’Relabel the element of $B$ if necessary so that $B$ will be disjoint from $A$, then consider $A \cup B$.’, they really mean ’Consider the disjoint union of $A$ and $B$.’ in a structural set theory. Very rarely do applications of set theory ever call for the hierarchy of pure sets.
As for that … I'll assume that you don't know the strength of ’sham’ in English, so I won't feel insulted.
AN: Sorry. I meant that the pure set page is a caricature of what was promised by the context of the link. (I hope this is acceptable language.) No argument was given for why the ZF axioms should hold; everything beyond the heditarily finite sets (which is the trivial part of ZF) is far too sketchy to support the strong claim that SEAR is equivalent to ZF.
Toby: This is all fairly well known; see (for example) Mac Lane & Moerdijk (I think Section VI.5) for details (although this does not deal with Replacement/Collection),
AN: so it is not a verification of the ZF axioms, which is what I had claimed is missing.
Toby continues: or Chapter 8 of Mike's paper Unbounded Quantifiers and Strong Axioms in Topos Theory (is that available yet, Mike?). Of course, these start with an explicitly categorial approach, but the equivalence of that with the approach of $\mathbf{SEAR}$ is fairly straightforward.
Mike Shulman: No, it’s not available yet, sorry. I got sidetracked with other things. But it’s back near the top of the to-do list.
AN: Then this should be mentioned in the main text rather than left for the reader to discover for himself or to wonder whether this is really true. Mathematics has a healthy convention that nontrivial claims are supported either by proofs or references to such proofs. Without these one is entitled to mistrust the claim.
…
…
Toby: You may mistrust it if you like. It is mentioned up top that this is all original; if there were papers to cite that we knew of, then we would cite them. If what you really want is to be certain that mathematics can be founded on a structural theory, then you should look at the established literature on $\mathbf{ETCS}$ or the type theory of Per Martin-Löf and Thierry Coquand.
Toby continues: But if you want precision, look at the Definition section, not the vague Idea. Equality of pure sets is also defined.
(There's still an error in that which I haven't fixed, but it's correct for well-founded pure sets, which are the ones that $\mathbf{ZFC}$ has.)
AN: I only saw a definition of equivalence. Now I realize that this should substitute for the nonexistence equality. I’ll comment more on the pure set page.
Toby continues: If you want a set of sets, you should consider whether it matters whether any of these sets happen to be equal, and how (for purposes of your application) you would know. In general, you take a family of sets (note to self: write an article there), that is an index set $I$ and, for each element $k$ of $I$, a set $S_k$. There is a handy trick for encoding this sort of thing as a set $\mathcal{S}$ and a function $\pi: \mathcal{S} \to I$; let $S_k$ be the preimage of $\pi^*(k)$ (which is a subset of $\mathcal{S}$. The purpose of the axiom of collection is to allow you to construct this set $\mathcal{S}$ (maybe I should write that down there for its motivation!). If you want, say, a family of groups, then you take $\pi: \mathcal{S} \to I$ and additionally a function $M: I \times \mathcal{S} \times \mathcal{S} \to \mathcal{S}$ such that, for each $k$, $M$ restricts to a function $m_k: S_k \times S_k \to S_k$ that satisfies the group axioms. And so on.
In this situation, you can't ask whether $S_k = S_{k'}$, or try $S_k \cap S_{k'}$, etc. If the structural perspective is valid, then you should only ever want to do that if the various $S_k$ are all subsets of some previously given ambient set $T$. There are two ways to do this; either define an $I$-indexed family of injections $S_k \to T$, or skip all of the above and instead consider a binary relation on $I$ and $T$; let $S_k$ be the set of elements of $T$ that $k$ is related to. This is a family of unary relations on $T$; you can do a set of binary relations in a similar way. (By the way, in this case you don't need the axiom of collection to define $\mathcal{S}$, since you can make it a subset of $I \times T$. This is the idea, possibly familiar to you, that replacement/collection is not needed wherever it naïvely applies, but only for relatively high-powered stuff.)
David Roberts: I was going to ask something about the claim that after axioms 0,1 and 2 we have a category of sets (which I think is very cool), but I convinced myself that this was a metacategory with a collection of arrows between a pair of objects and a composite for each pair of (composable) arrows one is given. However, from Mike’s reply to my question, we can use the definition of the set of functions to then define a metacategory with a set of arrows between any two objects (this I must admit requires more than just a sweeping statement) but still only a collection of objects. Once one has defined universes, then - as much as I understand it - things can proceed much as with any other category $U-Set$ one might define with a universe $U$. We then have the universal family that the axiom of collection is a virtual shadow of.
In response to Toby’s comment about forming the union of sets above: it always annoyed me that people worry whether sets just happen to have elements in common. It is very much a 'is $\sqrt{2} \in \pi$?' type thing.
Mike Shulman: I agree with pretty much everything Toby said, except that I don’t think I would go so far as to claim that structural set theory gets at what was the real meaning all along. Maybe it’s what Cantor meant, maybe it isn’t (probably he wouldn’t even have understood the question as we ask it today). Instead, I would say that over the course of the 20th century, it emerged that sets in mathematics were only ever really used structurally.
AN: only ever?? Undergraduate mathematics is always conceived of materially. It can hardly be taught from a strictly structural point of view. Even many of the most exercises for undergraduates would have to be rewritten completely, and to avoid that things would get completely confusing, utmost care is needed.
SEAR cannot even define the elementary sets {a,b,c} and {a,b,d} and take their union {a,b,c,d}. These objects exist in SEAR only as subsets, but they are different objects depending on the set a,b,c,d are elements of. But it doesn’t matter which set this is, and a purely structural view should take that into account! Thus one needs to assume a universal set from which all objects of discourse are taken that one might want to have as element in some set. (For maybe one will later introduce an element e….) The subsets of this universal set then form a proxy of the sets of standard set theory. But having that (and augmenting the universal set to contain power sets, which is a natural next step), one can do all standard mathematics in this universal set, obviating the need for SEAR.
Toby: I have taught naïve set theory in a structural way.
AN: I’s like to get a copy of the lecture notes!
…
…
Toby: No lecture notes, I'm afraid, but you can look at the homework assignments. I'm not sure if you'll like it, since it's not very formal; I'll probably still have to convince you that everything can be formalised in $\mathbf{SEAR}$ (which is fine, just ask). The assignment for July 10 makes it particularly clear that the set theory is structural, and it shows you how to intepret in a structural framework some of the most basic questions of naïve set theory; the assignment for July 13 is also a good one for featuring the disjoint union. But really, the point to get is that you normally can't tell whether someone thinks of set theory materially or structurally; the ideas are almost always almost exactly the same. So if you're not sure how to formalise, say, July 11 in $\mathbf{SEAR}$, then perhaps we should talk about that.
Toby continues: Not that I made a big point about that, but then I didn't need to! The only thing unusual that I had to do was to introduce the concept of disjoint union, which actually made the applications in that course (which were to combinatorics) a little easier. Of course, a course in axiomatic set theory would have to be rewritten.
For the exercise ‘What is the union of $\{a,b,c\}$ and $\{a,b,d\}$?’, there is no need to change that in the naïve course. But formally, it means ‘Let $U$ be a set, and let $a,b,c,d$ be elements of $U$. Then (by previous results) we have subsets $\{a,b,c\}$ and $\{a,b,d\}$ of $U$. Find a similar expression for the union of these subsets.’.
AN: And you are not allowed to claim that {a,b,c} are sets! I am quite sure you didn’t go that far in your course on naive set theory!
Toby: I don't understand what you're saying that I'm not allowed to claim here. There is a technical distinction between $\{a,b,c\}$ as a subset of $U$ and $\{a,b,c\}$ as a $3$-element set in its own right, one which is usually glossed over. But you can think of it as either, if you wish. The subset comes first; in $\mathbf{SEAR}$ it is a relation $1 \looparrowright U$; then its tabulation is a $3$-element set, which by abuse of notation we also write $\{a,b,c\}$.
Mike Shulman continues: The reason I believe in structural set theory is not out of a philosophy that this is the “real” meaning of sets; in fact I think that ZF-theorists are studying a very real and interesting world! But when I look at most mathematics as it is done by most mathematicians, what I see is sets treated structurally—so I think we should have a foundational account of sets which treats them that way.
AN: And when I look at most mathematics as it is done by most mathematicians, what I see is sets treated materially.
Clearly, this is not inherent in the mathematical writings but in the view. One needs both the material and the structural view, and foundations should provide both in an easy way.
To start with the material point of view has many advantages: It is easy to motivate, makes for easy language, and most textbooks are already written in that style.
Mike Shulman: Can you cite some example of mathematics outside of ZF-theory which really treats sets materially?
AN: In analysis, the vector space of real n-dimensional column vectors is probably universally treated as material.
Serge Lang, Algebra, second printing 1970
(which I happen to have at hand; sorry - my books on elementary math are all 40 years old, but all mathematics done then is still valid mathematics today!)
He begins in the first paragraph of the prerequisites with the assumption that a set may be contained in another set. This is actually heavily used; for example, a subgroup is for him clearly a group contained in another group, and not a group isomorphic to a such a group.
[This is also the case in modern text; the first algebra lecture notes I found with Google was by Wilkins has the same terminology for subgroups.
In Section I.7 on categories, he explicitly uses the formula A=B comparing two objects of a category for equality. Since Lang explicitly defines each allowed abuse of language, e.g., “By abuse of language, we sometimes refer to the collection of objects [of a category] as the category itself”, it is clear that he doesn’t consider A=B as an abuse of language, and hence adheres to a material point of view.
One can probably rewrite everything in a way that avoids all material issues, but (i) it hasn’t be done, and (ii) it would read quite different from what Lang actually writes.
…
…
Mike Shulman: I think the claim is not that existing mathematics doesn’t use the language of material set theory (after all, for decades that was the only language there was), but rather that its essence does not. Show me a result using the fact that a subgroup is a group literally contained in another group, but which would not work just as well for any injective group homomorphism.
AN: Maybe, but this cannot be discussed objectively since essence is not well-defined.
Toby: I do claim that existing mathematics uses the language of material set theory only a little more than it uses the language of structural set theory; for the most part, it is simply indifferent between them. In both cases, it is rife with little abuses of terminology and notation; if (like Lang) one is careful about that sort of thing, then it will be clear whether one thinks of sets materially or structurally. But if Lang had written the prerequisite set theory structurally, then the definition of ’subgroup’ could still have been written with exactly the same words (from my copy, 1993 edition)
Let $G$ be a group. A subgroup $H$ of $G$ is a subset of $G$ containing the unit element, and such that $H$ is closed under the law of composition and inverse.
In the prerequisites, he might(*) mention the abuse of language in which a subset is conflated with its underlying set (what Mike calls its ’tabulation’), which we need in order to think of $H$ as a set (and then a group) in its own right. But that is all in the set theory; the language of algebra is the same.
(*) On the other hand, there are other things that he did not mention. For a map $f : A \to B$, he defined the preimage $f^{-1}(B')$ of a subset $B'$ of $B$, but never defined the image $f(A')$ of a subset of $A$, even though this is used in the text. (He only mentioned $f(A)$ itself.) If he had, then he would have had to note the ambiguity in the case that $A'$ is also an element of $A$; this doesn't come up structurally. (Even for $f(A)$, it's hard to imagine that really intended to rely on the axiom of foundation to rule out the possibility that $A \in A$.) He took care to define what a ’family of elements’ of a given set is, but not a ’family of sets’, even though he mentions the concept. That is harder to formalise, both materially and structurally. Basically, he seems to avoid things that are tricky to state precisely.
The most common exception that I admit to my thesis is the disjoint union, or rather the reluctance to see this as one of the basic operations of set theory. It is actually easier (although not much) to construct a disjoint union materially than structurally (unless you take its existence as an axiom), but many people don't bother. What I do see is a lot of broad abuse of language to get around this, such as ’Take two disjoint copies of $A$.’ or ’If $A$ and $B$ are not disjoint, then relabel the elements of $B$ so that they are, and consider $A \cup B$.’. Structurally, you would not be tempted to say such things; although if we had all grown up with structural set theory, I'm afraid that we might have a tendency write ‘$A \cup B$’ for the disjoint union when $A$ and $B$ bear no relation, and that would also be an abuse of notation.
Mike Shulman: I’m actually basically in agreement with you, Toby, but I didn’t feel like getting into detail about the sorts of “abuses” (i.e. definitions of terminology/notation) that are necessary to read existing mathematics in a structural way. But you make a good point that reading it in a material way requires different “abuses,” some of which people tend to make explicit and some of which they don’t.
BTW, in a more leisurely pedagogical treatment of SEAR, I would be tempted to include an axiom of disjoint unions early on, and only remark later, after powersets are introduced, that they imply the existence of disjoint unions.
Toby: Also quotient sets and (in a constructive theory) function sets make good axioms; one may want these constructions even if one drops power sets. But for people weaned on $\mathbf{ZFC}$'s pairing and union axioms, disjoint unions are particularly important!
And the other one:
Mike Shulman: I think the claim is not that existing mathematics doesn’t use the language of material set theory (after all, for decades that was the only language there was), but rather that its essence does not. Show me a result using the fact that a subgroup is a group literally contained in another group, but which would not work just as well for any injective group homomorphism.
AN: Maybe, but this cannot be discussed objectively since essence is not well-defined.
Toby: I do claim that existing mathematics uses the language of material set theory only a little more than it uses the language of structural set theory; for the most part, it is simply indifferent between them. In both cases, it is rife with little abuses of terminology and notation; if (like Lang) one is careful about that sort of thing, then it will be clear whether one thinks of sets materially or structurally. But if Lang had written the prerequisite set theory structurally, then the definition of ’subgroup’ could still have been written with exactly the same words (from my copy, 1993 edition)
Let $G$ be a group. A subgroup $H$ of $G$ is a subset of $G$ containing the unit element, and such that $H$ is closed under the law of composition and inverse.
In the prerequisites, he might(*) mention the abuse of language in which a subset is conflated with its underlying set (what Mike calls its ’tabulation’), which we need in order to think of $H$ as a set (and then a group) in its own right. But that is all in the set theory; the language of algebra is the same.
(*) On the other hand, there are other things that he did not mention. For a map $f : A \to B$, he defined the preimage $f^{-1}(B')$ of a subset $B'$ of $B$, but never defined the image $f(A')$ of a subset of $A$, even though this is used in the text. (He only mentioned $f(A)$ itself.) If he had, then he would have had to note the ambiguity in the case that $A'$ is also an element of $A$; this doesn't come up structurally. (Even for $f(A)$, it's hard to imagine that really intended to rely on the axiom of foundation to rule out the possibility that $A \in A$.) He took care to define what a ’family of elements’ of a given set is, but not a ’family of sets’, even though he mentions the concept. That is harder to formalise, both materially and structurally. Basically, he seems to avoid things that are tricky to state precisely.
The most common exception that I admit to my thesis is the disjoint union, or rather the reluctance to see this as one of the basic operations of set theory. It is actually easier (although not much) to construct a disjoint union materially than structurally (unless you take its existence as an axiom), but many people don't bother. What I do see is a lot of broad abuse of language to get around this, such as ’Take two disjoint copies of $A$.’ or ’If $A$ and $B$ are not disjoint, then relabel the elements of $B$ so that they are, and consider $A \cup B$.’. Structurally, you would not be tempted to say such things; although if we had all grown up with structural set theory, I'm afraid that we might have a tendency write ‘$A \cup B$’ for the disjoint union when $A$ and $B$ bear no relation, and that would also be an abuse of notation.
Mike Shulman: I’m actually basically in agreement with you, Toby, but I didn’t feel like getting into detail about the sorts of “abuses” (i.e. definitions of terminology/notation) that are necessary to read existing mathematics in a structural way. But you make a good point that reading it in a material way requires different “abuses,” some of which people tend to make explicit and some of which they don’t.
BTW, in a more leisurely pedagogical treatment of SEAR, I would be tempted to include an axiom of disjoint unions early on, and only remark later, after powersets are introduced, that they imply the existence of disjoint unions.
Toby: Also quotient sets and (in a constructive theory) function sets make good axioms; one may want these constructions even if one drops power sets. But for people weaned on $\mathbf{ZFC}$'s pairing and union axioms, disjoint unions are particularly important!
There’s a citation in structural set theory to “Benacerraf’s paper”, but no paper (or other reference) is listed.
I put the reference in.
Oops! I forgot to add that reference. Thanks! I also added the other one I intended to add, by McLarty.
To the Examples-section at structural set theory I have added the following paragraph:
Generally, set theory set up in intuitionistic type theory is structural. For instance setoids in extensional type theory or h-sets in homotopy type theory (Rijke-Spitter 13).
Hope that’s okay. Please fine-tune if not. But I thought some mentioning like this must not be omitted from that page.
What do you intend the word “generally” to mean? One can just as well set up a material set theory inside ITT, such as Aczel’s construction of CZF.
Ah, I see. I have changed it to the following, is that better?
Set theory set up in intuitionistic type theory via setoids is structural.
Set theory set up via h-sets in homotopy type theory is structural (Rijke-Spitter 13).
Sure. Thanks!
I had a short discussion on structural set theory today. Tom’s beautiful short paper rethinking set theory seems to be missing. Also, we don’t seem to have local set theory by Bell and Aczel. I am inclined to put all three of them in structural set theory. Any objections to this? I seem to recall that we had a pending discussion on reorganizing the set theory pages.
Sounds good.
algebraic set theory misses a reference to stack semantics (michaelshulman). Should I just add the “external” link, or is there a better way?
external link is fine
I noticed that structural set theory was not cross-linked with Sets for Mathematics, so I added some.
Then I noticed that the lead-in paragraphs seemed to be lacking some gentle broad remarks before entering technical detail, so I expanded the first paragraph and added a second (before what is now the third).
Experts here may want to touch this further. Let’s try to keep in mind a reader with standard mathematics background but otherwise no initiation. Think of your colleague on the other floor. Try to make the entry give him a good idea of why strutural set theory matters.
Thanks, this looks pretty good. I tweaked the first paragraph since not all structural set theories (e.g. not SEAR) proceed by axiomatizing functions and the category $Set$.
Thanks!
Now I noticed that the Examples-section never mentioned the word “topos”. I have given each example a section header, and then added some lines containing the term “topos” to the section on ETCS and also a few words to the section on h-sets .
Would be great if you could fine a minute to fine-tune.
I would like to have the entry say that the idea of sets in HoTT is very much in the spirit (even if different in technical detail) of ETCS, especiall the spirit of “fixing one base topos and then doing all maths in there”. Maybe this could be said in the entry in some way that feels acceptable.
Looks fine, I think.
1 to 26 of 26