Why is `eq` more important than `heq`?

Stream: maths

[Antoine Labelle]

This question might be a little bit vague, but I hope it's ok.
I was trying to explain what type theory is to a non-math friend, and I started talking about how the proposition a = b is only meaningful if a and b have the same (i.e. definitionally equal) type. The person then asked why we can't just say that a = b is false rather than "meaningless" when a and b have different types, and I realized that I didn't really have any good answer. In fact, this is basically exactly what heq is doing (the contrapositive of docs#type_eq_of_heq says exactly that if a and b have different types, then it is false that a == b).
Hence my (perhaps naive) question is, why is eq the fundamental thing that we use everywhere and not heq? What can we do with eq that we can't do with heq that justifies this?

[Andrew Yang]

We cannot do substitution (or rewrite) using heq. a == b -> P a -> P b might not even type check.

[Antoine Labelle]

Isn't it what docs#heq.subst is doing?

[Eric Rodriguez]

note that that's an indexed family of propositions, as opposed to just a Prop

[Eric Rodriguez]

I think the answer is that it becomes type-theoretically annoying and you'll get motive errors far more often

[Eric Rodriguez]

but that's only due to the limitations of our systems... I think if you asked an Agda user, there's far different reasons and explanations

[Kyle Miller]

Antoine Labelle said:

the contrapositive of docs#type_eq_of_heq says exactly that if a and b have different types, then it is false that a == b

When you say the types are "the same" or "different" you have to be a bit careful since there's a difference between types being definitionally the same and types being eq. Lean doesn't say really anything about which types are or are not the same; in principle it could be the case that nat = int. At least types of different cardinalities can't possibly be eq...

[Kyle Miller]

In fact, there must be "different" types that are actually equal

[Antoine Labelle]

Interesting. I see indeed why heq.subst is very limited for rewriting.

[Patrick Johnson]

There is a trade-off between expressiveness and structuredness. Type theory imposes structure, hence expressiveness must suffer. In set theory, eq and heq are the same thing. Two sets are equal iff any unary predicate that holds for one of them also holds for the other.

[Patrick Massot]

I would say the opposite: type theory imposes structure, hence is more expressive.

[Patrick Johnson]

Being unable to properly express ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ, and being unable to substitute x with y given x = y due to type mismatch, is not what one may call expressive. But I agree that this may be quite subjective.

[Michael Stoll]

Whether ℕ ⊂ ℤ or not in set theory depends very much on how you construct the integers, and the standard way (take the quotient under an equivalence relation on pairs of natural numbers) definitely does not give you a superset. Rather, you "identify" the naturals with their canonical image in the integers, which is not much different from using the canonical injection (only that type theory forces you to make it explicit).

[Patrick Massot]

I don't know any construction of $\mathbb{Z}$ in set theory that would give an inclusion $\mathbb{N} \subset \mathbb{Z}$, and it gets much worse as you continue in your sequence of "inclusions".

[Jireh Loreaux]

Wouldn't a set-theoretic formalization force you to make it explicit too?

[Michael Stoll]

I assume you could redefine the natural numbers to be the set of nonnegative integers, once the integers are there. But then you'll have to do that each time (and transitively) you construct a "larger" structure...

[Jireh Loreaux]

That just means you can't really do it in practice.

[Kevin Buzzard]

You also can't do it because I can't simultaneously define the natural numbers to be all of the natural number subsets of the 2-adics, 3-adics, 5-adics,... and the reals.

[Patrick Johnson]

Related

[Michael Stoll]

Well, you could, but that would need an inordinate amount of plumbing.

[Mario Carneiro]

Patrick Massot said:

I don't know any construction of $\mathbb{Z}$ in set theory that would give an inclusion $\mathbb{N} \subset \mathbb{Z}$, and it gets much worse as you continue in your sequence of "inclusions".

The construction of $\mathbb{Z}$ used in Mizar is to do the usual construction with pairs of nats to get the negative integers, and then adjoin the actual set $\mathbb{N}$ (the first initial ordinal) because no ordinal is a pair. Yes this is a hack, but they manage to keep it up all the way through ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ.

[Michael Stoll]

How do they do p-adics?

[Mario Carneiro]

I'm not sure they do, but you can do a similar thing if you want ℚ to be included in it

[Mario Carneiro]

you can also simultaneously make it otherwise disjoint with ℂ

[Michael Stoll]

I guess you'll get quite ugly definitions by cases for addition etc. if you do this.

[Mario Carneiro]

sure, but once it's hidden behind an API it doesn't really matter

[Mario Carneiro]

indeed mizar has a fairly flexible system for "redefinitions" which allows you to make the equivalent of unfold foo use whatever theorem you want

[Mario Carneiro]

set theory is a lot easier at data hiding in that sense compared to DTT where defeq is a thing

[Mario Carneiro]

Michael Stoll said:

I assume you could redefine the natural numbers to be the set of nonnegative integers, once the integers are there. But then you'll have to do that each time (and transitively) you construct a "larger" structure...

Just a side note, there is no "and transitively" here, by embedding ℚ in ℝ you get ℕ ⊂ ℝ for free, you don't have to do extra work as the chain gets longer

[Michael Stoll]

Should "the" algebraic closure of ℚ be contained in ℂ as well? and in ℂ_p for all primes p?
What about the two distinct, but equally natural, inclusions of k[t] into k[x,y]? We like to pretend that k is a subset of k[t] and k[t] is a subset of k[t,u], but k[u] should also be a subset of k[t,u], so you need to construct physically different sets representing "the" univariate polynomial ring over k. It seems to be that proceeding like this will eventually get quite painful.

[Patrick Johnson]

The construction of $\mathbb{Z}$ used in Mizar is to do the usual construction with pairs of nats to get the negative integers, and then adjoin the actual set $\mathbb{N}$ (the first initial ordinal) because no ordinal is a pair. Yes this is a hack, but they manage to keep it up all the way through ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ.

There is no need for any hack. Given some set A whose exact model we don't know, and we want to construct some set B such that A ⊂ B (with some additional conditions), we can simply model set B in any way we want (call the model B'), and then we construct the actual B as A ∪ ((B' \ A) '' λ x, x ∪ {A}). So even if we don't know anything about the internal structure of A, we can still prove what we need using the axiom of regularity of ZF.

[Mario Carneiro]

Yes, that's the hack I mentioned

[Mario Carneiro]

you can also prove it without regularity if you use $\mathcal{P}(A)$ instead IIRC

[Kevin Buzzard]

You have to be extra-careful if the model B' accidentally contains elements which are in A (but which perhaps are not identified via the canonical map from A to B').

My instinct is that we formalise mathematics in type theory precisely so we can avoid nonsense like this. In other words, these hacks solve a problem in set theory which doesn't need to be solved in type theory.

[Mario Carneiro]

the trick Patrick Johnson mentions is to "shift" the elements of B to move them away from A, which works in general as long as A is a set

[Mario Carneiro]

The type theory solution is to say "this problem is stupid, let's just stop talking about it" rather than coming up with a solution. We just use embeddings everywhere (which you can also do in ZFC if you want)

[Kevin Buzzard]

In Patrick's solution there is an incorrectB' \ A. I don't think it works as it stands, but I'm just splitting hairs. The issue is that there is a canonical map c from A to B' but there is also the issue that an element of A might accidentally be in B' because set theory. I think Patrick shoudl be doing B' \ c(A).

[Mario Carneiro]

oh I see what you mean. Yes, you start with the set B' \ c(A) and then "disjointify" it with A to form set isomorphic to B' which contains A as a subset

[Reid Barton]

In a constructive setting, you couldn't do it like this in general because maybe $A \subseteq B$ but $B$ is not the disjoint union of $A$ and anything.

[Kevin Buzzard]

Is this why I've never heard of homotopy set theory?

[Mario Carneiro]

It's called homotopy theory :grinning_face_with_smiling_eyes:

[Patrick Johnson]

Not pretending to be an advocate for set theory, just providing different points of view how limitations of DTT can be resolved in other systems. The point is that set theory is not "missing" anything. Given some purely set-theoretic theorem prover, we can implement inductive macro for creating inductive types, just like Lean does. For instance, we can create List type:

inductive List (α : Set) : Set
| nil ∈ List α
| ∀ (x ∈ α) (l ∈ List α), cons x l ∈ List α

The macro would create the following constants (terms defined using choice, effectively constants):

List : Set → Set
nil : Set
cons : Set → Set → Set
rec : t → (Set → Set → t → t) → Set → t

And prove the following theorems for us:

∀ (α : Set), nil ∈ List α
∀ (α : Set) (x ∈ α) (l ∈ List α), cons x l ∈ List α
∀ (α : Set) (x ∈ α) (l ∈ list α), nil ≠ cons x l
∀ (α : Set) (x₁ x₂ ∈ α) (l₁ l₂ ∈ List α),
  cons x₁ l₁ = cons x₂ l₂ → x₁ = x₂ ∧ l₁ = l₂
∀ (α : Set) (z : t) (f : Set → Set → t → t), rec z f nil = z
∀ (α : Set) (z : t) (f : Set → Set → t → t) (x ∈ α) (l ∈ List α),
  rec z f (cons x l) = f x l (rec z f l)
∀ (P : Set → Prop) (α : Set),
  P nil → (∀ (x ∈ α) (l ∈ List α), P l → P (cons x l)) →
  ∀ (l ∈ List α), P l

The first two theorems correspond to type inference in Lean. They can be marked as "type class instances" and solved automatically using facts from the local context. The theorems involving rec correspond to computation in Lean. They can be marked as simplification theorems and "unfolded" when necessary.

One of the advantages of this is that most of the times you don't need to bother about "types". The inference does the job and everything aligns perfectly. However, if you want to express some more complex things (which would require heq in Lean), you can do that without any problem. The only artifact would be additional goal to prove that l ∈ List α for some l and α if it can't be proved automatically. In contrast, Lean would yell at you due to type mismatch or motive not being type correct.