added section on the axiom of extensionality in two-sorted set theories

Anonymous

]]>Added 2 additional definitions of set in fully formal ETCS

Anonymous

]]>Clarifying parentheses in the definitions of $\mathrm{set}(a)$ and $\mathrm{element}(a)$.

]]>Fixed spelling error

Anonymous

]]>The converse always holds because of the indiscernability of identicals

Anonymous

]]>adding some references to the page

Michael Shulman,

*Comparing material and structural set theories*(arXiv:1808.05204)Håkon Robbestad Gylterud, Elisabeth Bonnevier,

*Non-wellfounded sets in HoTT*(arXiv:2001.06696)

Anonymous

]]>When postulating weak and not the conventional extensionality, how far does epsilon-induction (instead of regularity/foundation) take you in defining equality?

]]>added statement of axiom of extensionality without the axiom of foundation.

Anonymous

]]>adding link to product extensionality

Anonymous

]]>Adding links to function extensionality and univalence

Anonymous

]]>I do not quite understand the discussion under the axiom of extensionality. It says that one can do two variants (of course), one is that equality is taken as a primitive (predicate) and another that the axiom is taken as a definition of equality. Of course, this is in the idea so, but then the second version of the axiom is written unclear (and it is not quite a definition) and the discussion is also unclear. I see it this way: there is a propositional calculus and there is a propositional calculus with equality. “The same” is probably here just an informal way to refer to *the* equality of the propositional calculus with equality, that means a distinguished binary predicate which satisfies substitution axiom, transitivity, reflexivity and symmetry. In that calculus we just state the axiom (not a definition) that the equality can be rephrased via belongness relation. If we work in just a propositional calculus then we can define a relation which we may call equality but we can also call it blablabla. Then we have to state explicitly which properties, possibly weaker than required in the propositional calculus with equality hold for that relation (I am not quite sure how entry extensional relation solves this, in particular, should we now prove the substitution axiom for equality). Now, one should do that version precisely. In calculus with equality there is no space for two versions as far as I see: equality is given (distinguished) by the propositional calculus with equality, we can only characterize it.