Inequality of Types

Stream: general

[DayDun]

Is it possible to prove that two Types are not equal? Such as nat and bool. Usually induction can be used to prove inequality of regular values, but is it possible to perform induction over Types?

[Junyan Xu]

nat ≠ bool is easy to prove, but if the two types have the same cardinality, then it's probably undecidable independent of Lean's type theory whether they are equal.

import data.fintype.basic

example : nat ≠ bool :=
begin
  intro h,
  have := congr_arg finite h,
  revert this,
  simp only [nat.infinite, imp_false, bool.fintype.finite,
    not_finite_iff_infinite, eq_iff_iff, iff_true],
end

[DayDun]

Thanks! That's an interesting way of proving it. Is there anything special about cardinality though? Wouldn't it be possible to construct some other proposition which holds for one type but not the other?

[Adam Topaz]

If you can prove that there is no bijection between your two types, then you can prove that the two types are not equal.

[DayDun]

So lean considers them equal if there's a bijection between the types?

[Junyan Xu]

@Mario Carneiro seems to indicate the existence of a "minimal model" of Lean's type theory such that nat = int and a "maximal model" such that nat ≠ int here (update: more explicit claim). I don't think the models are explicitly written down though. The model in his master thesis is probably closer to the maximal model.

[Mario Carneiro]

I have some unfinished work on a slightly more maximal model, where you can tag types with their method of construction and thus distinguish between identically defined inductive types or functions vs universes vs structures

[Mario Carneiro]

The cardinality model seems straightforward enough but it has not been written down in detail

[Mario Carneiro]

It would probably make more sense to write down a scheme for constructing models with any collection of types under some assumptions

[Mario Carneiro]

Assuming there are no issues in the construction, the cardinality model implies that the only thing you can use to provably distinguish types in lean is cardinality

[Mario Carneiro]

In more detail, the cardinality model works as follows: Types are represented as cardinals (initial ordinals), and we fix in advance a family of bijections for every possible way you can interpret a cardinal as a pair, a sigma type, a function type, a universe etc. The elements of a type are just the elements of the cardinal in the ZFC sense. Then when $f : A \to B$ and $x : A$, $f\;x$ is interpreted as taking $f \in |A \to B|$, using the chosen bijection $\tau_{|A|,|B|}:|A \to B|\simeq(|A| \to |B|)$ to get a function $\tau_{|A|,|B|}(f)$, and then applying it to $x$ to get an element $\tau_{|A|,|B|}(f)(x)\in |B|$.

[Kevin Buzzard]

@DayDun the point is that equality of types is often neither provable nor disprovable, because the axioms of type theory don't tell you what's going on "under the hood". An analogy would be that if I don't explicitly tell you which construction of the integers I'm using in a model of mathematics built within set theory then you can never be 100% sure whether the set underlying the integers happens to conclude with the set underlying the naturals.

[DayDun]

What determines if a pair of types can be compared? Just the cardinality?

[Kevin Buzzard]

Again: if two types don't have the same cardinality then they are not equal, and if they do then it's almost certainly undecidable whether they're equal or not and hence it's not the right question.

[Kevin Buzzard]

If you make two different classes in the same way in a programming language and then ask whether these classes are equal, the question doesn't really make sense, it will depend on things like how the compiler actually implemented the classes. It's not a meaningful question. This isn't set theory, where extensionality gives you a built in criterion for equality of sets.

[Mario Carneiro]

There are also examples in the other direction, where two not-obviously equal types are provably equal in lean. These are normally things like {x : nat // x > 0} vs {x : nat // x != 0}: here the types themselves are equal, because they are the subtype function applied to two lambdas that are equal due to funext and propext

[Mario Carneiro]

There aren't too many examples like this, it is basically only when you give equal arguments to a type former (and hence the resulting types have to be equal because type formers are functions and obey congr_arg like everything else).

[Mario Carneiro]

The other kind of example is when a type former can't be injective simply by cantor's theorem:

import tactic.by_contra
import logic.function.basic

inductive foo : set Type → Type

example : ∃ x y, x ≠ y ∧ foo x = foo y :=
begin
  by_contra' H,
  exact function.cantor_injective foo (λ x y h, by_contra $ λ h', H _ _ h' h),
end

(This one was responsible for an unsoundness in Agda, which wanted to assume all type formers are injective.)