When I was a graduate student, I taught a discrete mathematics course in the summers, and this included an introduction to set theory. There was no formal axiomatization, but I taught the set theory structurally.

For example, I said that you should only consider $A \cup B$ or $A \cap B$ when $A$ and $B$ are given as subsets of an ambient set $X$. Otherwise, the concept may appear meaningful, but the apparent result may depend on arbitrary coincidences of notation. Relatedly, I introduced the disjoint union as a basic operation on sets, on a par with the Cartesian product. The course also included some combinatorics, and I taught ${|A \uplus B|} = {|A|} + {|B|}$ as the basic sum rule for cardinality of (finite) sets, on a par with ${|A \times B|} = {|A|} \,{|B|}$ as the product. That ${|A \cup B|} = {|A|} + {|B|}$ when $A$ and $B$ are disjoint subsets of some ambient set is just a corollary.

And related to the disjoint union, I taught quotient sets as a fundamental concept too. Given a set $X$ and an equivalence relation $R$, there is a set $X/R$, called the *quotient* of $X$ modulo $R$ such that:

- an element of $X/R$ has the form $[a]_R$, called the
*equivalence class*of $a$ modulo $R$, for some element $a$ of $X$; - $[a]_R = [b]_R$ (in $X/R$) if and only if $R$ holds of $a$ and $b$.

(This specifies a set by explaining what form its elements take and when two of these elements are equal, which I got straight out of Bishop's *Constructive Analysis*.) As a side note, I explained the terminology ‘equivalence class’:

- given $a$ in $X$, the
*equivalence set*of $a$ modulo $R$ is the subset of $X$ consisting of those $b$ in $X$ such that $R$ holds of $a$ and $b$; - ‘class’ is an archaic synonym for ‘set’ or ‘subset’ (that now has another meaning, related but somewhat technical);
- if you identify the equivalence class of $a$ (the axiomatic $[a]_R$) with the equivalence set of $a$ (the subset of $X$, or element of the power set of $X$), then the set of equivalence sets modulo $R$ has the defining properties of $X/R$.

But you do not normally think about these equivalence sets when working with the quotient set.

I never used the word ‘isomorphism’, at least not precisely. But we had ‘bijection’, and I emphasized that a bijection between two sets allows us to use either for the purposes of the other. So for example, if you have a set $P$ of people and you wish to record some information about them, then you might want to use a bijection between $P$ and $\{1, 2, \ldots, n\}$ (or $\{0, 1, \ldots, n - 1\}$, since the students were mostly CS majors) for some natural number $n$, then refer to each person by the corresponding number. This well-known idea illustrates the power of isomorphism.

]]>Okay, I added some nuts-and-bolts details on the delooping bicategory to delooping; if anyone is so inclined, one could copy and paste to create a stub for delooping bicategory. :-)

]]>So I think Lawvere’s instructions (as a young instructor at Reed College circa 1964) were to teach a year-long foundationally-oriented course building to the basic theory of real analysis, meaning that it was to introduce students to some set theory before starting in on analysis proper. Apparently Reed had a departmental tradition of emphasizing “foundations”. Naturally I don’t know how successful Lawvere’s experiment was, although I think in his ETCS paper, he says it was.

But yeah, circumstances in which one would teach ETCS per se to undergraduates might be a tad unusual. Even in the best universities, it would be somewhat unusual to have students lining up to learn ETCS (when so much else is on offer). But I could see doing it as an independent study.

All that said, I do think it’s viable to promote a structuralist spirit in an introductory courses in modern mathematics (abstract algebra, topology, real analysis) where sets are treated as bags of dots with names, and universal mapping properties are introduced although not necessarily by that name. Certainly I tried that type of thing when I was teaching; I figured that sooner or later they’re going to have to learn this if they want to pursue mathematics. Mostly though it was not formal, more like on-the-job training with the idea it eventually it seeps in with enough gentle repetition.

I don’t see comparable advantages to teaching sets in terms of a cumulative hierarchy conception, unless it was to prepare students who wanted to go into set theory as mathematicians (and who should therefore learn the traditional points of view).

]]>That’s helpful; but I still think it would be useful to have a page about the delooping bicategory specifically that doesn’t require delving into $(n,k+1)$-categories, since it’s quite a simple special case and useful to build intuition for the general one.

Of course, if I really felt that strongly about it I would write such a page myself…

]]>(Also, I’m amused that your comment on that MO thread has more upvotes than the answer itself.)

]]>There’s some sense to that. But I still can’t imagine trying to teach ETCS to undergraduates. Maybe I’m an old hidebound fuddy-duddy, but I can’t imagine anyone really understanding the idea that “mathematics should be invariant with respect to isomorphism” until after learning some abstract algebra or point-set topology or some kind of abstract mathematics where you get to work with isomorphisms, whereas students need some kind of understand of what a “set” is *before* they can learn such a subject in the first place.

There probably isn’t a unique way to analyze any English sentence to decide which maps are coercions and which aren’t.

]]>Makes sense.

]]>Okay, I added a brief section to delooping, titled “Delooping of higher categorical structures”. But actually, Charles’s question might have been headed off at the pass had “delooping” there pointed instead to delooping hypothesis, which seems to give adequate explanation. (But no need to point it there now, as my edit takes care of it (and also mentions **delooping bicategory** specifically).)

in mathematical practice, we deal with elements, subsets, functions, and relations pretty directly, and

material[my emphasis] set theories tend to either have these as primitive notions or treat them with minimal encoding.

Toby, did you mean to say “structural” there?

I assume so, and it seems to be the main point. Recall that Lawvere introduced ETCS for pedagogical purposes, when he was teaching an undergraduate course: it connects directly with practice.

And by golly, I think structural set theory *does* promote a right set of values for modern practice (invariance with respect to isomorphism), that even very fine mathematicians occasionally forget when they think in terms of a membership-based set theory with an extensionality axiom. I’ll give two examples. The first is quoting Lawvere (the full quote can be found here:

The possibility of rejecting the rigid epsilon chains as a ‘foundation’ for mathematics occurred to many around 1960. But for me the necessity for doing so became clear at a 1963 debate between Montague and Scott. Each had tried hard to find the right combination of tricks which would permit a correct definition of the fundamental concept of a model of a higher-order theory (such as topological algebra). Each found in turn that his proposal was refuted by the other’s counter example (involving of course unforeseen ambiguities between the given theory and global epsilon in the recipient set theory).

The whole difficulty Montague and Scott were having seemed in utter contrast with what I had learned about the use of mathematical English and what we try to make clear to students: in a given mathematical discussion there is no structure nor theorem except those which follow from what we explicitly give at the outset. Only in this way can we accurately express our

knowledge ofreal situations. A foundation for mathematics should allow a general definition of model for higher-order theories which would permit that crucial feature of mathematical English to flourish, confusing matters as little as possible with its own contaminants. We are constantly passing from one mathematical discussion to another, introducing or discharging given structures and assumptions, and that too needs to be made flexibly explicit by a foundation.

Now of course I have no idea what specifically transpired in the debate, but if difficulties of that sort exist for professional logicians, then that too is telling. (Again Lawvere brings the discussion back to practical usage and to students.)

The second example comes from a brief MO comment thread, where one participant (with a solid reputation) says, “But the point is that there is no universally agreed upon definition of what the “disjoint union” of two nondisjoint sets is. Or is there? (I suppose if you forced me to give one, I would put $A \coprod B = A \times \{0\} \cup B \times \{1\}$, but surely not everyone agrees with this?)”.” I can’t think of a realistic scenario where that *should* be the point, but the reflex to pin down a notion or structure up to equality does seem to be a long-ingrained habit that I think is further promoted by working with membership-based frameworks where equality of sets is absolute (not contextual).

Thanks! I’m really glad you’re filling in these model-theoretic entries.

]]>Well, delooping can be seen to apply to structures in the periodic table, so that’s where I’d put the level of generality. The notion of delooping bicategory could be in a list of examples.

]]>Considering, say, the predicate on cats of being black. When I say ’The cat sitting on this mat is black’ am I coercing along the projection from the dependent sum, or is ’the cat sitting on this mat’ already just a cat?

Coercion is maybe quite common anyway, and I’m further mapping that cat to $Object$ where Black is first defined.

]]>Ah good, thanks. That makes splendid contact with something that was said at the last Bristol conference on Philosophy and HoTT.

Recall that idea of mine that we might try to make sense of ’the structure of $A$’ as arising from a contractible type

Structure of $A$ := $\sum_{(X: Type)} Equiv(A,X)$.

The objection was raised that this entails that all ’Structure of X’s are identical as each is contractible.

So I could have $P: Type \to Type$, $P(X) = Equiv(A, X)$. The dependent sum from this is my ’Structure of $A$’ and is contractible, hence we can introduce the element

the structure of $A$: Structure of $A$.

Returning to the ordinary language case of a singleton subtype. Say I have a type $Cat$, and a predicate $S(x)$ := Sitting on this mat$(x)$’ which applies to only one cat. Then the dependent sum ’Cat sitting on the mat’ is a singleton, so a candidate for ’the introduction’.

But maybe I’d be better off remembering the projection to $Cat$ and arrange things so that ’the cat sitting on the mat’ is in fact an element of $Cat$ rather than of $Cat\;sitting\;on\;this\;mat$.

So a general rule for ’the introduction’ could be that when we have $P: A \to Type$ and the dependent sum is contractible as witnessed by $(a, b)$, $a: A$ and $b:P(b)$ (along with proof $p$ that any other element in the dependent sum is equal to $(a, b)$, then

the $A$ that is $P$ := $a: A$.

In the Structure case, this would give me ’the structure of $A$’ as an element of $Type$, and I can choose any type equivalent to $A$.

]]>To fill in a grey link (though creating several more in the process), I’ve created Keisler-Shelah isomorphism theorem: two structures have the same theory iff they have an isomorphic ultrapower.

]]>Yes, that’s what is meant. But it’s clearly a problem if we use that term and can’t give a link that succintly explains what it means! Should have a dedicated page called delooping bicategory? It’s certainly an important idea.

]]>For instance, every element of a set defines a singleton subset of that set. But *as sets in isolation*, each singleton is isomorphic to each other singleton. It’s only when we consider them together with their predicates or inclusions to the original set that they are distinguishable.

Well, once we construct the dependent sum, it is just a type. Remembering how it was constructed is tantamount to remembering $P$ itself or the projection to $A$.

]]>It tells us something, but I’m not sure that it tells us that structural set theory is “better” as a foundation for mathematics. Once that encoding has been done (and it’s not really *that* much encoding, relatively speaking), is there any real disadvantage to the fact that we had to do it?

Charles, I believe what is meant is that $\mathbf{B}(\mathcal{C})$ has one object, and the endomorphism category at that object is $\mathcal{C}$, with 1-cells composed by the monoidal product. This delooping is parallel to what we call around here the delooping of a group $G$, namely the one-object category whose hom is given by $G$. I think under this reading, the nLab article is correct.

]]>So dualizable object offers the following as its definition:

An object $A$ in a monoidal category $(\mathcal{C}, \otimes, 1)$ is **dualizable** if it has an adjoint when regarded as a morphism in the one-object delooping bicategory $\mathbf{B}\mathcal{C}$ corresponding to $\mathcal{C}$. Its adjoint in $\mathbf{B}\mathcal{C}$ is called its **dual** in $C$ and often written as $A^*$.

It then goes on to assert that this is equivalent to a more conventional definition (involving certain maps $A^*\otimes A\to 1$, $1\to A\otimes A^*$, etc.). I can’t figure out what the above definition is saying, because the links don’t explain to me what a “delooping bicategory” is supposed to be. (They tell me what “delooping” is, and what a “bicategory” is. This does not help.)

One guess is that $\mathbf{B}\mathcal{C}$ is supposed to have one object, and the endomorphism category of that object would be the functor category $\mathrm{Fun}(\mathcal{C},\mathcal{C})$ (in which case its actually a 2-category). Thus you would “regard” an object of $\mathcal{C}$ as a morphism in $\mathbf{B}\mathcal{C}$ by means of a functor $\mathcal{C} \to \mathrm{Fun}(\mathcal{C},\mathcal{C})$ sending $X$ to $X\otimes -$. If this is so, then its not clear to me that the asserted equivalence of definitions holds, because this $\mathcal{C} \to \mathrm{Fun}(\mathcal{C},\mathcal{C})$ is not likely to be fully faithful.

Perhaps what is meant is that $\mathbf{B}\mathcal{C}$ is built, so that the endomorphisms of the object are a category whose objects are $(F,\gamma)$, where $F\colon \mathcal{C}\to \mathcal{C}$ is a functor, and $\gamma$ is a natural isomorphism $\gamma_{X,Y}\colon F(X)\otimes Y \to F(X\otimes Y)$, satisfying some evident properties (“right-module endofunctors”, i.e., the thing used in the usual proof of the MacLane strictness theorem), so that we get a fully faithful embedding. This seems more plausible, but it is certainly not spelled out.

Another way to describe the issue is as follows. Given an object $A$, suppose we know that the endofunctor $A\otimes-$ admits a right adjoint, which I’ll denote $[A,-]$ (note that I’m not assuming that internal hom exists in general, just for $A$). The first way of reading the above definition appears to assert that $A$ is dualizable if such a right adjoint exists, and if there exists an object $A^*$ and a natural isomorphism $A^*\otimes- \approx [A,-]$ of functors. I don’t believe this is correct, because it does not specify enough about the nature of the natural isomorphism.

Here’s a statement which I believe is correct: $A$ is dualizable iff there is a right adjoint functor $[A,-]$ such that the “evident” natural map $A^*\otimes X \to [A,X]$ is a natural isomorphism, where $A^*:=[A,1]$, the “evident” map being constructed from the data of the adjunction. This is Proposition 2.3 of Deligne, “Categories Tannakiennes”.

]]>In section 3.5 of the HoTT book it considers

$P : A \to \mathcal{U}$ is a family of mere propositions

and then forms the dependent sum $\sum_{(x:A)} P(x)$. Then as to whether to call this a subtype, it says

We may also refer to $P$ itself as a subset or subtype of $A$; this is actually more correct, since the type (3.5.2) [the dependent sum] in isolation doesn’t remember its relationship to $A$.

What does ’in isolation’ mean here? Can the dependent sum be given without information about how it has been constructed, and so then with its projection to $A$?

I’m looking at this as I’m still tweaking my ’the structure’ paper, and was thinking that many uses of ’the’ arise when a $P$ above gives rise to a singleton (or contractible) $\sum_{(x:A)} P(x)$.

]]>No worries! It was on my G+ post :-)

]]>Urs, I don’t think I understand the question. Could you give an example of what you mean?

]]>