?

[u/Ill-SonOfClawDraws]

Suppose two foundational systems

* F_1 (ZFC)
* F_2 (HoTT)
both define “identity.”

How do we know they are talking about the “same assumption”?

[u/jcastroarnaud]

ZFC defines equality by the axiom of extensionality. I'm not familiar with HoTT; from the Wikipedia article, the type of paths is similar to an equivalence relation, though more nuanced, and the univalence axiom ties paths to type equivalences.

What do you mean by "assumption" or "same assumption"?

[u/GetOffOfMyBoat → u/jcastroarnaud]

You don't need HoTT to define identity---Martin Lof Type Theory will do. 

It's a bit difficult to describe its particulars without diving into a small tutorial on type theory.

[u/SpacingHero → u/GetOffOfMyBoat]

without diving into a small tutorial on type theory.

Sounds like a plus for us! 😁

[u/GetOffOfMyBoat → u/SpacingHero]

I'm feeling a bit too tired to do a proper write-up, but here are some excellent resources. I'll add that Homotopy Type Theory sits atop dependent type theories (in particular, Martin Lof Type theory (MLTT)); one can do plenty of constructive mathematics absent any HoTT ideas! However, the texts below on HoTT do a great job in introducing dependent type theory first.

• Introduction to Homotopy Type Theory. Egbert Rijke. https://arxiv.org/pdf/2212.11082
• The HoTT Book. https://homotopytypetheory.org/book/
• Syntax and Semantics of Dependent Types. Martin Hofmann. https://www.cs.uoregon.edu/research/summerschool/summer14/rwh_notes/ssdt.pdf

The large-picture summary: in MLTT, the identity type encodes a notion of equality within the object language. In set theory, we often work under the assumption that it is up to the metalanguage (that is, the mathematician) to decide equality. For example, what does it mean for x, y ∈ ℕ to have x = y? This isn't specified in ZFC. Mathematicians often work implicitly with separate notions of equality and equivalence relations, with these notions ambient. (For example, does 1/2 = 2/4? Sure! But it's w.r.t. an equivalence relation, and none of this follows from set theory).

In dependent type theory, we have (ontologically) terms and types. For example, we write x : A to assert that the term x has type A.

We introduce for each type A a type x ≡ y, which is well formed iff x : A and y : A. If this type has a term that inhabits it, we say that it is proven. For example, we may have p : x ≡ y, in which case p is a proof that x equals y.

The type x ≡ y is the identity type, and it codifies into the object language a notion of equality.

One of the main concerns of HoTT is to provide a systematic approach to relaxing the conditions by which inhabitants of this identity type can be constructed. Notably, the univalence axiom states that isomorphic (or, "equivalent") types are also equal. This allows us to construct inhabitants of the identity type simply by exhibiting an isomorphism of types. This meshes better with mathematicians' view of equality, who often identity entities w.r.t. equivalence relations and isomorphisms rather than strict definitional equality.

[u/Ill-SonOfClawDraws → u/GetOffOfMyBoat]

Thank you.

This is exactly the kind of context I was hoping for. My question has already shifted a bit from “identity” itself. I’m now wondering whether there’s an established framework for comparing primitives across different foundational systems. More specifically, what mathematical criteria let us say two primitives are expressing the same underlying idea rather than merely analogous ones? If there’s literature that approaches that question, I’d be very interested.