The Structure of A

April 12, 2015

Posted by David Corfield

$MathML-enabled post (click for more details).$

I attended a workshop last week down in Bristol organised by James Ladyman and Stuart Presnell, as part of their Homotopy Type Theory project.

Urs was there, showing everyone his magical conjuring trick where the world emerges out of the opposition between $\emptyset$ and $\ast\;$ in Modern Physics formalized in Modal Homotopy Type Theory.

Jamie Vicary spoke on the Categorified Heisenberg Algebra. (See also John’s page.) After the talk, interesting connections were discussed with dependent linear type theory and tangent (infinity, 1)-toposes. It seems that André Joyal and colleagues are working on the latter. This should link up with Urs’s Quantization via Linear homotopy types at some stage.

As for me, I was speaking on the subject of my chapter for the book that Mike’s Introduction to Synthetic Mathematics and John’s Concepts of Sameness will appear in. It’s on reviving the philosophy of geometry through the (synthetic) approach of cohesion.

In the talk I mentioned the outcome of some further thinking about how to treat the phrase ‘the structure of $A$ ’ for a mathematical entity. It occurred to me to combine what I wrote in that discussion we once had on The covariance of coloured balls with the analysis of ‘the’ from The King of France thread. After the event I thought I’d write out a note explaining this point of view, and it can be found here. Thanks to Mike and Urs for suggestions and comments.

The long and the short of it is that there’s no great need for the word ‘structure’ when using homotopy type theory. If anyone has any thoughts, I’d like to hear them.

Posted at April 12, 2015 2:01 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2817

144 Comments & 0 Trackbacks

Re: The Structure of A

$MathML-enabled post (click for more details).$

Nice! (Nit: “Introduction to Synthetic Mathematics” isn’t the title of my chapter, just a blog post excerpted from a first draft of it — not much of which may make it into the final version at all.)

In section 3 you say

I claim that the only plausible candidate for ‘Structure of $A$ ’ is the type $Structure(A) = \sum_{X:U} Equiv(A,X)$

but I don’t see an immediate justification of that claim in the note. I suppose section 4 could be read as a sort of justification, but it’d be interesting to see if this can be justified on its own, prior to applying “the” to it.

One general principle (often honored in the breach) is that for a type to be called $foo$ , it ought to be the case that “ $x:foo$ ” means “ $x$ is a foo”. This convention is in force when calling the universe “ $Type$ ”, and also for examples like $List(A)$ and $Equiv(A,B)$ . So if we want to pronounce $\sum_{X:U} Equiv(A,X)$ as “structure of $A$ ”, it ought to be the case that $x:\sum_{X:U} Equiv(A,X)$ means “ $x$ is a structure of $A$ ”. That’s not quite grammatically correct, but I think a sufficiently generous reader could interpret it as meaning that $x$ is a structure of the same sort as $A$ , or that $x$ has exactly the same structure that $A$ does. Which seems roughly correct: if $x = (B,f)$ then the equivalence $f$ allows us to transport any structure possessed by $A$ over to $B$ in a canonical way.

Did you have an argument like this in mind?

Posted by: Mike Shulman on April 13, 2015 11:49 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Thanks!

As for the point about “I claim that the only plausible candidate…”, no, I don’t have have a prior justification. Given the section before, $Structure(A)$ needs to be contractible. Could there be something to say about possible solutions to

$X: Type \vdash F(X): Type,$

such that $F(X)$ is contractible?

In the case of topological spaces, is there some universal process of making a space contractible through a path space construction?

As for the grammatical point, $x: Structure(A)$ rendered as ‘ $x$ is a structure of the same sort as $A$ ’, would mean we’d have to say

$(A, id_A)$ is a structure of the same sort as $A$ ’,

which perhaps sounds odd.

$x$ is $A$ -structured,

any better?

Maybe we could think about the grammar of the path space version. If I want to indicate a type of cities from which London can be reached and a designated route, what would I say?

Posted by: David Corfield on April 14, 2015 9:44 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

we’d have to say “ $(A, id_A)$ is a structure of the same sort as $A$ ”, which perhaps sounds odd.

Well, we have the same problem whenever we use Sigma-types to implement subsets. For instance, the type of positive real numbers is $\sum_{x:\mathbb{R}} (x\gt 0)$ , but if $(x,p)$ is an element of that type then it sounds odd to say “ $(1,OneIsGreaterThanZero)$ is a positive real number”. I would probably say that there’s another general principle whereby $(x,p):\sum_{x:X}P(x)$ can be pronounced as “ $x$ is an element of $X$ such that $P(x)$ (as witnessed by $p$ )”. So we could say “ $A$ is a structure of the same sort as $A$ (as witnessed by $id_A$ )”.

The space of based paths (or singleton type $\sum_{x:X} (a=x)$ ) does have a sort of universal property: it’s the factorization of $x : 1 \to X$ into an equivalence followed by a fibration.

Posted by: Mike Shulman on April 14, 2015 6:25 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

(I don’t suppose the talks were videotaped?)

Posted by: Mike Shulman on April 13, 2015 11:51 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

No, there were no videos.

On the first day we had an introduction to HoTT by Stuart, then a discussion of whether a notion of identity could be defined via indiscernability in $HoTT^{-}$ (something like HoTT without the identity types) by James. After lunch we had Urs’s talk, and then Teru Thomas speaking about how HoTT and current varieties of structuralism fit (badly with so-called ‘object structuralism’).

It might be interesting to see what sense could be made of recent structuralist writings from the perspective of my note. E.g, when Shapiro writes

…grasping a [mathematical] structure and understanding the language of its theory amount to the same thing. There is no more to understanding a structure and having the ability to refer to its places than having the ability to use the language correctly. (Shapiro, Philosophy of Mathematics: Structure and Ontology, 1997, p. 137)

we should wonder what these ‘places’ are. Can I form ‘Places of Structure(A)’? I can’t say that’s obvious to me. You can see that the thought is to abstract something from what is common to two entities with the same structure, e.g., the third natural number is supposed to be a place in the natural number structure. But then we might say that there’s no need to abstract if you work with a structural language.

On the second day, we had me up first, and you’ll be able to read all about that in Landry’s book. Then there was Dimitris Tsementzis, arguing that the most interesting thing for philosophy of physics about HoTT is what Urs is doing with the cohesive version. Then Jamie spoke on categorified Heisenberg algebras, and the day was rounded off by a group discussion about representation.

Posted by: David Corfield on April 14, 2015 9:33 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

If I understand correctly what a “place” is supposed to be, then I would probably say that “places of” is just the first projection $Structure(A) = (\sum_{X:U} Equiv(A,X)) \longrightarrow U$ .

Posted by: Mike Shulman on April 14, 2015 6:18 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I’m not sure I see this. Why not what you have in the comment below?

…we happen to call structures “types” and their places “elements”.

And by “element” you mean “term”?

we can regard a term $a : A$ as … an element of the type $A$ … (HoTT Book, p. 8)

Posted by: David Corfield on April 15, 2015 6:51 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I think I like that better. But if $Structure(A)$ does mean $\sum_{X:U} Equiv(X,A)$ , then the closest correspondent to “elements = places” would be that the places are the elements of the type $X$ in a pair $(X,f):Structure(A)$ .

(Yes, “term”, “element”, “point”, etc. all mean the same thing roughly. I generally try to avoid “term” because it has connotations of syntax, unless I actually do want to talk about syntax.)

Posted by: Mike Shulman on April 15, 2015 9:04 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

We seem to want some kind of coherent section, picking out an element $a$ of $A$ at the same time as all the inverse images according to the equivalences.

No time right now (for shared writing deadline reasons) to work out how to phrase that, but it should be easy to say.

Posted by: David Corfield on April 15, 2015 10:29 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

As ever, I think you’re right. So it’s

$(X, f): Structure(A) \vdash PlacesIn(X, f) \equiv X: Type.$

And we can transport any elements of $PlacesIn(B, f)$ to $PlacesIn(A, Id_A)$ .

Posted by: David Corfield on April 15, 2015 5:01 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

That (coherent section) seems to me like an artifact of people trying to encode “structure” by abstracting it away from ZF-sets. In type theory it shouldn’t be necessary.

Posted by: Mike Shulman on April 15, 2015 7:05 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Oh, sorry, crossed comments (and little excuse for me, with a 2 hour delay). (-:

Posted by: Mike Shulman on April 15, 2015 7:07 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

But such a coherent section can now be naturally expressed at least:

$p: \prod_{(X, f): Structure(A)} PlacesIn(X, f).$

How would we pronounce this type?

Posted by: David Corfield on April 16, 2015 7:41 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

And I guess that dependent product is equivalent to $A$ .

Posted by: David Corfield on April 16, 2015 10:00 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Ah, right! My brain must have been turned off, because I was trying to do something fancier. But you’re right, that’s exactly what it should be, and it is equivalent to $A$ exactly because $Structure(A)$ is contractible with center $(A,id)$ . Nice!

Posted by: Mike Shulman on April 16, 2015 11:38 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

there’s no great need for the word ‘structure’ when using homotopy type theory.

Perhaps a more positive-sounding way to say the same thing would be that types in HoTT are structures. The idea that a “structure” is something that has to be “abstracted” from an underlying set-like thing comes from material set theory, where any particular set has lots of non-structural information. But in HoTT, we don’t need to perform the same abstraction: we can consider HoTT to be a “synthetic theory of structures”, in which we happen to call structures “types” and their places “elements”. Univalence then says that if we have an isomorphism between the places of two structures, then they are in fact the same structure, just as we would expect.

Posted by: Mike Shulman on April 14, 2015 6:52 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Thinking about all this in the context of space-time, ‘place’ has a more literal meaning.

There should be very natural ways to avoid the mistakes of the hole argument using (informal) HoTT language.

Posted by: David Corfield on April 15, 2015 7:19 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I’m actually planning to use the hole argument in my chapter, as an example of why we need to remember specific isomorphisms. But I haven’t yet thought of a way in which HoTT language improves its treatment over the nLab discussion.

If we define spacetimes in the “structural/univalent” way (of the two I described in my last post), then it seems that we are in more or less exactly the same situation as under a classical foundation, talking about transporting metrics across diffeomorphisms. I guess one could mention that path induction implies that Einstein’s special case ( $\phi=id$ ) is in fact generic, but I’m not sure that that really adds much to the discussion.

It seems that there ought to be more novel to be said if we use the “Erlangen” approach, defining the type of spacetimes as a HIT; but I don’t see what yet. One issue that I haven’t gotten past yet is that the hole argument seems to rely on the fact that a single manifold can have more than one metric on it, which seems to belong more to the “structural/univalent” approach. Maybe a hybrid approach is called for, defining the type of manifolds as a HIT and then talking about metrics as structure on it?

Posted by: Mike Shulman on April 15, 2015 7:14 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

So far we’re talking about “the Structure of A”. Has there been any interest in the philosophical community in simply defining what “a structure” is? It seems to be that it would be preferable to be able to talk about structures without talking about examples of those structures. Of course, in HoTT, there should be an equivalence between the type of structures and the type of types (or maybe not quite – perhaps in addition there should be “the inconsistent structure” – more on this below).

So what is a structure? Well, I’m unsure about how the higher homotopy works out here, but here’s my understanding at the 1-truncated level: The structure of A, as David has defined it, is basically the slice groupoid $\mathrm{Type}/A$ , where $\mathrm{Type}$ is the groupoid of types and equivalences. A point of “the structure of $A$ ” a carrier type $X$ along with an equivalence to $A$ equipping it with an $A$ -structure.

So maybe we could define a structure to be an indiscrete groupoid $I$ . That’s not quite right: we also need a forgetful functor $U: I \to \mathrm{Type}$ , taking a point of the structure to its carrier type. Moreover, we need a certain “surjectivity”: we need to know that if $p: Y \sim F(x)$ , then there is $q: y = x$ such that $F(y) = Y$ and $F(q) = p$ . This says that every possible way to exemplify our structure “counts” as exemplifying the structure.

I believe the surjectivity /fibration requirement is redundant in HoTT. So basically a structure is a map from an indiscrete 1-type to $\mathrm{Type}$ .

Now, there is an equivalence between indiscrete 1-types and propositions: the empty indiscrete 1-type is equivalent to the empty type while all others are equivalent to the contractible type. So this means that a structure is either the map $0 \to \mathrm{Type}$ or else it is a point of $\mathrm{Type}$ . So the type of structures is the disjoint union $\{0 \to \mathrm{Type}\} \amalg \mathrm{Type}$ . I’d interpret this to say that a structure is either inconsistent, or else it is exemplified by a type in HoTT.

Wait – isn’t the inconsistent structure exemplified by the empty type? I think not. The empty space is a perfectly good space, and there are properties it doesn’t have – e.g. the property of being inhabited. So the theory of the empty space is consistent. The inconsistent structure is exemplified by any type which has an inconsistent theory – a type which is both inhabited and not inhabited for example. Of course, there are no such types, not even the empty type.

Posted by: Tim Campion on April 18, 2015 3:17 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I don’t think I would consider the “inconsistent structure” as a structure.

Posted by: Mike Shulman on April 18, 2015 7:12 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I don’t think I would consider the “inconsistent structure” as a structure.

I don’t know about the specific arguments here but “the” inconsistent structure or “a” one (say where some substructure is inconsistent/contradictory/non-existent) can be talked about. How else would you record the structure of a proof by contradiction other than by saying it contains a contradiction? Or should just an empty proof be used to indicate failure?

Posted by: RodMcGuire on April 18, 2015 11:03 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

You yourself pointed out that the empty structure is consistent.

Posted by: Mike Shulman on April 19, 2015 5:27 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

More specifically to your proposal, the slice groupoid $Type/A$ is not just indiscrete, but inhabited, and hence contractible. I don’t see any reason to want to generalize from contractible groupoids to indiscrete ones.

Posted by: Mike Shulman on April 19, 2015 5:35 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Fair enough. The only issue I have with using contractible groupoids is that in order to exhibit a contraction of a groupoid, you need to exhibit an object of the groupoid, i.e. (in this case) an example of the the structure you’re talking about. It just seems to me that it should be possible to talk about a structure without exhibiting a distinguished example of it.

Maybe I’m a little confused about what is really meant by “structure”. What would be an example of an object in ordinary (mathematical) language whose “structure” we might consider? Are we trying to capture examples like “the structure of the group $\mathbb {Z} /2$ ”? If so, what would $A$ be in this case? Is it just the carrier set $\{0,1\}$ ?

Posted by: Tim Campion on April 19, 2015 4:20 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

As an example of a type with some additional structure, we might take the HoTT book’s

$Semigroup :\equiv \sum_{A : \mathcal{U}} \sum_{(m: A \to A \to A)} \prod_{(x,y,z:A)} m(x,m(y, z)) = m(m(x, y), z).$

Then for a particular $(A, m, a): Semigroup$ ,

$Str(A, m, a) :\equiv \sum_{(X, y, z): Semigroup} f: Equiv_{Semigroup}((A, m, a), (X, y, z)),$

where $Equiv_{Semigroup}$ requires of an element that it is an equivalence between carrier types and transports the semigroup structure.

Posted by: David Corfield on April 21, 2015 8:40 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

David, what does $Str(A,m,a)$ mean? Tim Campion’s question was, “what is $Str(\mathbb{Z}/2)$ ”? I.e., what is the structure of the cyclic/permutation group $A = (\{0,1\},\oplus)$ ?

Posted by: Jeffrey Ketland on April 21, 2015 4:14 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

$Str(A, m, a)$ is meant to be the type of semigroups with a specified semigroup equivalence to a designated one $(A, m, a)$ .

I chose the semigroup structure as it’s simpler. A few more bells and whistles would give us a type $Group$ . An element of that type will be some kind of tuple $(A, m, a, ...)$ recording the carrier type (which we may require to be a type of hlevel 0, or set), multiplication, proof of associativity, and so on (inverse, identity, and proofs of various equations).

We can specify a particular group in this format to capture the cyclic group of order 2, beginning with a type which is a set of cardinality 2. If we call this group $G$ , then I’d define $Str(G)$ as the type of elements of $Group$ with a designated group-equivalence to $G$ . Then `the structure of $G$ ’ can just be $(G, id_G)$ .

This may not appear much simpler than any other approach, but at least there’s no need to abstract away from the way the group is given in the language to get at its structure. Anything you can say just is structure.

And when later in the HoTT book they develop an account of categories, they manage to set it up so that the natural notion of identity is equivalence in the ordinary category theoretic sense and not the stronger isomorphism. So that’s pleasing.

Posted by: David Corfield on April 21, 2015 9:04 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Ah look, the HoTT book has a cleverer way of defining the cyclic group of order 2 via one relation defined on the free group on one element. See p. 204.

Posted by: David Corfield on April 21, 2015 9:26 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

David, thanks. I see now - your $A$ was originally the argument in $Str(A)$ ; but in your example, $(A,m,a)$ , it means just the domain/carrier set, and $m$ is the operation and $a$ the unit.

Going back to treating $A$ as the group, field, etc., it seems to me that what you’re defining is the equivalence class/isomorphism type,

$Str(A) := \{B \in \mathcal{U} \mid B \cong A\}$

but re-expressed in type-language.

On the second point, equivalent categories $\mathcal{C}$ and $\mathcal{D}$ may have different cardinalities. But do you wish to say cardinality is not a structural property? I’d treat cardinality as the classic structural property - so, if they have different cardinalities, they have different structure (even if some of their objects come in “indiscernible” clusters). If someone shows me graphs $A$ and $B$ with distinct numbers of vertices, I know for sure they don’t have the same structure. Equivalence is then a notion of indiscerniblity, and not sameness-of-structure, because having distant cardinalities is a structural property that distinguishes them.

Posted by: Jeffrey Ketland on April 21, 2015 9:45 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

The definition $\sum_{B:\mathcal{U}} (B\cong A)$ is very much like $\{B\in \mathcal{U} \mid B\cong A\}$ , but it has the crucial difference that the isomorphism $B\cong A$ is retained as part of the data involved in an element of $Str(A)$ . In particular, this means that the type-theoretic $Str(A)$ is contractible whereas the set-theoretic isomorphism class is not.

I would say that categories do not have cardinalities, because in order to give a cardinality to a category you have to be able to ask whether two of its objects are equal (rather than isomorphic), which is not a category-theoretic notion. I mean, of course if you define categories inside of set theory, then such an equality exists and you can talk about cardinality, but it’s no more a part of the structure of a category than $1\in 2$ is part of the structure of the natural numbers.

Posted by: Mike Shulman on April 21, 2015 11:24 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, on the second (cardinality) point, why do you think $1 \in 2$ is connected to this? Suppose $\mathcal{C}$ has one object (say, $c$ ) and $\mathcal{D}$ has two objects (say $c,d$ , with $c \neq d$ ), but $\mathcal{C}$ is equivalent to $\mathcal{D}$ . Why is the distinctness of $c$ and $d$ connected to set theory? They’re just distinct entities, but bear no set-theoretic connections at all.

In order to say “there are at least three things …”, we use the identity predicate, $\exists x \exists y \exists z(x \neq y \wedge x \neq z \wedge y \neq z \dots)$ , but this isn’t connected to set theory.

So, it seems clear to me that the cardinality of a category is essential to its structure, just as when graphs have different numbers of vertices, they differ in structure.

Posted by: Jeffrey Ketland on April 22, 2015 1:04 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Jeff

So, it seems clear to me that the cardinality of a category is essential to its structure,…

What would it take to convince you otherwise?

One may give two different presentations of equivalent categories which employ different numbers of objects, but it doesn’t mean that this is essential to the category’s structure.

The group generated by $a$ with no relations, and the group generated by $b$ and $c$ with the relation $b = c$ are isomorphic. There’s nothing essential to the group’s structure about the number of generators or number of relations.

It’s a very similar case.

Posted by: David Corfield on April 22, 2015 4:42 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

David, “What would it take to convince you otherwise?”

Consider the case you mentioned of groups. Let $G_1 = (X,f)$ and $G_2 = (Y,g)$ be groups. If $|X| \neq |Y|$ , then $G_1$ and $G_2$ do not have the same structure. Do you think that’s incorrect? But then you’re saying that groups with distinct numbers of elements can have the same structure?

Normally, one says groups have the same structure when isomorphic; graphs have the same structure when isomorphic; etc. This is certainly what structuralists like Hellman, Shapiro, Resnik, Ladyman, Leitgeb, and all others have intended to mean by “same structure” (“ante rem structure”, etc.). I know almost all these people: that’s what they mean.

(I agree you’re free to use the word to mean something different from what the relevant authors mean.)

Posted by: Jeffrey Ketland on April 22, 2015 6:13 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Of course isomorphic groups as structured sets have the same number of elements. I was trying to get you to see that already at the level of groups there are some aspects with numbers attached which are not invariants.

Just as the number of generators and relations of a group is not invariant under isomorphism, so the number of objects and morphisms of a category is not invariant under equivalence.

I think we can really boil it down to the simplest example. Construct a groupoid $G$ with two objects $A$ and $B$ and a single isomorphism $f: A \to B$ . This groupoid is equivalent to the groupoid $\mathbf{1}$ .

Now, although I said ‘two objects’, there is no intrinsic two-ness about $G$ . The only cardinality I can associate to $G$ is 1.

The two descriptions of the equivalent groupoids are just two presentations. I can even say it that way: the groupoid freely generated by two objects and an isomorphism between them is equivalent to the groupoid freely generated by one object.

There is no intrinsic notion of the number of objects in a groupoid any more than there is an intrinsic notion of the number of generators in a group.

Whether structuralists such as Hellman, Shapiro, Resnik, Ladyman, Leitgeb haven’t realised this, is neither here nor there. I should hope you’re wrong about Ladyman as he’s been funded to study HoTT.

I’ve been pointing this out for a dozen years, but if people choose to ignore it then what can I say?

Posted by: David Corfield on April 23, 2015 9:13 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

David,

I was trying to get you to see that already at the level of groups there are some aspects with numbers attached which are not invariants.

Run this example again. A group $G = (X,\circ)$ , right? (inverse and identity element are definable, so we can ignore them). A set $Y \subseteq X$ generates $G$ if each $g \in X$ is a finite combination of elements of $Y$ . Now I’m not sure what the point is - what are you saying is not invariant under isomorphism?

Posted by: Jeffrey Ketland on April 25, 2015 11:29 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Why should a group have a unique set of generators? Obviously a group may have more than one set of generators - so I’m completely baffled. Suppose $Gen(G_1)$ is $G_1$ ’s set of generating sets, and $Gen(G_2)$ is $G_2$ ’s set of generating sets. Then an isomorphism $G_1 \overset{f}\cong G_2$ induces a bijection between $Gen(G_1)$ and $Gen(G_2)$ . In particular, $|Gen(G_1)| = |Gen(G_2)|$ .

Posted by: Jeffrey Ketland on April 25, 2015 11:50 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

The analogue for categories of your $Gen(G)$ would be the “set” of all sets that could be the set of objects (of some equivalent category), which is of course a proper class but other than that is indeed an invariant of the category. The cardinality of a specific set of objects for the category would be analogous to the cardinality of a specific set of generators, which as you say is certainly not unique. The key is just to start thinking of “a category” as “only defined up to equivalence”, in the same way that “the cyclic group of order 2” is only defined up to isomorphism.

Posted by: Mike Shulman on April 26, 2015 4:48 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

The analogue for categories of your $Gen(G)$ would be the “set” of all sets that could be the set of objects (of some equivalent category), which is of course a proper class but other than that is indeed an invariant of the category.

And then note the important point that, taking a simple category such as $\mathbf{1}$ , any set can act as its set of objects. For a given such set, just relate these objects by single isomorphisms.

Compare with the case with groups: $\langle a \rangle$ and $\langle a, b | a = b \rangle$ and $\langle a, b, c | a = b = c \rangle$ , etc. are all the same group.

Posted by: David Corfield on April 26, 2015 7:56 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

David, but a group doesn’t have a unique set of generators. Similarly, a vector space doesn’t have a unique basis. Etc. So, the argument by analogy doesn’t work.

Mike (and David), yes, the philosophical idea is to say that if categories are merely equivalent, then they’re “the same”. But, although they’re indiscernible in some important sense, they’re still distinguishable if they’re distinct. As Bishop Butler put it, “Every thing is what it is, and not another thing”.

Posted by: Jeffrey Ketland on April 26, 2015 11:12 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

In our world, a category does not have a unique set of objects either.

Maybe it would help to say this: you are thinking of a “category” as a structure consisting of a set of objects and a set of morphisms and stuff. That sort of structure also exists in our world, but we don’t call it a “category”, we call it a “strict category”. For us a “category” is a different kind of thing which is not put together out of sets. It has a “collection” of objects but that collection is not intrinsically a set, and in particular it does not make sense to speak about “equality” between its objects in any sense other than isomorphism.

We’re not saying something weird and different about things that you’re familiar with; we’re saying that mathematics can and should be extended to encompass a new kind of thing that behaves differently.

Posted by: Mike Shulman on April 26, 2015 5:41 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Re $Str(A)$ , as Mike pointed out, the isomorphism (or whatever notion of equivalence is relevant) is retained. This is crucial. We need it to avoid confusions such as how the complex conjugate acting on the complex numbers seems to make $i$ be the same as $-i$ .

Re cardinality, this seems to be a difficult thing to learn for those who haven’t passed along the category theoretic way, even some now looking at HoTT.

The only good definition of cardinality (invariant under equivalence) for the $n$ -types of HoTT that I know is the one at groupoid cardinality:

$|X| := \sum_{[x] \in \pi_0(X)}\prod_{k = 1}^\infty |\pi_k(X,x)|^{(-1)^k} = \sum_{[x]} \frac{1}{|\pi_1(X,x)|} |\pi_2(X,x)| \frac{1}{|\pi_3(X,x)|} |\pi_4(X,x)| \cdots \,.$

For $0$ -types this gives ordinary set cardinality. For groupoids, we sum the reciprocals of the automorphism groups at one element in each component. This has the fun result that the groupoid $FinSet$ has cardinality $e$ . Adding extra copies of finite sets will make no difference.

Any contractible type will have cardinality 1.

Posted by: David Corfield on April 22, 2015 8:53 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Thanks, David, but let’s define a category to be a 2-sorted first-order structure,

$\mathcal{C} = (O,M,s,t,\circ)$ ,

with collection $O$ of objects, collection $M$ of morphisms, and three partial operations, source $s$ , target $t$ and composition $\circ$ , satisfying the category axioms (cf., a vector space over a field is a 2-sorted first-order structure satisfying the relevant axioms).

It seems to me that $|O|$ is a good definition of $\mathcal{C}$ ’s cardinality (or maybe the pair $(|O|,|M|)$ ). It’s not being invariant under “equivalence” just shows that equivalence does not mean “has same structure”. Equivalence is a notion of indiscernibility, and not a notion of same-structure. (Cf., first-order equivalence is a notion of indiscernibility, not a notion of sameness of structure.)

Posted by: Jeffrey Ketland on April 22, 2015 1:17 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Is there any way forward if I say “So much the worse for first-order equivalence”?

Are you really wishing to commit to there being an answer to the question “In the category of finite sets, how many objects correspond to sets of cardinality 3”?

Presumably you won’t even want to say the category of finite sets since different versions according to your first order description will afford different answers to my question, so won’t be equivalent in your eyes.

Posted by: David Corfield on April 22, 2015 4:51 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

David, “Are you really wishing to commit to there being an answer to the question “In the category of finite sets, how many objects correspond to sets of cardinality 3”?”

I don’t quite get this. $\mathbf{FinSet}$ is a large category, and therefore there is a bijection $f: \mathbf{FinSet} \to V$ . If $\mathbf{3}$ is the class of 3-element sets, then there is a bijection $f : \mathbf{3} \to V$ . But you seem to be saying that $\mathbf{FinSet}$ is not a large category. But surely it is a large category. (It is locally small.)

The concepts “large category” and “locally small category” are defined in terms of the cardinalities of $Obj_{\mathcal{C}}$ , $Mor_{\mathcal{C}}$ and $Hom_{\mathcal{C}}(a,b)$ . So I’m unclear why you’re objecting to these notions, despite their being standard ones used in category theory?

Posted by: Jeffrey Ketland on April 22, 2015 6:30 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

“Locally small category” is about the cardinality of the individual hom-sets $Hom(a,b)$ , and no one is objecting to that. The notions of “large category” and “small category” are indeed not really category-theoretic, and actually not really used very much in category theory either; generally what people really mean is an essentially large or essentially small category. FinSet is essentially small.

Posted by: Mike Shulman on April 22, 2015 8:30 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I do distinguish between strictly small categories and essentially small categories. Otherwise one has to constantly replace “essentially small” sets with strictly small sets all the time, and it is far from obvious to me whether this can be done in a coherent way. (This objection is not specific to material set theory – it still makes sense in homotopy type theory when one is being careful with universes.)

Posted by: Zhen Lin on April 22, 2015 10:56 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I think you’ve got it backwards. The fact that the cardinality of the set of objects is not invariant under equivalence of categories doesn’t mean that equivalence isn’t the right notion of sameness of structure, it means that cardinality is not a structural (i.e. category-theoretic) property. This is what I was trying to say by analogy using the example of $1\in 2$ . Here it is more explicitly:

In ZFC we can consider rings as tuples $(R,+,0,\cdot,1)$ . Of any such ring we can ask whether $0\in 1$ . But this is not a structural (i.e. not ring-theoretic) notion, and not invariant under isomorphism. (Which direction the causality flows there is just a question of how you define “structural”.) If we instead define rings in a more structural foundational system, like ETCS or HoTT, then we can no longer even ask whether $0\in 1$ .

Similarly, in ZFC we can as you say define categories to be tuples $(O,M,s,t,\circ)$ , and for any such category we can define the cardinality of its set of objects. But that is not a structural (i.e. not category-theoretic) notion, and not invariant under equivalence. And again, if we define categories in a more structural foundation, like HoTT (ETCS is no longer structural enough), then we can no longer talk about the cardinality of the set of objects (because there is no longer a set of objects).

Isomorphism is not God-given as the only correct notion of “has same structure”. It’s an empirical observation that many mathematical structures are naturally organized into categories and that isomorphism in those categories is the correct notion of sameness which captures their intended structural properties. But categories are instead naturally organized into a 2-category, and the correct notion of sameness for them is equivalence (in that 2-category), and so on for higher categories.

Posted by: Mike Shulman on April 22, 2015 6:26 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, if one says a category is a 2-sorted, first-order, structure $\mathcal{C} = (O,M,s,t,\circ)$ , why does this relate to ZFC?

One cannot say $1 \in 2$ in ZFC, because the terms “ $1$ ”, “ $2$ ” don’t exist in $L_{ZFC}$ . There is a definitional extension $ZFC^{+}$ in an extended language with these terms. But there are countlessly many such extensions. It’s a matter of convenience. The point is that there is a translation $t : L_{PA} \to L_{ZFC}$ which preserves theoremhood: if $PA \vdash \phi$ then $ZFC \vdash t(\phi)$ . There are many such translations which interpret $PA$ into $ZFC$ . But these are translations, not claims of what is or isn’t.

Posted by: Jeffrey Ketland on April 22, 2015 6:44 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

[I]f one says a category is a 2-sorted, first-order, structure C=(O,M,s,t,∘), why does this relate to ZFC?

It relates to ZFC because without ZFC (more generally: without any other formal system strong enough to provide good semantics for first-order theories) you cannot express the notion $\vert O \vert$ of the “cardinality” of $O$ as you seem willing to do in order to make your points. The cardinality of $O$ is not a notion definable syntactically in the two-sorted first-order theory of categories. It is a notion definable syntactically in ZFC in which we can also define a notion of a model $M$ of the two-sorted first-order theory of categories $T_{\text{cat}}$ . Inside ZFC we can then find two models $M_1$ and $M_2$ of $T_{\text{cat}}$ that are equivalent but which do not have the same cardinality. (What it means to be a model of $T_{\text{cat}}$ and what it means for two such models to be equivalent in the category-theoretic sense can also be defined by formulas in ZFC.) But that is not saying anything about $T_{\text{cat}}$ as a piece of syntax but rather about properties of its models when it is interpreted in ZFC. This is why ZFC is related.

The point here is that in order to make your points about cardinality being part of the structure of a category, you need to refer to a notion of cardinality that is not definable from the two-sorted first-order axioms of a category. The notion you are using is the notion of cardinality defined in ZFC (or similar so-called “material” set theories.) So in order to make your points you need to take your semantics in a system like ZFC - this is why ZFC is relevant. I think Mike and David are not disagreeing with you that these points can be made if you take your semantics in ZFC. They are merely trying to argue that there are other systems (e.g. ETCS and HoTT) which have notions of cardinality that prevent one from making your points. That we should want to take our semantics in such systems is then a matter of “empirical” observation of the practice of mathematics, as Mike also suggests - and certainly up for debate and further reflection. However it seems to me that implicit in all your arguments is that the only correct way to take the semantics of first-order theories is in a material set theory like ZFC and that kind of conviction seems to me unrelated to the question of what the relevant structure of certain mathematical objects is.

Posted by: Dimitris on April 22, 2015 7:54 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Dimitris, I agree it’s true that one can define $card(x)$ for a set $x$ if one wishes. However, there’s no need to do this. One can take $|.|$ as primitive, with axiom,

(C) $|X| = |Y| \leftrightarrow X \sim Y$

where $X \sim Y$ means there is a bijection $F : X \to Y$ . Then we can add (C) to ZFC conservatively.

But (C) doesn’t seem connected to ZFC at all. Of course, if one insists that $|X|$ should be defined, as a set, then it does. But I don’t think it needs to be defined.

Posted by: Jeffrey Ketland on April 22, 2015 9:12 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I agree that it has nothing to do with ZFC. ZFC was just an example of a system in which you can speak of cardinalities. My point was simply that your axiom (C) is not an axiom in the language of the two-sorted first-order theory of categories. It is an axiom that belongs to systems in which this theory is interpreted. ZFC could be one such system.

Posted by: Dimitris on April 23, 2015 4:18 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

It doesn’t relate to ZFC in particular, but it relates to the fact that you are thinking of your first-order structures as having their sorts interpreted by sets, so that you can talk about whether two of their elements are equal. If you prefer to talk in the language of FOL, then the same point would be made by saying that a category should not be defined in a language where the sort of objects comes with an equality relation (more precisely, a set-like equality relation; the HoTT equality is not a problem).

Posted by: Mike Shulman on April 22, 2015 8:21 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, “it relates to the fact that you are thinking of your first-order structures as having their sorts interpreted by sets, so that you can talk about whether two of their elements are equal.”

The sorts $S_i$ of a many-sorted structure $(S_1, \dots; \dots)$ are sets, yes. But their elements aren’t necessarily sets. The elements could be numbers, or anything, really, including non-mathematical things! For example, a vector space is a messy 2-sorted structure (vectors and scalars), but there’s no reason why a vector $v$ or scalar $r$ should be a set.

I think the issue of equality (identity) is the important thing - and not ZFC, which I think is a red herring. Equality (identity) is not being treated as a “global notion”; whereas, for me, identity is a global notion: it makes sense to ask if $x = y$ ? But with type theories, the type-restrictions prevent this (as does the 1920s/30s idea, amongst philosophers, of category mistakes), as in Russell’s, Church’s type theories through to HoTT. I’m pretty sure that lies right at the heart of this debate involving HoTT and other approaches.

Posted by: Jeffrey Ketland on April 22, 2015 9:38 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I agree entirely that the issue has to do with equality. If you are philosophically committed to a global equality predicate, there may not be any more to say. We have various reasons for not wanting or needing such a thing, but if none of them convince you, then I guess we have to agree to disagree.

Posted by: Mike Shulman on April 23, 2015 12:50 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Thanks for the example, David.

In your note, $Structure(x)$ was a type dependent on $x : \mathrm{Type}$ . But in this example, it seems to me that $Structure(X,x)$ is a type dependent on $X: \mathrm{Type}$ and $x: X$ , where in this case we’re taking $X = \mathrm{Semigroup}$ and $x = (\mathbb{Z}/2,+):\mathrm{Semigroup}$ . Is this generalization intentional?

Section 2.14 of the HoTT book shows that equivalence of semigroups agrees with identity of semigroups. So this definition really would generalize to all $X$ : we have

$Structure(X,x): \,\, X: \mathrm{Type},\,x:X \vdash \sum_{y: X} x=y$

So we end up talking about “structure of $x$ , regarded as an $X$ ”, whereas before we had “structure of $x$ , regarded as a type”.

Section 2.14 of the book suggests that this generalization is really not necessary so long as we’re talking about types $X$ which are defined by operations and equations on a carrier type, because if $x:X$ and $|x|$ is the carrier type of $x$ , then any equivalence $|x| = Y$ automatically transports the operations of $x$ to operations on $Y$ .

But perhaps there are types $X$ which are not of this algebraic flavor for which we can legitimately talk about “structure of $x: X$ , regarded as an $X$ ”. For instance, what if $X$ is defined inductively, e.g. $X = \mathbb{N}$ , the natural numbers. Does it make sense to talk about “structure of $n: \mathbb{N}$ , regarded as a natural number”?

Posted by: Tim Campion on April 21, 2015 10:27 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Is this generalization intentional?

I was generalizing from plain types to structured types. I only suggested we go as far as structured types of the form ‘type equipped with…’, so defined as a dependent sum on $Y: Type$ .

Section 2.14 of the book suggests that this generalization is really not necessary…

So certainly an equivalence of carrier types will allow the transport of any structure on one type to a similar structure on the other. But we would still need to keep track of this extra structure. I mean, we could have two non-equivalent structured types whose carrier types were equivalent.

Does it make sense to talk about “structure of $n:\mathbb{N}$ , regarded as a natural number”?

Were we to define

$Str_{\mathbb{N}}(n) : \equiv \sum_{m:\mathbb{N}} Id_{\mathbb{N}}(n, m),$

this would result in any element of $\mathbb{N}$ which is provably equal to $n$ along with its proof. Since $\mathbb{N}$ is a set, $Id_{\mathbb{N}}(n, m)$ is a proposition, so either empty or if inhabited, contractible. (If I’m being constructively sensitive enough.) Essentially, we’d just be gathering terms equal to $n$ .

Things only start to become interesting once there are nontrivial autoequivalences.

Posted by: David Corfield on April 22, 2015 9:08 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Thanks, David. I have some further comments/questions. You said:

I was generalizing from plain types to structured types. I only suggested we go as far as structured types of the form ‘type equipped with…’, so defined as a dependent sum on $Y:Type$ .

I don’t see how this new notion of structure can be dependent on just $Y: Type$ . What is $Y$ in the semigroup $\mathbb{Z}/2$ example?

It sounds to me as though when it comes to kinds of structure of the form “types equipped with…”, you’re advocating a family of constructors $Str_{\mathcal{S}}$ , one for each kind $\mathcal{S}$ of structure. And it seems to me that the constructor $Str_{\mathcal{S}}$ has to be dependant on $Y: \mathcal{S}$ , not on $Y: Type$ . For example, when $\mathcal{S} = Semigroup$ , $Str_{Semigroup}$ is the constructor you defined in your example,

$(A,m,a): Semigroup \vdash Str_{Semigroup}(A, m, a) : \equiv \sum_{(X, y, z): Semigroup} f: Equiv_{Semigroup} ((A, m, a), (X, y, z))$

Would that be accurate?

Now I observed that in light of the fact that invariably $Equiv_{\mathcal{S}} = Id_{\mathcal{S}}$ , we might as well just observe that what we have is $Y: \mathcal{S} \vdash \mathrm{Str}_{\mathcal{S}} (Y) = \sum_{X: \mathcal{S}} X =_{\mathcal{S}} Y$ . But this equality is propositional, so perhaps it wouldn’t do to take this as a definition for the purposes of explicating structure?

I further observed that if we do make this substitution, what we really have is a constructor $Str$ dependent on two pieces of data, $\mathcal{S}: kind of structure, Y: \mathcal{S} \vdash Str_{\mathcal{S}}(Y) = \sum_{X: \mathcal{S}} X=_{\mathcal{S}} Y$ . I suggested that we simply take $kindofstructure = Type$ , but it sounds like you would prefer to restrict to some subtype of $Type$ corresponding to “types equipped with…”. Or, if $Equiv_{\mathcal{S}}$ should be taken as part of the data of the structure $\mathcal{S}$ , perhaps it should be $(\mathcal{S},Equiv_{\mathcal{S}}): kind of structure, Y: \mathcal{S} \vdash Str_{(\mathcal{S},Equiv_{\mathcal{S}})}(Y) = \sum_{X: \mathcal{S}} Equiv_{\mathcal{S}}(X,Y)$ .

Finally, I wasn’t objecting to the “uninterestingness” of the structure of being a natural number. Rather, I was just testing the waters of the possibilities of what “structure” might mean if we allow for exotic notions of “kind of structure”. Another example along these lines, which I think is not uninteresting in the way you describe, would be the structure of a point of the 2-sphere $S^2$ ( i.e. take the kind of structure $\mathcal{S}$ to be $S^2$ ). It’s still uninteresting in the way it needs to be – $Str_{S^2}(p) = \sum_{q: S^2} Id_{S^2}(p,q)$ is still contractible. But the automorphism type $Id_{S^2}(p,p)$ is interesting.

Posted by: Tim Campion on April 23, 2015 3:47 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Would that be accurate?

Yes, that’s right. I’m probably shifting between a term in the type of structured types, $X: \mathcal{S}$ , and an expression of such a term as a tuple which starts with a type, $(X, a, b,...): \mathcal{S}$ .

But this equality is propositional,…

I don’t see that. Why can’t there be many ways to identify $X$ and $Y$ ?

I suggested that we simply take $kindofstructure = Type$

That would take us back to my original formulation, a contractible type of types equipped with an equivalence to $Y$ .

As for the sphere example, are you looking at the higher inductive type defined version (p. 182 of HoTT book), or through the elaborate process of carving out a piece of $\mathbb{R}^3$ .

Posted by: David Corfield on April 23, 2015 8:50 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

But this equality is propositional

Sorry, maybe I’m misusing the term “propositional”, or maybe it’s an ambiguous term. I just meant that it’s not a judgmental equality; I didn’t mean to say anything about the higher homotopy. I think the non-judgmentalness of the the equality between $\sum_{X: \mathcal{S}} X =_{\mathcal{S}} Y$ and $\sum_{X: \mathcal{S}} \mathrm{Equiv}_\mathcal{S}(X,Y)$ might be relevant because after all, they are also (non-judgmentally) equal to the contractible type $1$ , and it certainly wouldn’t seem very enlightening to tell this story with the definition $Str_\mathcal{S}(Y) \equiv 1$ .

Next, I said:

I suggested that we simply take $kindofstructure = Type$

To which you replied:

That would take us back to my original formulation, a contractible type of types equipped with an equivalence to $Y$ .

I’m not sure what you mean. We’ve never left the notion that for any $\mathcal{S}: kindofstructure$ and $Y: \mathcal{S}$ , we should have $Str_\mathcal{S}(Y)$ be a contractible type consisting of $X:\mathcal{S}\,\,$ ’s equipped with equivalences to $Y$ . The difference between this formulation and the original one is that there’s a new parameter, the $\mathcal{S}: kindofstructure$ . Your original formulation was

$Y: Type \vdash Str_{Type}(Y) \equiv \sum_{X: Type} Equiv(X,Y)$

whereas this formulation is more general:

$(\mathcal{S},Equiv_\mathcal{S}): kindofstructure,Y: \mathcal{S} \vdash Str_{\mathcal{S}}(Y) \equiv \sum_{X: \mathcal{S}} Equiv_\mathcal{S}(X,Y)$

Even if we take $kindofstructure = Type$ and require $Equiv_\mathcal{S} = Id_\mathcal{S}$ , it’s still more general:

$\mathcal{S}: Type,Y: \mathcal{S} \vdash Str_{\mathcal{S}}(Y) \equiv \sum_{X: \mathcal{S}} Id_\mathcal{S}(X,Y)$

Lastly, in my $\mathcal{S}=S^2$ example, I’m thinking of $S^2$ as a higher inductive type.

Posted by: Tim Campion on April 23, 2015 4:01 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

…it certainly wouldn’t seem very enlightening to tell this story with the definition $Str_{\mathcal{S}}(Y) \equiv 1$ .

Well, that’s really the punchline. It isn’t very enlightening. $(Y, Id_Y)$ just is `the structure of $Y$ ’, whatever kind of structured type $Y$ is. But that’s not a bug, since all we ever wanted is a synthetic theory of structures, with no need to abstract.

Regarding, the next point about $kindofstructure$ , I see what you mean now.

Regarding the 2-sphere, so now we have a HIT with a point $base : S^2$ , and a 2-dimensional path $surf : reﬂ_{base} = reﬂ_{base}$ in $base = base$ .

So let’s think

$Str_{S^2}(base) = \sum_{q: S^2} Id_{S^2}(p,q)$

which is going to be contractible witnessed by $(base, refl_{base})$ .

Posted by: David Corfield on April 23, 2015 5:44 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Glad to get that squared away.

I think the one thing I’m still confused is the discussion of kinds of structure like $\mathcal{S} = \mathbb{N}$ or $\mathcal{S} = S^2$ . I agree that $Str_\mathcal{S}(p)$ will be contractible for any $p: \mathcal{S}$ , and that that is kind of the point. When I pointed out that $Id_{S^2}(p,p)$ is not contractible, I was trying to respond to your point back here, where you said

Things only start to become interesting once there are nontrivial autoequivalences.

I found this comment puzzling because even if $p: \mathcal{S}$ has nontrivial autoequivalences, its type of structures $Str_\mathcal{S}(p)$ is still contractible, so it doesn’t seem to make any difference to the story of what “structure” means. Were you simply re-iterating that your account of “structure” is deflationary in that $Str_\mathcal{S}(p)$ is always contractible?

Posted by: Tim Campion on April 23, 2015 6:02 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I really just meant that if a type, $A$ , is a set, then when we were looking at $Str_{A}(a)$ it was particularly boring, and we didn’t have to mention the identity for an element of $\sum_{b:A} Id_A(a, b)$ ,

At least if $A$ has higher $h$ -level, then mentioning the equivalence under which something is equivalent to the designated term must be done. So I can’t just say that $\mathbb{C}$ is `the structure of $\mathbb{C}$ ’, but should say $(\mathbb{C}, Id_{\mathbb{C}})$ or $(\mathbb{C}, conjugate)$ .

Posted by: David Corfield on April 23, 2015 6:17 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

David, we got sidetracked, but let’s go back to Benacerraf’s 1965 example and see how it works. Let

$A = (\omega, \leq)$

be the usual wellorder of the finite von Neumann ordinals. And let

$B = (Z, \preceq)$

be the structure obtained by letting $Z$ be the closure of $\{\varnothing\}$ under the singleton mapping. Then, as Benacerraf points out, we have:

$A \neq B$ , but $A \cong B$ .

But, Bencerrraf asks, “which of these is the genuine system of natural numbers wellordered by “less-than-or-equal-to”?” Presumably, neither. So, natural numbers are not sets.

All well and good and extremely well-known. Every first year philosophy student knows this. One answer is that $A$ and $B$ have “something in common” - their “abstract structure”. In particular, Shapiro thinks this is itself structured, and is an abstract “ante rem” pattern isomorphic to $(\omega, \leq)$ (and $(Z,\preceq)$ of course). (And there are other structuralists who agree with this - e.g., Leitgeb and Horsten.) Others simply think it’s not much of a problem, and instead consider the equivalence class $\{C \in \mathcal{U} \mid C \cong (\omega,\leq)\}$ (where we restrict it to a universe, or something like that, to avoid Cantorian largeness paradoxes).

Where $A$ is a structured object, I’ve given a definition of “ $Str(A)$ ” in terms of the propositional function expressed by a certain higher-order categorical diagram formula $\Psi_{A}$ .

But you’ve given a definition of “ $Str(A)$ ”. So, I’m curious about how this works.

Does $Str((\omega,\leq))$ have a carrier set (e.g., of “places”)?
Is $Str((\omega,\leq))$ isomorphic to $(\omega, \leq)$ ?
How do you define “ $p$ is a place in $Str((\omega,\leq))$ ”?

Posted by: Jeffrey Ketland on April 24, 2015 1:01 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I know this was addressed to David, but let me also answer it for my proposed definition, namely $Str(A)=A$ .

Yes, $Str((\omega,\le))$ has a carrier set, namely $\omega$ .
Yes, $Str((\omega,\le))$ is isomorphic to $(\omega,\le)$ .
“ $p$ is a place in $Str((\omega,\le))$ ” means “ $p:\omega$ ”.

The point is that by univalence, we do have $(\omega,\le) = (Z,\preceq)$ (for any appropriate coding of your $\omega$ and $Z$ into type theory). So Benacerraf’s problem vanishes, and there is no need for convoluted attempts to define “abstract structure”. It’s good to find workarounds for problems, but we shouldn’t get so attached to our workarounds that we want to hang onto them even when it is discovered that there’s a way to make the problems go away entirely.

Posted by: Mike Shulman on April 24, 2015 4:01 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, is that a deliberate choice to avoid my

$A: \mathcal{S} \vdash Str(A) = \sum_{X: \mathcal{S}} (A = S),$

where $\mathcal{S}$ is a type of structured types?

It doesn’t amount to much, since both of us agree that very little is gained by forming the $Str(-)$ construction. But yours seems especially redundant.

Given my definition, with $\mathcal{S}$ defined as ordered sets to pick up on Jeff’s questions, I would now answer

No, $Str((\omega,\le))$ is contractible. On the other hand, we could define

$(A, r, f): Str((\omega,\le)) \vdash carrier(A, r, f) : \equiv A: Set,$

where $r$ is the order on $A$ , and $f$ witnesses that $(A, r)$ is isomorphic to $(\omega,\le)$ . This is my $PlacesIn(-)$ construction.

In words, any ordered set that is structurally isomorphic to $(\omega,\le)$ has a carrier set.

Remember my construction was made to find a way to express things like ‘the structure of $(\omega,\le)$ ’ and this is a term of my type $Str((\omega,\le))$ , an obvious choice of which is $((\omega,\le), Id)$ . The carrier of this is of course $\omega$ .

Again, no. $Str((\omega,\le))$ is not isomorphic to $(\omega,\le)$ . On the other hand, any element of $Str((\omega,\le))$ is an ordered set and an isomorphism to $(\omega,\le)$ .
Now I agree with Mike, $p$ is a place in $Str((\omega,\le))$ means $p:\omega$ .

Whichever version of $Str(-)$ we choose, very little hangs on it, as it won’t be used. It’s just here as an exercise to show how thoroughly structural HoTT is.

Everything Mike says after his answers, I agree with. HoTT isn’t just a minor variant on the tools familiar to philosophers. In particular one mustn’t read ‘set’ in the usual material-extensional way as composed of self-subsisting elements.

Posted by: David Corfield on April 24, 2015 9:04 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

To begin with I was going to say, why not just put $Str(A) : = A$ ? As that’s pretty much what Steve Awodey uses in his recent informal “Univalence, …” paper. I mentioned the similarity between what you have suggested, and the usual equivalence class $\{B \in \mathcal{U} \mid B \cong A\}$ , as it seems conceptually so similar, but now you’ve made it clearer that a term in $Str(A)$ has the form $(B,f)$ where $B \overset{f}\cong A$ . Actually, I mucked around with this for several years, 2006-2012 and decided I didn’t like it at all, because it is parameter-dependent: it’s an equivalence class with parameters. It’s not ante rem structuralism at all as Shapiro intended it. Then I decided we have to get rid of the carrier set altogether, and came up with $Str(A) : = \langle \Psi_A \rangle$ . I’m confident that’s a good answer, particularly for applications. It also meshes nicely with the widespread use of skolem terms in mathematics (“ $i$ ” and “ $-i$ ” are skolem terms. So are the terms “ $e$ ”, “ $a_1$ ”, etc., used in describing groups.)

The definition $Str(A) = A$ (Awodey/Shulman) is fine with me, so long as one accepts Univalence, and treating $A$ throughout as a type. So now everything hinges on:

$A \cong B \Rightarrow A = B$ .

That’s the conceptual sticking point. Here’s a query (again, $Z$ is the Zermelo “numbers” in Benacerraf’s example, and $\preceq$ the induced wellorder):

$(\omega,\leq) \cong (Z,\preceq)$ .
So, $Str((\omega,\leq)) = Str((Z,\preceq))$ .
The carrier set of $Str((\omega,\leq)$ is $\omega$ . (Mike)
So, the carrier set of $Str((Z,\preceq))$ is $Z$ .
So, $\omega = Z$ . (!!!)

What went wrong? In other words, for sets we don’t want to say:

$X \cong Y \Rightarrow X = Y$ .

Posted by: Jeffrey Ketland on April 24, 2015 10:18 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Nothing went wrong. I don’t have a problem with $\omega=Z$ . We just have to get used to the fact that with univalence, “ $=$ ” now means isomorphism.

Posted by: Mike Shulman on April 24, 2015 6:17 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

David, I wasn’t deliberately trying to avoid your definition, just trying to find a definition of “Str” that more or less matches the idea that types themelves are already structures.

Posted by: Mike Shulman on April 24, 2015 6:22 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

David, “Everything Mike says after his answers, I agree with. HoTT isn’t just a minor variant on the tools familiar to philosophers. In particular one mustn’t read ‘set’ in the usual material-extensional way as composed of self-subsisting elements.”

It was philosophers who invented these tools, which are well-known to them. Type theory was invented by philosophers (Frege, Russell, Carnap, …), as was lambda-abstraction, many-sorted logic, etc. (I have a graduate student working on type-theory and abstraction.) Much of this is also well-known to undergraduate students as well - for example, even first-year students studying mathematics and philosophy. Again, it was philosophers who made the central points about intensionality and extensionality; it was philosophers who sharply distinguished use and mention; it was philosophers who analysed the notion of identity and indiscernibility; and philosophers who noted the importance of “haecceities” for certain definitions of identity. Again, this is all well-known, and in many cases known to undergraduates.

Posted by: Jeffrey Ketland on April 25, 2015 1:41 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Then why is it proving so hard for Mike and me to convey to you the basic idea of univalence?

I wasn’t denigrating the contribution of philosophers through the ages. In fact, I think we should be trying to emulate Frege, etc. by ensuring that we understanding the foundational needs of the mathematics of our day. But these needs change, and the gulf in general philosophical understanding has widened alarmingly over recent decades.

At some point we need to get to grips with the work of people like Jacob Lurie. Fortunately for us a window of opportunity presents itself in that HoTT should at least be recognisable. Still, I think it’s not so easy to understand without a background in category theory.

Posted by: David Corfield on April 26, 2015 8:37 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

It’s not hard to convey it. The claim that if $A \cong B$ then $A = B$ is a mistake. This is because “ $x = y$ ” means that $x$ is exactly the same thing as $y$ , and doesn’t mean “ $x$ and $y$ are indiscernible”. Likewise the constructivist idea that a proposition is identified with its “proofs”. What is the “proof” of CH? What is the “proof” of those countlessly many $\Pi_1$ -truths which no axiom system captures?

Posted by: Jeffrey Ketland on April 26, 2015 11:23 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Inside of HoTT/UF, it can’t be a mistake, because it’s true. Apparently you don’t like it. We’re trying to explain to you why we like it, and that’s what David was saying is proving difficult. Your comment about philosophers sounded almost like saying that you didn’t like it because it wasn’t invented by philosophers, but I’m sure that’s not what you meant.

Posted by: Mike Shulman on April 26, 2015 5:47 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, I agree it’s true under the revised semantics (for the models concerned). But the revised semantics assigns a new semantic meaning to “=”. Univalence is then a principle like “if $A$ and $B$ are indiscernible one way, then they’re indiscernible some other way”. Of course, then I’m at least clear what the claim is and I don’t think any of those who might raise eyebrows at $A \cong B \Rightarrow A = B$ would demur.

(Strictly speaking, philosophers did in fact invent something very much like this: it’s called supervenience. For example, physically indiscernible objects must be mentally indiscernible.)

Maybe an analogy is with the Brouwerian conclusion that “all functions are continuous”. What occurs here is that the meaning of “function” and “continuous” has shifted, and then, yes, “all functions are continuous” is true. But even so, the average mathematician will be reluctant to adopt those revised meanings for “function” and “continuous”.

Posted by: Jeffrey Ketland on April 26, 2015 6:57 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

The point I made below is that for the most part, the meaning of existing instances “ $=$ ” has not shifted. The meaning of “ $=$ ” has simply been expanded to include other things in situations where it didn’t apply before (identifications in higher $n$ -types). It’s true that there are a few instances of the old meaning of “ $=$ ” that are no longer applicable with the new one, like strict equality between sets; but those instances essentially never arise in mathematics, so they oughtn’t to disturb the average mathematician.

Posted by: Mike Shulman on April 27, 2015 4:44 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, take the two cases we discussed. The Benacerraf problem (Z-“numbers” vs vN “numbers”) and Einstein hole argument problem (manifold $M$ with two metrics $g, g'$ , with $g'$ a pushforward of $g$ ).

For the second, I assumed $g' = \phi_{\ast}g$ , for some diffeomorphism $\phi : M \to M$ , with $g'(p) \neq g(p)$ , for some $p \in M$ , as Einstein set it up. (Einstein had a “hole” and worried about determinism, but all now agree that is a non-issue, and the initial value problem for GR is well-posed, etc.) This gave us $g \neq g'$ ; from which we infer $(M,g) \neq (M,g')$ , even though $(M,g) \overset{\phi}\cong (M,g')$ . So how do these represent the same physical solution? Univalence, though, gives us $(M,g) = (M,g')$ . I think the average mathematician might shrug their shoulders and say, “ok…”. But this latter does seem to imply $g = g'$ , contradicting the above. So, if we keep $g \neq g'$ , it looks like we have to reject

(Proj) $(A,R) = (A,S) \rightarrow R = S$ ,

which seems conceptually more basic. Alternatively, we might maintain (Proj), and instead say, $g = g'$ holds, after all; for the existence of a point $p \in M$ with $g(p) \neq g'(p)$ isn’t sufficient to conclude $g \neq g'$ . I think the average mathematician would demur at that. By analogy, if we have $x \in \mathbb{R}$ with $f(x) \neq h(x)$ , then $f$ and $h$ are distinct functions, even if $h = \phi_{\ast}f$ , for some $\phi : \mathbb{R} \to \mathbb{R}$ . (I concede that a brave mathematician might well say, “actually, $f$ and $h$ are the same function, one is just a diffeomorphic image of the other”.)

For the first, we set up $(\omega,\leq) \cong (Z,\preceq)$ , and then note, as Benacerraf points out, $\omega \neq Z$ , because $\{\{\emptyset\}\} \neq \{\emptyset, \{\emptyset\}\}$ . Now Univalence gives us $(\omega,\leq) = (Z,\preceq)$ . But then I say, “hang on, that implies $\omega = Z$ ”. And you say, you’re ok to conclude $\omega = Z$ (!!). I do think the average mathematician would demur at that.

Posted by: Jeffrey Ketland on April 27, 2015 10:21 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

In fact, in dependent type theory, the implication $(x_0, y_0) = (x_1, y_1) \to y_0 = y_1$ is not even well formed in general. That is because the type of $y_i$ can depend on $x_i$ . Incidentally, this is how the problem of $\pm \sqrt{-1}$ in $\mathbb{C}$ is handled in dependent type theory.

Posted by: Zhen Lin on April 27, 2015 2:19 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Yes, I know, but in the $(M,g)$ case and the $(\omega,\leq)$ case, the type-declarations will be ok; so, e.g., $(M,g) = (M,g')$ will be well-formed. I’m curious about the point about how $\pm \sqrt{-1}$ in $\mathbb{C}$ is handled. The Burgess/Keranen line of argument was that $\sqrt{-1} \neq -\sqrt{-1}$ , but this may violate structuralism - because an automorphism takes $\sqrt{-1}$ to $-\sqrt{-1}$ , so they’re “structurally the same place”, but still distinct. How is this answered?

Posted by: Jeffrey Ketland on April 27, 2015 5:35 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

No, I don’t agree. The type of $(M, g)$ is $\sum_{X : Manifold} Metric(X)$ , the type of $(Z, \lt)$ is $\sum_{X : Set} Order(X)$ , and the type of $(\mathbb{C}, \sqrt{-1})$ is $\sum_{X : Field} Element(X)$ . All of these are dependent sums, so the second projection is dependent. And we must consider them as elements of dependent sums: sticking with the simple example of $(\mathbb{C}, \pm \sqrt{-1})$ , we have $(\mathbb{C}, +\sqrt{-1}) \ne (\mathbb{C}, -\sqrt{-1})$ as elements of the type $\{ \mathbb{C} \} \times Element(\mathbb{C})$ but $(\mathbb{C}, +\sqrt{-1}) = (\mathbb{C}, -\sqrt{-1})$ as elements of $\sum_{X : Field} Element(X)$ .

If there is a moral to take away here, it is that when people say homotopy type theory is the study of equality, it is not entirely facetious.

Posted by: Zhen Lin on April 27, 2015 6:46 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Yes, I agree they’re dependent sums. But I’m not sure you’ve resolved the problem; or at least not sure you’ve resolved the problem Burgess and Keranen raised in their 1999 and 2001 articles:

$(\mathbb{C},+\sqrt{-1}) \neq (\mathbb{C},-\sqrt{-1})$ as elements of the type $\{\mathbb{C}\} \times Element(\mathbb{C})$ …

But Burgess and Keranen asked: why? We agree that $\sqrt{-1}$ and $-\sqrt{-1}$ are “structurally the same”. So, what makes them different? Are they primitively distinct, as a brute fact?

Posted by: Jeffrey Ketland on April 27, 2015 8:09 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

They are different because $i$ and $-i$ are unequal as elements of the set $\mathbb{C}$ . “Why” this is depends on exactly how we constructed $\mathbb{C}$ . The fact that $\mathbb{C}$ has an automorphism which swaps them is totally irrelevant to whether they are different elements. In fact, if we assume classical logic, then any set has an automorphism which swaps any two of its elements, and yet we are perfectly happy to say that sets have distinct elements.

Posted by: Mike Shulman on April 27, 2015 10:21 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike,

They are different because $i$ and $-i$ are unequal as elements of the set $\mathbb{C}$ . “Why” this is depends on exactly how we constructed $\mathbb{C}$ .

This still doesn’t seem to answer Burgess/Keranen’s question: why is $i \neq -i$ , given that an automorphism takes us from $i$ to $-i$ , and they’re therefore “structurally the same”? Burgess and Keranen are asking a fairly exact question about what makes $i$ and $-i$ distinct, and so far I don’t see what the proposal is.

Posted by: Jeffrey Ketland on April 28, 2015 9:57 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

$\pm \sqrt{-1}$ are distinct as elements of $\mathbb{C}$ , but $(\mathbb{C}, \pm \sqrt{-1})$ are equal as elements of $\sum_{X : Field} Element(X)$ . This, if you like, is just a brute fact. If the conclusion you want to draw from this is that $\pm \sqrt{-1}$ are not structurally the same after all, then I have no objections. After all, “structurally the same” does not have a precise meaning for me.

Posted by: Zhen Lin on April 28, 2015 12:32 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

“ $a$ is structurally indiscernible in $A$ from $b$ ” is defined to mean: $\pi(a) = b$ , for some $\pi \in Aut(A)$ . So, $i$ and $-i$ are structurally indiscernible in the field $(\mathbb{C},0,1,+\times)$ . However, $i \neq -i$ , and this is, as you say, a brute fact. But, no, it doesn’t imply $i$ and $-i$ are not structurally indiscernible.

The point is that $i \neq -i$ is indeed a brute fact, as it were; which means that $=$ is treated here as a primitive notion, and not one that is defined in terms of indiscernibility. The fact that $i$ and $-i$ are indiscernible (in a certain sense) does not imply they’re identical. So:

Structural indiscernibility of objects in a structure doesn’t imply identity.

That’s the central point. (This has all been sorted out before, about 10 years ago; and since then there’s been some technical papers about various notions of structure-relative indiscernibility and how they’re interrelated.)

Posted by: Jeffrey Ketland on April 28, 2015 2:28 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

One common definition of $\mathbb{C}$ is as $\mathbb{R}\times\mathbb{R}$ , with the multiplication $(a,b)(c,d) = (a c - b d, a d + b c)$ and so on. With this definition, $i = (0,1)$ and $-i = (0,-1)$ , and so $i\neq -i$ because $(0,1)\neq (0,-1)$ , which in turn is because $1\neq -1$ .

Posted by: Mike Shulman on April 28, 2015 2:30 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, yes, I know. But that response - building up $\mathbb{C}$ from its “analytic” representation in $\mathbb{R}^2$ - is not available to structuralists, who think that $\mathbb{C}$ should be understood independently of a specific construction, as an “ante rem” structured entity, whose places/nodes/positions only have “relations to each other”. Burgess 1999 and Keranen 2001 were criticizing Shapiro/Resnik style structuralism - the idea that the structure $\mathbb{C}$ is an “ante rem” structured object, and doesn’t need to be constructed or built up from sets, etc. Burgess and Keranen both said, in their own way, $i$ and $-i$ can’t be told apart structurally, so what makes it so that $i \neq -i$ ?

In 2005, James Ladyman proposed as a reply that one could use Quine’s notion of “weak discernibility”. He had taken his hint from a couple of papers in philosophy of physics by my Oxford colleague Simon Saunders. So, I’ll write “ $x \sim_A y$ ” to mean: $x$ is not weakly discernible in $A$ from $y$ , and omit the exact definition. And of course, it’s true that $\neg(i \sim_{\mathbb{C}} -i)$ . I’d actually seen this talk by Ladyman and I knew there were counterexamples to this suggestion, in general.

So, in reply, in 2006, I noted various counter-examples: i.e., structures $A$ with distinct elements $a,b$ which are not discernible in this way. I.e., $a \sim_A b$ but $a \neq b$ . (Tim Button, a former student of mine, also gave similar counter-examples.) And I gave some results about this notion, and others, based on a technical paper I wrote and distributed to friends, but I didn’t bother to publish it until 2011. I think the nicest result is, for elements $a,b \in A$ ,

$a \sim_A b \Rightarrow \pi_{ab} \in Aut(A)$ ,

where $\pi_{ab}$ is the transposition of $a,b$ . This, by the way, implies,

if $A$ is rigid, then, for all $a,b \in A$ , $a \sim_A b \Leftrightarrow a = b$ .

So, since Ladyman’s weak discernibility idea doesn’t work, instead, I suggested that the structuralist can just treat “=” as a primitive notion when defining a structure (e.g., a group, field, whatnot).

Then the other structuralists said, “yes, that’s what we think too”. So, Shapiro 2008, Ladyman 2007 and Leitgeb & Ladyman 2008 replied again along those lines, agreeing that in some cases, we just have to treat “=” as an undefined primitive. Shapiro 2008 was also, the first time I think, someone who explained the reference problem for “ $i$ ” and “ $-i$ ” - namely, they are skolem constants. Understood as a field, we have

$(\mathbb{C},0,1,+,\times) \models \exists x \exists y(x \neq y \wedge x^2 + 1 = 0 \wedge y^2 + 1 = 0 \wedge \forall z(z = x \vee z = y))$ .

Then “ $i$ ” is a skolem term for the variable $x$ in this existential quantified formula. One can introduce a second term “ $j$ ” too, for $y$ , but then one shows easily that $j = -i$ .

So, roughly, that’s the history (1999-now), or at least part of it. The remaining part is a small sub-literature on notions of indiscernibility which grew out of that, sometimes applied to problems in the foundations of physics.

Posted by: Jeffrey Ketland on April 28, 2015 4:20 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

If that’s all you were asking, then I guess the answer to your question is “yes, we do it the same way”, because all types, including $\mathbb{C}$ , come with a “primitive” notion of equality.

Posted by: Mike Shulman on April 28, 2015 7:56 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, yes - and the structuralists responding to the Burgess/Keranen objection generally ended up in with the same conclusion anyway. There’s actually a lot less to many of these questions than appears at first sight! But that debate all occurred within the context of standard mathematical logic, no type-theoretic/constructivity/category-theoretic bells and whistles. For pretty much everyone though, the answer is: a structured object – like a field, a group, an ordering etc. – comes with its own primitive identity on the underlying carrier set. By the way: what is your preferred way to refer to these? For model theorist, they’re structures or models (even if they’re $n$ -sorted, or higher-order) or $\sigma$ -structures if you want to make the signature explicit.

Posted by: Jeffrey Ketland on April 28, 2015 9:12 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

what is your preferred way to refer to these?

shrug structures, probably.

Posted by: Mike Shulman on April 29, 2015 5:47 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

shrug structures sounds good. :) I don’t think there’s any “should” about describing differences of meanings – people may choose to use/speak whatever language is most convenient, and the meanings of the logical connectives in some language L will vary depending on the semantics of that language L. They might be classical, or three-valued, or $n$ -valued, or valued in $[0,1]$ , or in some Boolean algebra, etc. Or they might not be many-valued, but rather explained constructively in terms of proofs (or warrants/witnesses/verifications), e.g., BHK, or maybe with Kripke frames, and so on. (There is a topological interpretation of intuitionistic connectives, due to Tarski in the 1930s, developed later by Scott and others. I’m guessing, but maybe this is part of the background of what developed into MLTT.) What I mean by “real debate” is again guesswork - partly down to my own ignorance - but it’s about what the differences are of meanings in $L_{HoTT}$ , as compared with meanings in a classical theory T formulated in some classical FOL or HOL language $L$ , such as $PA$ , $ACA_0$ , $Z_2$ , or $ZF$ , etc. (in particular, what does $Id_A(X,Y)$ mean in $L_{HoTT}$ ?).

Posted by: Jeffrey Ketland on April 29, 2015 3:03 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

in particular, what does $Id_A(X,Y)$ mean in $L_{HoTT}$ ?

Well, if “meaning” means what it gets interpreted by in some semantics, as you seem to be suggesting, then it of course depends on the semantics. In the simplicial set model, it’ll be interpreted by the path-space in $A$ between $X$ and $Y$ .

Posted by: Mike Shulman on April 29, 2015 6:18 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, thanks - yes. But this - simplicial sets, higher category theory - is now where my ignorance does start. Most philosophers who work in areas related to mathematical logic would run a mile from all this algebraic topology/category theory stuff: it’s just too hard. Not type theory or non-classical/constructive logics, which are ok, as are recursion theory, model theory, standard parts of set theory (constructible sets, even forcing models, etc.). But I’m interested in HoTT and in particular what $(A \simeq B) \simeq (A = B)$ means, when you unpack it.

Posted by: Jeffrey Ketland on April 29, 2015 8:53 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Here’s something which might be helpful. I also initially resisted the idea that the identity type in HoTT should be written as “ $=$ ”. One of the things that eventually convinced me is that there is no other candidate to be written as “ $=$ ”. The identity types are the mathematical notion of “equality”. So when you write $e^{i\pi}=-1$ , that “ $=$ ” has to be the identity type $Id_{\mathbb{R}}(e^{i\pi},-1)$ ; the same identity type about which univalence asserts that $Id_{Type}(A,B) \simeq (A\simeq B)$ . So if you accept univalence in some form (which I admit may also be a stumbling block for you), and you want to use the standard notation “ $=$ ” when doing ordinary mathematics, you have to be willing to write univalence as $(A=B) \simeq (A\simeq B)$ .

(Sometimes people argue that “ $=$ ” should be restricted to the special case of $Id_A$ when the type $A$ is a set (a 0-type). However, this also has consequences that they may not intend. For instance, every contractible type is a set, and so this includes also types like $\sum_{B:Type} (A\simeq B)$ (“the structure of $A$ ”!); thus we would still have to say that $(B,e) = (A,id_A)$ for any $e:A\simeq B$ . Moreover, there is the first projection function $pr_1 : (\sum_{B:Type} (A\simeq B)) \to Type$ , so if you say $(B,e) = (A,id_A)$ but are not willing to say $B=A$ , then you have to deny that $x=y$ implies $f(x)=f(y)$ for all functions $f$ , which looks odd to say the least.)

(To be completely correct, it’s true that there is also judgmental/definitional equality. But this is really a technical device and not at all the ordinary mathematical equality; e.g. $e^{i\pi}=-1$ is not true judgmentally.)

Posted by: Mike Shulman on April 26, 2015 7:05 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, I can definitely play along with UF (or, say, Brouwerian intuitionism, or SIA, or ETCS, etc.), without actually thinking it’s the right picture of mathematical reality, all things considered. Thanks to your and David’s clear expositions of what’s involved, I have a much better idea of the four main conceptual points now:

How is mathematical reality organized? UF answer: It is organized into types.
What is identity? UF answer: Identity is $Id_C(-,-)$ , for relevant $C$ .
What is structure? UF answer: $Str(A) := A$ ; or $Str(A) := \sum_{B: Type} (B \simeq A)$ .
Should we assume constructivity - i.e., identify propositions with the type of proofs of them? UF answer: Yes.

I don’t think objections to these rest on ZFC or anything like that. For example, I believe there are numbers, pairs, models and structures, etc., but I don’t believe they are sets. (I think they are sui generis.) Also, I don’t doubt many of the other points: conceptual simplicity; fruitfulness; mathematical power; engaging with mathematical practice in some of the more abstract areas of mathematics (topology, geometry), etc., and well as computational areas too (formalizability using a type-theoretic programming language). These virtues are real and explain the current interest in developing HoTT/UF.

So if I had to write a short piece summarizing the objections to the UF picture, I’d focus on the four guiding principles above.

Posted by: Jeffrey Ketland on April 26, 2015 10:21 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

(4) Should we assume constructivity - i.e., identify propositions with the type of proofs of them? UF answer: Yes.

I don’t agree that that is what HoTT/UF says. It is sort of true that HoTT/UF uses the “propositions as types” paradigm, although modified to include propositional truncation. But I don’t believe that that paradigm should be called “constructivity”, nor that it should be described as “identifying propositions with the type of proofs of them”. The elements of the type corresponding to a proposition are better thought of as “reasons” or “witnesses” why it is true; “proof” has too many other misleading connotations. It’s also not clear that we identify propositions with their corresponding types. And finally, this principle is not tied to constructivity in the sense of constructive logic; at least the HoTT/UF version of it is fully compatible with excluded middle and choice. I discussed this in somewhat more detail in section 4 of the draft I posted recently.

I also wouldn’t really agree with 1-3 as being “the main conceptual points” either. For one thing, “mathematical reality is organized into types” is a pretty empty statement until you know what a “type” is. And David’s and my definitions of “Str(A)” are (I would say) just sort of noodling around and far from fundamental to the theory; most people working on HoTT/UF wouldn’t even think of considering a question like “what is structure”. Instead, univalence itself ought certainly to have a place in any list of the main conceptual points of HoTT/UF.

For what it’s worth, let me also mention that in my opinion, a foundation for mathematics should be evaluated only on its value to mathematics, in the same way that a programming language should be evaluated on its usefulness to programmers. If it seems wrong to philosophers for extra-mathematical reasons, that’s too bad, but it probably just means their intuitions need re-training.

Posted by: Mike Shulman on April 27, 2015 4:40 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I definitely agree the evaluation should depend mainly on those factors. But it’s my mathematical intuition that tells me the meaning of, e.g., $Con(ZFC + extras)$ , shouldn’t be defined in terms of proofs, witnesses, etc. So, e.g., a statement like $\forall n(f(n) = g(n))$ , with $f,g$ recursive functions, is meaningful independently of there being a proof/witness for it. I’m not sure how central the constructivity issue is for HoTT/UF though. The normal argument, from Hilbert onwards, has been that constructivists wish to revise mathematics for philosophical reasons, but this kind of philosophically-motivated revisionism isn’t justified on mathematical grounds. I.e., mathematical practice supported the classical view (Hilbert) over the constructivist one (Brouwer, Heyting, Weyl).

Posted by: Jeffrey Ketland on April 27, 2015 7:24 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I don’t think there are many constructivists left who want to revise mathematics on philosophical grounds. All the “constructivists” I’ve interacted with do constructive mathematics because it tells us more than classical mathematics does. There are “algorithmic” constructivists, who like the fact that a constructive proof is automatically an algorithm, whereas a classical proof is not. And there are “topos” constructivists, who like the fact that a constructive proof is valid in more models than a classical one is. Both of these modern kinds of constructivism have a value supported by mathematical practice, and there are probably others.

But really, the question of constructivism is irrelevant to the question of interpreting propositions as types. It’s perfectly possible to posit LEM and AC in HoTT/UF, thereby destroying the “constructive content” but retaining the fact that propositions are interpreted by types.

The point of using a word like “witness” rather than “proof” is that it can mean whatever we want it to mean. Whatever your favorite statement $P$ is, we define a “witness of $P$ ” to be a thing of which there exists one exactly when $P$ is true. The rules of type theory specialize to the rules of logic, so that e.g. if we have a witness of $P$ and $Q$ then we have a witness of $P\wedge Q$ . The meaning of a statement is not “defined in terms of witnesses”, it’s defined in terms of its constituent parts as usual; witnesses are just the type-theoretic way of tracking that dependency.

Posted by: Mike Shulman on April 28, 2015 5:02 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, just a quick point on the expression “witness” - it comes from model theory. Intuitively, a witness for a formula $\exists x \phi(x)$ is a constant $c$ such that $\phi(x/c)$ is true. In a model $A$ , an element $a \in A$ is sometime called a witness for $\exists x \phi(x)$ if $A \models \phi[a]$ . So, in Henkin’s completeness proof for FOL, we begin with a set $\Delta$ assumed consistent, and aim to define a maximal consistent extension $\Delta^+$ with witnesses. We ensure this by adding “witness statements”, of the form $\exists x \phi(x) \to \phi(x/c_{\phi})$ , adding a constant $c_{\phi}$ for each $\phi(x)$ .

I agree one can say “witness” instead of “proof”, sure. What you’re describing is the BHK interpretation. But the real debate concerns what a witness for $\phi \vee \theta$ is or a witness for $\exists x \phi(x)$ is, or a witness for $\neg \phi$ or $\phi \to \theta$ . For example, under BHK, a witness for $\phi \to \theta$ is a construction/proof that converts a witness for $\phi$ to a witness for $\theta$ .

Posted by: Jeffrey Ketland on April 28, 2015 9:50 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

“Witness” is an English word meaning, among other things, “something serving as evidence”. You’re right that it’s used in Henkin completeness proofs with one precise mathematical meaning, but that’s not the meaning it’s being given here.

What I’m describing is not the BHK interpretation, because BHK doesn’t include propositional truncation. And I’m not sure what you are referring to by “the real debate”. Can you explain how you think the meaning of logical statements should be defined?

Posted by: Mike Shulman on April 29, 2015 5:39 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Perhaps I was wrong to say that what I’m describing is what “a structure” is. Perhaps I should say that a map from an indiscrete groupoid to $\mathrm{Type}$ is a kind of structure, rather than a structure. So the map $0 \to \mathrm{Type}$ is the inconsistent kind of structure.

It’s confusing since the point is really that there is only really one (or possibly zero) structure(s) of each kind.

Posted by: Tim Campion on April 20, 2015 3:18 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Tim, “It’s confusing since the point is really that there is only really one (or possibly zero) structure(s) of each kind.”

There are some posts on this here, here, here and here. The notion I give there I call “the diagram view”, which says that, given a structured object $A$ (an ordering, graph, group, lattice, field, topological space, etc.), the abstract structure of $A$ is a propositional function $\langle \Psi_A \rangle$ , expressed by a higher-order categorical diagram formula $\Psi_A$ , which defines the isomorphism type of $A$ .

(From model theory, the diagram of a model $A$ is the set of atomic and negated atomic formulas true in $A$ , assuming a constant $c_a$ for each $a$ in $A$ .) There’s draft paper on this idea, “Abstract Structure”.

For the example Tim Campion suggested above, suppose $A = (\{0,1\},\oplus)$ , where $0 \oplus 0 = 0 = 1 \oplus 1$ and $0 \oplus 1 = 1 = 1 \oplus 0$ . Then the diagram formula $\Psi_A(X,Y)$ is,

$\exists x_0 \in X \exists x_1 \in X(x_0 \neq x_1 \wedge \forall z \in X(z = x_0 \vee z = x_1 )$ $\wedge Y(x_0, x_0, x_0) \wedge \neg Y(x_0, x_0, x_1) \wedge \neg Y(x_0, x_1, x_0) \wedge Y(x_0, x_1, x_1)$ $\wedge \neg Y(x_1, x_0, x_0) \wedge Y(x_1, x_0, x_1) \wedge Y(x_1, x_1, x_0) \wedge \neg Y(x_1, x_1, x_1)).$

where $X$ and $Y$ are free second-order variables ( $X$ labels the domain and $Y$ labels the distinguished relation, i.e., the binary operation $\oplus$ ).

The formula $\Psi_A$ is a syntactic object, a sequence of symbols. It is categorical: all of its models are isomorphic. Despite being a syntactic object, it expresses a non-syntactic propositional function (its intensional content), denoted $\langle \Psi_A \rangle$ , where propositional functions are assumed to be governed by the principle that logical equivalent formulas express the same propositional function.

Then the abstract structure of $A$ is defined to be $\langle \Psi_A \rangle$ . In particular, all isomorphic copies of $A$ have the same unique abstract structure.

Posted by: Jeffrey Ketland on April 20, 2015 1:58 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Jeffrey, I think one example which your definition may have trouble with is “the structure of the homotopy type of the 2-sphere”. There’s no underlying set to talk about when we’re talking about homotopy types, but it seems to me that if anything has structure, a homotopy type surely does.

Posted by: Tim Campion on April 21, 2015 11:31 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Tim, yes, I agree - the approach I described above builds up from particular representative structured sets/models, and defines what they “have in common”, using roughly the logical diagram, bit by bit, atomically, by listing the elements and specifying every relationship involved. E.g., let $P_1 = (X,\preceq_1)$ and $P_2 = (Y,\preceq_2)$ be a pair of isomorphic partial orders, but distinct. Their structure is identical. But on the point you make, I agree - if there’s no underlying set, then there is no structure involved. So, cardinals like $0, 1, \dots, \aleph_{\alpha}, \dots$ , for example, are not structured. E.g., I can’t see how the number $7$ could be thought to be “structured” unless one is trying to identify $7$ with, e.g., the class of all $7$ -tuples, $\{a_1,\dots,a_7\}$ .

Posted by: Jeffrey Ketland on April 22, 2015 1:36 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Just to be clear, when I said –

it seems to me that if anything has structure, a homotopy type surely does

– I meant it. To me, it seems perverse to deny that the homotopy type of $S^2$ , say, is a structure, and highly structured at that.

There’s been a lot of discussion here of the structure of a category. Perhaps for variety we might toss homotopy types into the ring as well. It’s helpful that spaces-considered-up-to-weak-homotopy-equivalence and spaces-considered-up-to-homeomorphism already have separate names (homotopy types and topological spaces, respectively).

And it’s clear that cardinality of the underlying space is not an invariant of homotopy types.

Posted by: Tim Campion on April 26, 2015 5:26 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

There’s is a fun thought you can have with $S^2$ that taking the Baez-Dolan groupoid cardinality for it, see here, would seem to produce a non-converging infinite product, since the homotopy groups go on for ever. Any yet you’d like it to relate to the Euler characteristic, 2.

Posted by: David Corfield on April 26, 2015 8:08 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Tim,

And it’s clear that cardinality of the underlying space is not an invariant of homotopy types.

Yes, but spaces have the same homotopy type when there is a certain kind of continuous deformation of one to the other. Types needn’t have elements which are all isomorphic! For a silly example, not all structures of the same signature are isomorphic, but all structures of the same signature do have the same “similarity type”. Similarly, define the concept “first-order equivalence type” by saying $L$ -structures $A,B$ have the same first-order equivalence type just if for all $\phi \in L$ , $A \models \phi$ iff $B \models \phi$ . But, by the Lowenheim-Skolem theorem, structures with the same “first-order equivalence type” needn’t have the same cardinality.

The point is that the fact that $A,B$ are indiscernible with respect to certain conditions/properties (“equivalent” somehow) doesn’t automatically imply their identity, or often, even their being isomorphic.

Posted by: Jeffrey Ketland on April 26, 2015 12:08 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Jeffrey, I don’t understand how you could construe my comment as a claim that homotopy equivalent spaces are homeomorphic.

Posted by: Tim Campion on April 26, 2015 3:49 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Tim, I didn’t mean to say you meant they’re homeomorphic. I just mean the spaces are homotopy equivalent - and so there’s no reason for them to have the same cardinality, or be isomorphic, homeomorphic, and so on.

Posted by: Jeffrey Ketland on April 26, 2015 6:29 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Well, right now I think I prefer the notion I suggested here that a structure is the same as a type.

Posted by: Mike Shulman on April 20, 2015 6:23 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

On this view, what type is the structure of the semigroup $(\mathbb{N},+)$ ?

Is the structure the carrier set? This is adequate in one sense, because any equivalence of the carrier set with another type $Y$ allows us to transport the addition on $\mathbb{N}$ to $Y$ . But in another sense this is wrong because it leads us to say that $(\mathbb{N},+)$ and $(\mathbb{N},\times)$ have the same structure because they have the same carrier set.

Posted by: Tim Campion on April 21, 2015 11:02 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

On this view, the phrase “the structure of” is not sensical or necessary. The semigroup $(\mathbb{N},+)$ is itself a structure; there’s no need to build something else called “its structure”.

Posted by: Mike Shulman on April 22, 2015 12:06 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

(The reason I said “a structure is the same as a type” is that at that point, we were only talking about “the structure of $A$ ” when $A$ was a type, so I said that $A$ itself is a structure. Now we’ve moved on to the case when $A$ is a structured type, like a semigroup or a group, but the answer is the same: $A$ is itself a structure.)

Posted by: Mike Shulman on April 22, 2015 12:10 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, let $X$ be the closure of $\{\varnothing\}$ under singleton mapping, $\{.\}$ . Let $x \preceq y$ be defined to be the ordering induced. (The “Zermelo numbers”, in Benacerraf’s 1965 example.) Let $A = (X,\preceq_1)$ be the resulting wellordering. Let $B = (\omega,\preceq_2)$ be the wellorder of the finite von Neumann ordinals. Then, $A \cong B$ , but we have $A \neq B$ - do you think this is incorrect?

Benacerraf pointed out that $A \neq B$ because $\{\{\varnothing\}\} \neq \{\varnothing,\{\varnothing\}\}$ . He concluded (correctly) that “numbers are not sets”. Numbers can be modelled as sets, but this doesn’t imply that they are sets.

The idea of structuralists like Shapiro (1997), Resnik (1997) et al is that $A$ and $B$ have “the same structure” - Shapiro calls it an “ante rem structure”, it is the abstract structure that all copies of $A,B,...$ have in common.

Posted by: Jeffrey Ketland on April 22, 2015 2:14 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I’m well aware of all that. The point is that all of that is only true if you take ZFC (or a similiar material set theory) as your basic system. The contortions that those structuralists have to go through to define “a structure” by abstracting away all the irrelevant information contained in any particular instance are only necessary because the instances are defined in ZFC. If we instead define $\mathbb{N}$ in type theory, then its elements have no irrelevant information (e.g. we can’t even ask whether $1\in 2$ ) and no extra step of abstraction is necessary. Univalence completes the picture by ensuring that any two isomorphic structured-types are actually equal, so it can never happen that $A\cong B$ but $A\neq B$ .

Posted by: Mike Shulman on April 22, 2015 6:27 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, “The point is that all of that is only true if you take ZFC (or a similiar material set theory) as your basic system.”

This is what we disagree about. I see it as having nothing to do with $ZFC$ . If I am interested in, say, a graph $G = (V,E)$ , it doesn’t matter if the elements of $V$ are sets or not. They might be natural numbers, real numbers, or anything really, eggs, say. So, I can’t see the connection with $ZFC$ , which is really just a system of 10 or so axioms, in a language $L_{\in}$ , which doesn’t even contain the terms “ $0$ ”, “ $1$ ”, etc.

But there’s a separate thing too: whether the notion of object-identity, $X = Y$ , for $X,Y \in Obj_{\mathcal{C}}$ , can or can’t be treated as a primitive notion. I’m not 100% clear yet how this is directly connected, but I think it’s connected to how you think of what “structural” means: for you, it means something like “treating indiscernible things as identical”, whereas for me it means “what isomorphic patterns have in common”.

Posted by: Jeffrey Ketland on April 22, 2015 6:59 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Is an isomorphism of graphs for you an elementary equivalence between them as models of the first-order theory of graphs?

Posted by: Dimitris on April 22, 2015 8:14 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Dimitris, “Is an isomorphism of graphs for you an elementary equivalence between them as models of the first-order theory of graphs?”

No, elementary equivalence does not imply isomorphism - this is the point I mentioned before. An isomorphism $f : A \to B$ is a bijection between the carrier sets of $A,B$ that preserves structure. In the case of graphs, let $G_1 = (V_1, E_2)$ and $G_2 = (V_2,E_2)$ . Then an isomorphism $f : G_1 \to G_2$ is a bijection $f : V_1 \to V_2$ such that for all $x,y \in V_1$ , $\{x,y\} \in E_1 \Leftrightarrow \{f(x),f(y)\} \in E_2$ .

For finite structures, $A \equiv B$ implies $A \cong B$ . But for infinite structures, $A \equiv B$ does not imply $A \cong B$ . For example, the real number field $(\mathbb{R},0,1,+,\times)$ has a countable elementary equivalent submodel.

Posted by: Jeffrey Ketland on April 22, 2015 9:52 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

[E]lementary equivalence does not imply isomorphism

This statement only makes sense if you’ve fixed your semantics, i.e. your background theory/foundation. That’s the point my question was meant to bring out.

As I said above, it seems to me that your notion of the structure of a mathematical object is defined in terms of a particular choice of foundation (not necessarily ZFC but something close enough to it, i.e. a material set theory.) The others (I don’t speak for them, but that’s how I interpret them) take their notion of the structure of a mathematical object to be given (mainly) by mathematical practice and by how mathematicians use these objects and then speak of foundations that do justice to this particular notion of structure. UF is such a foundation.

The debate at its core seems to me about whether “the structure of A” should be understood in terms of a particular foundation or whether it should serve as input in the design of a particular foundation. Structuralists in the philosophy of mathematics tend to take the first approach. UF takes the second approach. This is why, as David argues, it is not really meaningful to speak of the “structure of A” inside UF since UF has been designed in order to incorporate a particular view of the structure of mathematical objects.

Posted by: Dimitris on April 23, 2015 4:37 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Dimitris, the point that $A \equiv B$ doesn’t imply $A \cong B$ is a standard result in mathematics.

Posted by: Jeffrey Ketland on April 23, 2015 10:47 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Dimitris, there are lots of “foundational theories” - i.e., some system $F$ of axioms/rules in a precisely formalized notation $L$ , into which ordinary mathematical results from core mathematics can be interpreted and proved: e.g., $I \Delta_0, S^1_2, PRA, I \Sigma_1, RCA_0, PA, ACA_0, \Pi^1_1-CA, STT, HA, PA_{\omega}$ $Z, ZF, ZFC, ZFC + large cardinals, CZF, MLTT, ETCS, \dots$ .

Then there are questions about how to interpret/translate various things and their proof-theoretic strength, and so on. (For a nice example, $PA$ and $ZF - Inf + \neg Inf$ are bi-interpretable. Another is that $I \Sigma_1$ conservatively extends $PRA$ .)

It’s possible $UF$ and $ZFC$ are intertranslatable, maybe that’s the end of the matter, aside from questions of simplicity, usefulness and conceptual clarity.

Posted by: Jeffrey Ketland on April 24, 2015 9:19 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I agree with all this but none of this is in any way related to anything I said. We are obviously not communicating at all here, so let’s just agree to leave it at that.

Posted by: Dimitris on April 24, 2015 5:16 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

The discussion of things like $\{\emptyset\}$ is what only makes sense in ZFC. You’re right that the notion of structure is not dependent on ZFC. But the idea that structure must always be about isomorphism is closely connected to having some kind of set theory as a place to model first-order structures. I think the central point of disagreement is that you’re insisting that structure is always about isomorphism, whereas we’re saying that category-theoretic structure is about equivalence instead.

Posted by: Mike Shulman on April 22, 2015 8:27 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Mike, the notion of isomorphism between patterns is a very intuitive. It’s just the idea of one pattern “matching” another. I don’t think one needs to model any of this in set theory, or ZFC in particular. You need some bunch $A$ of “things” linked together by “relations” and some bunch $B$ of “things” linked together by “relations” and a way of matching them up.

Between 1870s and 1900, Dedekind, Frege, Cantor and Hilbert were all doing this before Zermelo wrote out axioms for $Z$ in 1908. Famously, Dedekind showed that all systems satisfying certain conditions were isomorphic - to $(\mathbb{N},0,S)$ , but this was 20 years before anything like set theory appeared on the scene.

Posted by: Jeffrey Ketland on April 22, 2015 10:03 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

The intuitiveness of isomorphism doesn’t imply that it is always what structure is about. Frequently in mathematics we start from something intuitive and then learn that sometimes it has to be generalized to something that initially seems less intuitive, but which comes to be equally intuitive with experience.

Posted by: Mike Shulman on April 23, 2015 12:51 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I agree one might in principle be convinced to drop isomorphism and replace it with equivalence, as the relevant criterion of structure, but I don’t think in the end that it’s really connected to ZFC as such, or ZFC vs ETCS, etc. I think, but I’m not sure, that the central distinguishing mark in the HoTT vs “opponents” debate is about type-theoretic vs non-type-theoretic understandings of identity and membership.

Global identity ( $x = y$ ) and global membership ( $x \in y$ ),

vs,

Type-restricted identity ( $Id_A(x,y)$ ) and type-theoretic “membership” ( $a : A$ ).

Posted by: Jeffrey Ketland on April 23, 2015 1:50 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Well, I’m not exactly sure who you’re referring to by “opponents”, and whoever they are, I wouldn’t presume to characterize all of their points of view under a single heading. But global equality and membership is indeed a difference between type theory and some other theories (although ETCS, for instance, is on the side of type theory here with only local equality and membership). I’m sorry that I apparently gave you the impression that I was saying it’s only about ZFC; that was never my intent. I was just using ZFC as an example of another theory to compare to.

Posted by: Mike Shulman on April 23, 2015 7:10 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Yes, all fair enough. But still, the view remains unclear - particularly, what is really meant in saying something like $A = B \Leftrightarrow A \cong B$ . The usual structuralist argument, from Benacerraf 1965 onwards, points out that we have $A \cong B$ and $A \neq B$ (e.g., von Neumann numbers vs Zermelo numbers), and then says there is something they have in common, $Str(A)$ , say, such that $Str(A) = Str(B) \Leftrightarrow A \cong B$ .

(The type-theoretic view is simply that $1 \in 2$ is meaningless, violating syntax-requirements. Whereas one might just say that $1 \in 2$ is merely false, since $1$ is not an element of $2$ . After all, $2$ is not a set!)

Posted by: Jeffrey Ketland on April 23, 2015 11:02 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Well, it’s perfectly clear to me what is meant. (-:

Posted by: Mike Shulman on April 24, 2015 12:08 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Hannes Leitgeb has an axiomatic theory, “axiomatic theory of abstract graphs” ( $ATAG$ ), with

$ATAG \vdash G_1 = G_2 \leftrightarrow G_1 \cong G_2$ .

Hannes and I discussed it a bit, and I do get how that theory works. Hannes has

“ $G$ is an abstract graph”,
“ $v$ is a vertex in $G$ ”,
“ $v$ and $u$ are related by an edge in $G$ ”

as primitive notions and the axioms for abstract graphs resemble those of $ZF$ , building up graphs by certain operations of adding vertices/nodes. But I don’t think he published it yet. I think the theory might face a problem (a permutation objection); but maybe wait and see til it appears in print.

Posted by: Jeffrey Ketland on April 24, 2015 1:48 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Are you saying that you don’t understand how univalence works?

Posted by: Mike Shulman on April 24, 2015 4:00 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

There’s some truth in that, yes. But what is probably better to say is: $Id_U(A,B)$ works here as a notion of indiscernibility, rather than identity; so formulations saying that $A \cong B \Rightarrow A = B$ are maybe misleading.

You mentioned the “hole argument” above; here’s an application of univalence (simplified) and tell me if you think it works. We have some spacetime model $(M,g)$ and a diffeomorphism $\phi : M \to M$ . Let’s assume this is not an isometry. So there is a point $p \in M$ , with $g(p) \neq (\phi_{\ast}g)(p)$ ). Let $g^{\prime} = \phi_{\ast}g$ . So, $g^{\prime} \neq g$ . By construction, $(M,g) \cong (M,g^{\prime})$ . But since $g^{\prime} \neq g$ , it follows that $(M,g) \neq (M,g^{\prime})$ . These spacetime models therefore seem to represent different physical worlds … despite the fact that they are physically indistinguishable.

Applying univalence - as before, consider $(M,g)$ , a diffeomorphism $\phi : M \to M$ , with $\phi$ not an isometry. Again, $g^{\prime} \neq g$ and $(M,g) \cong (M,g^{\prime})$ . But by univalence,

$(M,g) = (M,g^{\prime})$ .

So, we have the same physical worlds being represented after all. I.e., the reasoning from the fact that $g^{\prime} \neq g$ to the distinctness of the models is mistaken reasoning, about the mathematics of structures. And the hole problem is solved, after all!

Posted by: Jeffrey Ketland on April 24, 2015 4:14 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

That’s exactly right! Doesn’t that make univalence seem necessary?

Posted by: Mike Shulman on April 26, 2015 5:45 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

No, but at least it focuses sharply on the conceptual issue: viz., identity/individuation of structures. We have a manifold $M$ , and metrics $g,g'$ , and diffeomorphism $\phi : M \to M$ , with

(1) $g \neq g'$ (pointwise)

(2) $(M,g) \overset{\phi}\cong (M,g')$ .

I then do want to conclude, from (1),

(3) $(M,g) \neq (M,g')$ .

But Univalence, gives us, from (2),

(4) $(M,g) = (M,g')$ .

So we may resolve the “hole argument” if we accept Univalence.

The principle I use to get from (1) to (3) is roughly this: let $A$ be a set, and $(A, \leq), (A,\preceq)$ expansions with orderings $\leq, \preceq$ , then

(5) $(A,\leq) = (A,\preceq) \rightarrow \leq = \preceq$

More generally, if $A$ is a structure, and $(A,R), (A,S)$ are expansions with relations $R,S$ , then

(6) $(A,R) = (A,S) \rightarrow R = S$

E.g., if $R \neq S$ , then $(A,R) \neq (A,S)$ , even if $(A,R) \overset{\phi}\cong (A,S)$ .

So, what the justification for (6)? This states a criterion for how structures are “individuated” (in Quine’s terminology). Well, that’s just how I think of models/structures. They are bundles of a distinguished relations over some carrier set. To be identical, therefore, the carrier sets must be identical and the relations identical (the relations have to be “matched up” by a signature, but let’s omit this fussy detail).

Posted by: Jeffrey Ketland on April 26, 2015 8:35 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

I would have thought that resolving the hole argument would be a desirable thing.

Posted by: Mike Shulman on April 27, 2015 4:28 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Yes, definitely, and Univalence is one way - actually, I do think I can resolve it my own way, by defining a physical world to have the form $w = \langle \Psi_{(M,g)}\rangle[\overset{\to}R]$ (here $\overset{\to}R$ is a sequence of corresponding physical relations). Then I can get: $(M,g) \cong (M, g') \rightarrow w = w'$ , as required. But I’m not satisfied with the Univalence solution, because of the “identity spookiness” that I keep whining about …

Posted by: Jeffrey Ketland on April 27, 2015 6:14 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

As a sample in the wild, Woodin writes

The structure of the projective sets is of fundamental mathematical interest since it is simply the structure of the standard model of Second Order Number Theory:

$\langle \mathcal{P}(\mathbb{N}),\mathbb{N},+,\cdot,\in\rangle$

Posted by: David Roberts on April 20, 2015 5:41 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Here’s a question: if $\mathcal{S}$ is a kind of structure, what happens if $\mathcal{S}$ has nontrivial automorphisms?

It seems as though if $p: \mathcal{S} = \mathcal{S}'$ and $X: \mathcal{S}$ and $Y: \mathcal{S}'$ , and $q: p_*(X) = Y$ , then we ought to say that $X$ and $Y$ have the same structure by virtue of $q$ . One nice consequence of this is that it doesn’t matter how we present our kinds of structures. I could present the theory of Boolean algebra using $\vee,\wedge$ , and $\neg\,$ , or I could present it using Sheffer strokes. By virtue of the isomorphism between the types of boolean algebras under these interpretations, I can still compare boolean algebras presented differently and ask if they have the same structure.

But for example, take $\mathcal{S} = \mathcal{S}'$ to be the type of directed graphs, and take $p$ to be the automorphism which sends a graph to its opposite graph (where the edges are all reversed). Then the question is: does a graph have the same structure as its opposite graph?

Actually, I kind of like the idea that the answer should be yes! But maybe this is a good point to just recognize that there are many different notions of “structure”, and stop trying to get just one of them. Also, there’s a question whether the appropriate identities between kinds of structures are just identities of types, or whether more is required. For example, if $A$ and $B$ are Morita-equivalent rings, is an $A$ -module structure the same as a $B$ -module structure? This gets back to the question of whether $kindofstructure = Type$ , or if it’s more complicated than that.

By the way, notice that now I’m talking about a relation “have the same structure”. This is either

$\mathcal{S}: kindofstructure, X,Y: \mathcal{S} \vdash samestructure_\mathcal{S} (X,Y) \equiv X=_\mathcal{S} Y$

or maybe something like

$\mathcal{S},\mathcal{S}': kindofstructure, X: \mathcal{S}, Y: \mathcal{S}'$

$\vdash samestructure_ (X,Y) \equiv\sum_{p: \mathcal{S}=_{kindofstructure}\,\,\mathcal{S}'} p_*(X) =_{\mathcal{S}'} Y$

Either way, we can still derive David’s contractible type $Str$ as

$Str(X) \equiv \sum_{Y} samestructure(X,Y)$ .

Posted by: Tim Campion on April 26, 2015 4:15 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

does a graph have the same structure as its opposite graph?

Yes… but to be correct you should also indicate that this is a “sameness” relative to the “opposite” automorphism of the theory of graphs. In HoTT/UF we sometimes call these “dependent equalities” or “heterogeneous equalities”, and you have to keep track of the equality “downstairs” that they depend on. Similarly, for instance, you could say that $\{\emptyset, \{\emptyset\}\}$ and $\{\{\emptyset\}\}$ are the same natural number, but only relative to the standard isomorphism between the von Neumann and Zermelo definitions of natural number.

Posted by: Mike Shulman on April 26, 2015 5:51 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Tim,

what happens if 𝒮 has nontrivial automorphisms?

Something like this question actually did arise as an objection to (Shapiro-Resnik-style) structuralism around 1999/2001, with argument by John Burgess (1999 review of Shapiro’s 1997 book on structuralism) and Jukka Keranen (“The Identity Problem for Realist Structuralism”), noting that conjugation in $\mathbb{C}$ seems to contradict structuralist assumptions, because, e.g., $i$ and $-i$ are “structurally the same place” and yet distinct - and so, what constitutes their difference? It must be “non-structural”. So, structuralism is wrong.

Posted by: Jeffrey Ketland on April 26, 2015 7:35 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Sorry, I left some ambiguity there. My question was about what happens when the kind of structure has an automorphism, not when a particular [example of a] structure has an automorphism. So in my example, the kind of structure is the directed graph kind of structure; there is an automorphism $\alpha$ of the category of graphs, which sends each graph to its opposite graph. A graph need not be isomorphic to its opposite, and yet a graph and its opposite have the same structure “relative to $\alpha$ ” – you have to specify the automorphism as part of the data.

In your example, $\mathbb{C}$ is a structure (of the kind field-extensions-of- $\mathbb{R}$ , say) which has a nontrivial automorphism. The issue with how to think about places in a structure with automorphisms seems to be solvable in a similar way, though – by keeping the equivalence between two structures as part of the data of what makes them the same structure.

Posted by: Tim Campion on April 27, 2015 3:57 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Yes, my bad (I got the level wrong). In that mini-literature started by Burgess/Keranen, the problem was for the structuralist (Shapiro et al) to explain why $i \neq -i$ , given that $z \mapsto z^{\ast}$ is an automorphism of $\mathbb{C}$ (e.g., $i$ and $-i$ seem to be “structurally indiscernible” - so why aren’t they identical?). One answer to the problem is simply to say that $=$ is a primitive logical notion available to structuralists - after all, it is needed to define what an algebraic structure is: i.e., $A$ is a field iff $A \models 0 \neq 1 \wedge \forall x,y(x + y = y + x) \wedge \dots$ . Here we must use $=$ as a logical primitive in order to ensure that $A$ is a field. The point of the objection was: how does the structuralist explain why $i \neq -i$ . It’s not clear why keeping track of $z \mapsto z^{\ast}$ being an automorphism helps to explain why $i \neq -i$ …?

I’m not sure of this - but I think, on your “kind of structure” question, the corresponding question seems to be: $\alpha$ is an automorphism of the category, so why do we have some $G$ with $\neg(\alpha(G) \cong G)$ ? But this seems ok, since the notion $X \cong Y$ is perfectly legitimate for structuralists.

Posted by: Jeffrey Ketland on April 27, 2015 6:48 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Keeping track of the conjugation automorphism does solve the problem. The point is that “ $i=-i$ ” is a dependent equality “over” or “along” conjugation, which is different than an “ordinary” equality (which you might say lives “over” the identity map).

Posted by: Mike Shulman on April 27, 2015 10:17 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

The indiscernibility notion here is defined in papers I wrote which appeared in 2006 (on structuralism) and 2011 (on identity and indiscernibility). That is, $i$ is structurally indiscernible from $-i$ in (the field) $\mathbb{C}$ because there is an $\pi \in Aut(\mathbb{C})$ such that $-i = \pi(i)$ . More generally, given a structure $A$ ,

Elements $a,b$ are structurally indiscernible in $A$ (relative to $\pi$ ) iff $\pi \in Aut(A)$ .

However, the fact that $a,b$ are structurally indiscernible in $A$ does not imply $a = b$ . So this does not explain why $i \neq -i$ . To explain that, you must take $=$ to be a primitive notion in the language of fields (i.e., undefined). There is a variety of other indiscernibility notions that one can define, and one can study their properties, and prove results about them. But one can sometimes prove that identity cannot be defined using that indiscernibility notion, or in the relevant structure. I.e., the question is

when can $=$ be defined in $A$ ?

And various answers can be given (e.g., if a strict linear order $\lt$ is definable in $A$ , then $x = y$ can be defined by $\neg(x \lt y) \wedge \neg(y \lt x)$ ).

I’d agree with Zhen’s point earlier that,

homotopy type theory is the study of equality

if it were replaced with

homotopy type theory is the study of indiscernibility relations.

And add that the outlook of someone critical of HoTT is probably that indiscernibility is not the same as identity. If $A$ and $B$ are indiscernible in some way - perhaps by both satisfying some class of properties, or perhaps by there being a nice kind of mapping between $A,B$ (e.g., isomorphism, equivalence) - it does not follow that they’re identical. The identity of $A$ and $B$ consists in their being exactly the same thing, so there is exactly one, not two.

Posted by: Jeffrey Ketland on April 28, 2015 10:50 AM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

The statement

Elements a,b are structurally indiscernible in A (relative to π) iff π∈Aut(A)

has what I can only assume is a typo: if this were correct, then any two elements of A would be structurally indiscernable relative to the identity, which is absurd. The correct statement is

Elements a,b are structurally indiscernible in A (relative to π) iff π∈Aut(A) and $\pi(a)=b$ .

I don’t think anyone is claiming that equality has to be defined. Equality is a primitive notion in intensional type theory just as it is in more familiar theories, although the rules governing how to reason about it are somewhat different.

But note that a = b iff a and b are structurally indiscernable relative to the identity. So a = b iff a and b are structurally indiscernable relative to $\pi$ and $\pi$ is equal to the identity.

If I might express my own proto-view, I think that in HoTT, the primitive objects are structures, and it turns out that structures in general don’t admit a classical notion of equality (as evidenced by arguments like those of Burgess and Keranen), but they do admit an intensional notion of equality, which happens to satisfy the univalence axiom (in fact I tend to think of univalence as stating that we are talking about structures – things which are the same if they are equivalent – in the same way that the axiom of extensionality in ZFC says that we are talking about (material) sets). I think the principle feature of intensional equality is that two things can be equal in more than one way, and you have to keep track of those ways.

Maybe it would be helpful in this debate about the nature of equality to be clear about which objections apply to univalence specifically, and which objections apply to intensional equality more generally.

Posted by: Tim Campion on April 28, 2015 4:35 PM | Permalink | Reply to this

Re: The Structure of A

$MathML-enabled post (click for more details).$

Tim, yes, thanks - that’s a typo! Thanks for the correction.

On the conceptual point – which is trying to clarify what is “revolutionary” (in Steve Awodey’s terms) in HoTT and Univalence – may be something like intensional identity, as you say. But is this a relation of objects (entities, structures, …), or a relation of how objects are “presented”?

Frege famously wondered (1892, “On Sense and Reference”) how

Morning star = Evening star

could be informative if there’s just one thing involved (i.e., the referent of “Morning star” is the very same thing as the referent of “Evening star”). Frege’s solution is that the intensions of the expressions “Morning star” and “Evening star” are different, even though their referents are the same. He called these Sinne–senses. He likened them to “modes of presentation”. Later, Russell (1905) more or less identified “modes of presentation” with descriptions (“the unique object $x$ such that $F(x)$ holds”), and said that to understand a name $n$ (e.g., “Sir Walter Scott”), you must associate it with a description $D_n$ (e.g., “the person who wrote Waverly”). Then Kripke (1972, 1980) objected to this, but it’s a long convoluted story. Roughly, Kripke pointed out that Sir Walter Scott might not have written Waverley; but, under these possible circumstances, “Sir Walter Sott” still refers to Walter Scott, and not anyone else, whereas “the author of Waverly” refers to anyone who, in those circumstances, did write Waverley. Kripke says that names are (modally) rigid, whereas descriptions aren’t.

I’m not sure if intensionality is the prime ingredient. Maybe so. Frege knew concepts could be intensionally distinct, but extensionally the same, and even tried to write down an axiom for this, Basic Law V,

$ext(C) = ext(C') \leftrightarrow \forall x(C(x) \leftrightarrow C'(x))$

But this turned out to be inconsistent, as Russell discovered.

It’s worth writing out the proof, because it’s not connected to set theory at all. It takes places entirely in second-order logic. Let $R(x)$ be $\exists C(x = ext(C) \wedge \neg C(x))$ . Let $r : = ext(R)$ . Then assume $R(r)$ . So, $\exists C(r = ext(C) \wedge \neg C(r))$ . So, $r = ext(C)$ and $\neg C(r)$ . So, $ext(C) = ext(R)$ . So, by Basic Law V, $\forall x(C(x) \leftrightarrow R(x))$ . So, $C(r) \leftrightarrow R(r)$ . So, $\neg R(r)$ . Contradiction. So, assume $\neg R(r)$ . Then $\forall C(r = ext(C) \to C(r))$ . So, $r = ext(R) \to R(r)$ . So, $R(r)$ . Contradiction.

Maybe the issue that makes Univalence revolutionary is about intensionality. I’m not sure. I think HoTT/UF replaces strict identity claims with indiscernibility claims, along with a type-theoretic view that identity is “localized”, and so “ $A$ is strictly identical to $B$ ” doesn’t make proper sense (it’s a syntax error). If that’s about right, then HoTT/UF isn’t so much the study of equality/identity (at least as classically understood), but is rather the study of indiscernibility (while adding that classical identity has to be revised or dropped).

Posted by: Jeffrey Ketland on April 28, 2015 6:34 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

April 12, 2015