Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Added reference at Favonia to his thesis, Higher-Dimensional Types in the Mechanization of Homotopy Theory.
There’s even a section ’Buddhism in Martin-Löf Type Theory’.
That looks fun.
The statement that he actually proves in that section with Buddhism in the title, that statement has an established name in logic, doesn’t it. I forget the technical term, but people here will readily know: It’s the statement that two things are equal precisely if there is no proposition distinguishing between them.
Leibniz equality.
principle of identity of indiscernibles — but I think the statement in the thesis has a distinct content, or is at least intended as such. Something like, if a concept is equivalent on its fibres over all objects then it ultimately has no content, is-non-dual
is a proposition about a concept, not two inhabitants of a type. According to the proof here, identification of any two objects “at an ultimate level” (induced by recognition of the interdependence of all things, the realization that a concept and its antithesis are in complete continuity, supposedly) is necessary and sufficient for demonstration of the “non-duality” or ultimate emptiness of a concept, which doesn’t seem too surprising.
This results really in a severe form of scepticism or quietism, intended to quell our philosophical anxieties. There is a literature on the relation between Pyrrhonian scepticism and Madhyamaka Buddhism, which are useful parallels (eg. Garfield 1990). Disastrous for many reasons, although there is no better stimulus to the formulation of alternatives: the presuppositionless structure of the Science of Logic is very much designed as the ultimate bulwark against Pyrrhonism (Trisokkas 2012).
Incidentally I see that (Ladyman & Presnell 2016) has an appendix formulating no fewer than 4 forms of the PII in HoTT. I will add this material to the PII page in due course.
Leibniz equality
and
Thanks! That’s it.
I have put a pointer to Favonia’s formalization there. (Though this probably was formalized elsewhere before?)
but I think the statement in the thesis has a distinct content, or is at least intended as such.
It may be intended differently, but clearly this is exactly what it says.
On another note, I am not convinced by the quote by John Baez on that page. It was added by Colin Zwanziger when the page was created in revision 1. I vote for removing this.
Strangely the HoTT book only has it in reverse (and misspelled). In Section 1.12 there is ’Indiscernability of identicals’.
I am not convinced by the quote by John Baez on that page.
Yes, not very helpful.
The HoTT book “has it in reverse” because it’s actually talking there about the reverse implication: the eliminator for the identity type is the indiscernibility of identicals. Identity of indiscernibles is the opposite. In the presence of an identity type, identity of indiscernibles is trivial because of haecceities; but extensionality principles like function extensionality, propositional extensionality, and univalence (“typal extensionality”) are indeed naturally regarded as a stronger form of identity of indiscernibles. In particular, the consistency of univalence means that in MLTT without univalence, one cannot define any predicate that provably distinguishes isomorphic types; thus isomorphic types are “externally indiscernible”, and univalence incarnates that principle internally by making them identical.
I didn’t write ’strangely’ because I thought you had the direction wrong, but because you only give an account of the far less frequent of the two ways.
Less frequent to the philosopher, perhaps, but I would say that to a mathematician that’s the more important direction.
I assumed that that phrase was chosen as something in the way of a play on words.
ETA: Here is somebody who thinks that Leibniz’s principle is properly understood as including both directions: http://www.oberlin.edu/faculty/mwallace/LeibnizsLaw.html.
Function extensionality, univalence, etc are forms of Leibniz’s principle, but applied after making a judgement about what predicates one is allowed to apply to a function, type, etc. Leibniz’s principle by itself, while still important, is also trivial when you have identity predicates, as Mike said. To get function extensionality (for example) as well, you first say that there are some basic predicates about functions that generate all of the predicates, so that if two functions have those predicates (which are the values of the function, or rather their haecceities^{1}) in common, then they have all predicates in common (and so, pace Leibniz, are equal).
I thank Mike for teaching me this word. For our purposes, the haecceity of $x$ is the predicate $- = x$. ↩
It doesn't seem to me that Appendix B of Favonia’s thesis actually contains a formulation of the identity of indiscernibles. The statement that they^{1} prove is not that two things are identical iff no properties distinguish them; it is that all things are identical iff no properties distinguish anything.
That is, they did not prove^{2}
$\forall\, o_1,\; \forall\, o_2,\; \bigl(o_1 = o_2 \;\leftrightarrow\; \forall\, P,\; P(o_1) \;\leftrightarrow\; P(o_2)\bigr) ;$rather, they proved
$(\forall\, o_1,\; \forall\, o_2,\; o_1 = o_2) \;\leftrightarrow\; \bigl(\forall\, o_1,\; \forall\, o_2,\; \forall\, P,\; P(o_1) \;\leftrightarrow\; P(o_2)\bigr) .$Of course, the second statement follows from the first, so there is that.
‘I prefer singular they but people often choose he because of my perceived gender.’ ―https://www.cs.cmu.edu/~kuenbanh/#pronoun ↩
That this was in HoTT rather than FOL didn’t seem to add anything, and Favonia even said that their statements omitted some truncations, so I just truncated everything here. ↩
Toby #12 that’s another good way to describe it. For function extensionality it is easy to say what predicates we are interested in, namely those that involve evaluating the function. But it’s less clear to me how to say what predicates we are interested in for univalence; what would you say?
The haeccity business comes into play in discussions emanating from Max Black’s discussion of a universe containing only two identical spheres. The debate considers whether one can say that there are two objects if there is no property which distinguishes one sphere from another. It hinges on whether you allow naming a ball, $a$, and then a predicate, $-=a$.
In my Structurepaper, I suggest that viewing the situation via an equivariant context $\mathbf{B} S_2$ is useful. In that context there are two things. In the empty context, the dependent product gives us nothing, and the dependent sum a singleton.
Thanks, Mike, that makes sense. I have added that to the entry here. And also to the Idea-section at univalence.
1 to 16 of 16