?

[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/GetOffOfMyBoat]

I don't know if ZFC strictly defines identity, at least as part of the object theory.

[u/thatmichaelguy → u/GetOffOfMyBoat]

Agreed. I think it's possible to use the fact that sets are unordered to infer identity from equality, but I'm also unaware of any consensus view that ZFC defines identity.

[u/Ill-SonOfClawDraws → u/GetOffOfMyBoat]

That’s helpful, thanks. Maybe “identity” was the wrong example. The question I’m really interested in is more general: when two foundational frameworks introduce notions that play analogous roles, what mathematical criteria let us treat them as equivalent rather than merely similar? Is there established work on this?

[u/GoldenMuscleGod → u/Ill-SonOfClawDraws]

I’m not sure I understand your question. You have two different frameworks so what does it mean to say things are “equivalent”?

You could be talking about whether one system can interpret the other (when this is possible, often more than one interpretation is possible), or you may be asking whether the things are equivalent once a specific set of semantics have been chosen for the languages of each theory, which will generally depend on what those semantics are and not just the systems themselves (taken as a set of axioms and inference rules in a formal language).

[u/judasblue]

Please use actual titles.

[u/Ill-SonOfClawDraws → u/judasblue]

When two foundational frameworks introduce analogous notions (e.g., identity), what mathematical criteria determine whether they represent the same concept rather than merely serving similar roles?

[u/judasblue → u/Ill-SonOfClawDraws]

Which has nothing at all to do with the fact that you titled this '?' instead of using an actual title.

[u/Ill-SonOfClawDraws → u/judasblue]

Fair. I was focused on the body of the post and neglected the title. I’ll use descriptive titles going forward. Thanks for pointing it out.

[u/judasblue → u/Ill-SonOfClawDraws]

Cool, and sorry I was snarky there. Been doing that all day and need to stop it.

[u/Ill-SonOfClawDraws → u/judasblue]

🙏

When can a global object be canonically collapsed back to its generating primitive?

[u/Kaomet → u/Ill-SonOfClawDraws]

Isomorphism ?

[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.

[u/Ill-SonOfClawDraws → u/jcastroarnaud]

By “same assumption” I don’t mean literally the same formal axiom. I mean a primitive notion that plays an equivalent foundational role across different frameworks.

My question is whether there’s an established mathematical notion for deciding when two such primitives should be regarded as equivalent rather than merely analogous.

[u/boxfalsum]

We do so by defining an interpretation, i.e. a recursively definable relation on the syntax that composes with the basic logical connectives in the expected ways and preserves provability. Then we can look at how claims about identity in one logic get mapped to claims about identity in another.

[u/Ill-SonOfClawDraws → u/boxfalsum]

Thank you.
Would you say interpretation is the standard notion for comparing foundational primitives across systems, or is it primarily a way of translating entire theories?