I rolled back the last edit; as Matt said, it was correct before with “provably distinguishes”.

]]>I think it’s reasonable to interpret “indiscernible” in a positive way in a constructive context, just as the reasonable constructive interpretation of “nonempty” is “inhabited”.

]]>Arvid, but you still can’t prove $\not P(N2)$. That is, P doesn’t discern N1 and N2. So N1 and N2 are no longer identical, but they’re still indiscernible. Removing axioms never makes things discernible.

Although it’s probably way too late, I think the original discussion missed an important point: Equivalence is a positive, constructive statement, while indiscernibility is negative. If anything, univalence is “identity of interchangeables”, which seems intuitively weaker than identity of indiscernibles. Also, type theory’s identity elimination rule seems like interchangeability of identicals, which is intuitively stronger than indiscernibility of identicals.

]]>Without Univalence, such predicates are of course definable: Define two types of natural numbers, say, N1 and N2, and let the predicate be $P = \lambda x. x = N1$.

Arvid Marx

]]>Identity of indiscernibles in higher-order category theory means equivalence of objects that are discernible only by evil means.

]]>It seems to me that the issue of whether there is a sense in which differently-presented instances of the same structure are "actually" distinct and the issue of evil properties "outside of math" are of a similar species since both involve bringing in an ontological notion of identity. ]]>

Right, so one side says “I can choose a ball and say that it has the property of being in the place it occupies, while the other ball doesn’t occupy that place. Properties differ.” The other side worries that in effect, you’ve placed yourself in the universe as observer, or at least introduced something extraneous to the universe itself.

And yes, mathematics, of course, is able to cope with entities with autoequivalences permuting non-identical subparts.

]]>Unless position is not considered to be a property, I don’t see any reason for the two spheres to be indiscernible. This is the same argument that shows that a set can have many different one-element subsets.

]]>That was rather loose on my part. I was thinking about an applied type theory where two entities are given as the interpretations of two equivalent terms.

Metaphysicians often think up simple universes to test out their intuitions. For example,they imagine two physically identical spherical objects as the sole occupants of a space. Leaving aside the matter of whether this is physically possible, the worry is that no properties distinguish the objects and yet we don’t want to think of them as identical.

]]>I’m not sure what “equivalence” means outside of mathematics.

]]>So one question is, outside of mathematics, what would lead one to employ properties which are not invariant under equivalence. It would be important to remember that just as it is right to distinguish non-identical isomorphic subgroups of a group, so one should distinguish ’isomorphic’ subregions of the universe.

]]>The way I think about it, in type theory, identity of indiscernibles is just true, essentially by definition of “identity” – that’s the induction principle for identity types. Possibly the issue is rather that the notion of “indiscernibility” refers to a notion of “property”, and the question is what sort of properties we consider. In mathematics, we generally only consider properties that are invariant under equivalence; thus equivalent objects are indiscernible, and hence identical.

]]>Hi all, I added an entry for Leibniz’s identity of indiscernibles.

I thought it would be nice to include a discussion of the way in which univalence refines the identity of indiscernibles, but I am just beginning to learn about UF and was not sure what to say.

In Awodey’s 2013 exposition of univalence he states:

“Rather than viewing it as identifying equivalent objects, and thus collapsing distinct objects, it is more useful to regard it as expanding the notion of identity to that of equivalence. For mathematical purposes, this is the sharpest notion of identity available; the question whether two equivalent mathematical objects are “really” identical in some stronger, non-logical sense, is thus outside of mathematics.”

Thus we can regard univalence as “loosening” the notion of identity in such a way that it validates Leibniz’s law.

Certainly, I can just add something like this. However, it seems to me that a philosophical notion of equality that accords with intuition may profitably make a distinction between isomorphic structures when they are not “really” equal ontologically. Awodey is making a stance about “mathematical” rather than “real” identity, as is considered in (some formulations?) of Leibniz’s Law.

Is it possible to think about the connection to Leibniz’s Law like this:

Equivalence is akin to and entails a kind of “observational equivalence”/indiscernibility.

Thus we have the following putative principles:

- Indiscernibility of Identicals–intuitively true
- Identity of indiscernibles–controversial
- Indiscernibility is indiscernible from identity–intuitively true, and maintains some of the intent of identity of indiscernibles

So can we think of Univalence as a refinement that says “Indiscernibility is indiscernible from identity, so we may as well treat indiscernibles as equal by transporting isomorphisms into identifications.”? Or is this not the way to think about this/do folks in UF have a stronger stance such as “real” equality being absurd?

Best, Colin

]]>