# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

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

• CommentRowNumber1.
• CommentAuthorDavidRoberts
• CommentTimeJun 20th 2016

I added to principle of equivalence the following quote:

Either a thing has properties that nothing else has, in which case we can immediately use a description to distinguish it from the others and refer to it; or, on the other hand, there are several things that have the whole set of their properties in common, in which case it is quite impossible to indicate one of them. For if there is nothing to distinguish a thing, I cannot distinguish it, since otherwise it would be distinguished after all. (Tractatus §2.02331)

and a suggestive comment after it about considering such a statement for any given language, rather than the global setting stated in §1 (’the world’).

In the language given by the internal logic of a category one can never distinguish objects that share all their properties! My thesis is that ideas such as the internal language of a category and the Yoneda lemma have precursors in Tractatus, but I’ve not had time to sit down and nut out the details. Others have written about identifying the logic of the Tractatus (eg Potter’s The logic of the Tractatus, Weiss’ Logic in the Tractatus I: Definability, but I haven’t done a thorough search). I haven’t added these comments to the nLab anywhere, but I hope to do so when I flesh out my arguments.

In the process, I added to Tractatus Logico-Philosophicus some online sources for the text.

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeJun 20th 2016

There’s been a lot of discussion over the years about a scenario pondered by Black (1952) where we have a space empty except for two identical spheres. How many spheres are there?

If there are no distinguishing features, how can we distinguish them? Intuitively you would like to say that it would be possible to look at one and call it $A$, and then what distinguishes the one you look at from the other is that it’s identical to $A$ while the other isn’t. Opponents have considered this a dubious property, since the other one is identical to itself too, and they think this implicit labelling is unjustified. So as to how many spheres there are, answers range from 2 to 1 to 0.

How about the HoTT answer(s)? For $S$ the type of spheres, in the context $\mathbf{B} Aut(S)$, the cardinality of $S$ is 2, even if a single sphere can’t be designated in that context. Dependent sum along $\mathbf{B} Aut(S) \to \ast$ has cardinality 1, reflecting that there’s one kind of sphere; dependent product has cardinality 0, reflecting that neither can be specified.

Everybody is right!

• CommentRowNumber3.
• CommentAuthorDavidRoberts
• CommentTimeJun 20th 2016

@David - nice! I’d be curious as to the pre-HoTT argument for why there are 0 spheres.

Having two identical spheres makes me think of the comment that Gershom B made on my G+ post about atomic facts being either there or not, without affecting other such facts. But perhaps this is a superficial reading, and is orthogonal to your point.

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeJun 20th 2016

Well maybe nobody has actually said 0, but it makes for a good story. Than again, it wouldn’t surprise me.